[STATEMENT]
lemma slp_preds:
  assumes "n -as\<rightarrow>\<^bsub>sl\<^esub>* n'" and "preds (kinds as) (cf#cfs)"
  and "length cfs = length cfs'"
  shows "preds (kinds as) (cf#cfs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preds (kinds as) (cf # cfs')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. preds (kinds as) (cf # cfs')
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^bsub>sl\<^esub>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'
[PROOF STEP]
have "n -as\<rightarrow>* n'" and "same_level_path_aux [] as"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^bsub>sl\<^esub>* n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& same_level_path_aux [] as
[PROOF STEP]
by(simp_all add:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>* n'
same_level_path_aux [] as

goal (1 subgoal):
 1. preds (kinds as) (cf # cfs')
[PROOF STEP]
from \<open>n -as\<rightarrow>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n'
[PROOF STEP]
have "\<forall>a \<in> set as. valid_edge a"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'

goal (1 subgoal):
 1. \<forall>a\<in>set as. valid_edge a
[PROOF STEP]
by(rule path_valid_edges)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. valid_edge a

goal (1 subgoal):
 1. preds (kinds as) (cf # cfs')
[PROOF STEP]
with \<open>same_level_path_aux [] as\<close> \<open>preds (kinds as) (cf#cfs)\<close>
    \<open>length cfs = length cfs'\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux [] as
preds (kinds as) (cf # cfs)
length cfs = length cfs'
\<forall>a\<in>set as. valid_edge a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [] as
preds (kinds as) (cf # cfs)
length cfs = length cfs'
\<forall>a\<in>set as. valid_edge a

goal (1 subgoal):
 1. preds (kinds as) (cf # cfs')
[PROOF STEP]
by(fastforce elim!:slpa_preds)
[PROOF STATE]
proof (state)
this:
preds (kinds as) (cf # cfs')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma liouville_lambda_prime [simp]: "prime p \<Longrightarrow> liouville_lambda p = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> liouville_lambda p = - (1::'a)
[PROOF STEP]
by (simp add: liouville_lambda_def prime_factorization_prime)


[STATEMENT]
lemma liouville_lambda_prime_power [simp]: "prime p \<Longrightarrow> liouville_lambda (p ^ k) = (-1) ^ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> liouville_lambda (p ^ k) = (- (1::'a)) ^ k
[PROOF STEP]
by (simp add: liouville_lambda_def prime_factorization_prime_power)


[STATEMENT]
lemma liouville_lambda_squarefree: "squarefree n \<Longrightarrow> liouville_lambda n = moebius_mu n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree n \<Longrightarrow> liouville_lambda n = moebius_mu n
[PROOF STEP]
by (auto simp: liouville_lambda_def moebius_mu_squarefree_eq' intro!: Nat.gr0I)


[STATEMENT]
lemma power_neg_one_If: "(-1) ^ n = (if even n then 1 else -1 :: 'a :: ring_1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (1::'a)) ^ n = (if even n then 1::'a else - (1::'a))
[PROOF STEP]
by (induction n) (simp_all split: if_splits)


[STATEMENT]
lemma liouville_lambda_power_even:
  "n > 0 \<Longrightarrow> even m \<Longrightarrow> liouville_lambda (n ^ m) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; even m\<rbrakk> \<Longrightarrow> liouville_lambda (n ^ m) = (1::'a)
[PROOF STEP]
by (subst liouville_lambda.power) (auto elim!: evenE simp: liouville_lambda_def power_neg_one_If)


[STATEMENT]
lemma liouville_lambda_power_odd:
  "odd m \<Longrightarrow> liouville_lambda (n ^ m) = liouville_lambda n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd m \<Longrightarrow> liouville_lambda (n ^ m) = liouville_lambda n
[PROOF STEP]
by (subst liouville_lambda.power) (auto elim!: oddE simp: liouville_lambda_def power_neg_one_If)


[STATEMENT]
lemma liouville_lambda_power:
  "liouville_lambda (n ^ m) =
     (if n = 0 \<and> m > 0 then 0 else if even m then 1 else liouville_lambda n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liouville_lambda (n ^ m) = (if n = 0 \<and> 0 < m then 0::'a else if even m then 1::'a else liouville_lambda n)
[PROOF STEP]
by (auto simp: liouville_lambda_power_even liouville_lambda_power_odd power_0_left)


[STATEMENT]
lemma liouville_lambda_divisors_sum:
  "(\<Sum>d | d dvd n. liouville_lambda d) = ind is_square n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. liouville_lambda d) = ind is_square n
[PROOF STEP]
proof (rule multiplicative_function_eqI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. multiplicative_function (\<lambda>a. \<Sum>d | d dvd a. liouville_lambda d)
 2. multiplicative_function (ind is_square)
 3. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
show "multiplicative_function (\<lambda>n. (\<Sum>d | d dvd n. liouville_lambda d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. \<Sum>d | d dvd n. liouville_lambda d)
[PROOF STEP]
by (rule liouville_lambda.multiplicative_sum_divisors)
[PROOF STATE]
proof (state)
this:
multiplicative_function (\<lambda>n. \<Sum>d | d dvd n. liouville_lambda d)

goal (2 subgoals):
 1. multiplicative_function (ind is_square)
 2. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
show "multiplicative_function (ind is_square)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (ind is_square)
[PROOF STEP]
by (rule is_nth_power.multiplicative_function_axioms)
[PROOF STATE]
proof (state)
this:
multiplicative_function (ind is_square)

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
fix p k :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
assume pk: "prime p" "k > 0"
[PROOF STATE]
proof (state)
this:
prime p
0 < k

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
hence p_gt_1: "p > 1"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < k

goal (1 subgoal):
 1. 1 < p
[PROOF STEP]
by (simp add: prime_gt_Suc_0_nat)
[PROOF STATE]
proof (state)
this:
1 < p

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
have "(\<Sum>d | d dvd p ^ k. liouville_lambda d) = (\<Sum>d\<in>(\<lambda>i. p ^ i) ` {..k}. liouville_lambda d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd p ^ k. liouville_lambda d) = sum liouville_lambda ((^) p ` {..k})
[PROOF STEP]
using pk
[PROOF STATE]
proof (prove)
using this:
prime p
0 < k

goal (1 subgoal):
 1. (\<Sum>d | d dvd p ^ k. liouville_lambda d) = sum liouville_lambda ((^) p ` {..k})
[PROOF STEP]
by (intro sum.cong refl) (auto intro: le_imp_power_dvd simp: divides_primepow_nat)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd p ^ k. liouville_lambda d) = sum liouville_lambda ((^) p ` {..k})

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd p ^ k. liouville_lambda d) = sum liouville_lambda ((^) p ` {..k})

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
from pk and p_gt_1
[PROOF STATE]
proof (chain)
picking this:
prime p
0 < k
1 < p
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. liouville_lambda (p ^ i))"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < k
1 < p

goal (1 subgoal):
 1. sum liouville_lambda ((^) p ` {..k}) = (\<Sum>i\<le>k. liouville_lambda (p ^ i))
[PROOF STEP]
by (subst sum.reindex) (auto simp: inj_on_def prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
sum liouville_lambda ((^) p ` {..k}) = (\<Sum>i\<le>k. liouville_lambda (p ^ i))

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum liouville_lambda ((^) p ` {..k}) = (\<Sum>i\<le>k. liouville_lambda (p ^ i))

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
from pk
[PROOF STATE]
proof (chain)
picking this:
prime p
0 < k
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. (-1) ^ i)"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < k

goal (1 subgoal):
 1. (\<Sum>i\<le>k. liouville_lambda (p ^ i)) = sum ((^) (- (1::'b))) {..k}
[PROOF STEP]
by (intro sum.cong refl) simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. liouville_lambda (p ^ i)) = sum ((^) (- (1::?'b3))) {..k}

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. liouville_lambda (p ^ i)) = sum ((^) (- (1::?'b3))) {..k}

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
have "\<dots> = (if even k then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) (- (1::'b))) {..k} = (if even k then 1::'b else (0::'b))
[PROOF STEP]
by (induction k) auto
[PROOF STATE]
proof (state)
this:
sum ((^) (- (1::?'b4))) {..k} = (if even k then 1::?'b4 else (0::?'b4))

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((^) (- (1::?'b4))) {..k} = (if even k then 1::?'b4 else (0::?'b4))

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
from pk
[PROOF STATE]
proof (chain)
picking this:
prime p
0 < k
[PROOF STEP]
have "\<dots> = ind is_square (p ^ k)"
[PROOF STATE]
proof (prove)
using this:
prime p
0 < k

goal (1 subgoal):
 1. (if even k then 1::'b else (0::'b)) = ind is_square (p ^ k)
[PROOF STEP]
by (simp add: is_square.prime_power)
[PROOF STATE]
proof (state)
this:
(if even k then 1::?'b5 else (0::?'b5)) = ind is_square (p ^ k)

goal (1 subgoal):
 1. \<And>p k. \<lbrakk>prime p; 0 < k\<rbrakk> \<Longrightarrow> (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
show "(\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)

goal (1 subgoal):
 1. (\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd p ^ k. liouville_lambda d) = ind is_square (p ^ k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_liouville_lambda_times_zeta: "fds liouville_lambda * fds_zeta = fds_ind is_square"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds liouville_lambda * fds_zeta = fds_ind is_square
[PROOF STEP]
by (rule fds_eqI) (simp add: liouville_lambda_divisors_sum fds_nth_mult dirichlet_prod_def)


[STATEMENT]
lemma fds_liouville_lambda: "fds liouville_lambda = fds_ind is_square * fds moebius_mu"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
have "fds liouville_lambda * fds_zeta * fds moebius_mu = fds_ind is_square * fds moebius_mu"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds liouville_lambda * fds_zeta * fds moebius_mu = fds_ind is_square * fds moebius_mu
[PROOF STEP]
by (simp add: fds_liouville_lambda_times_zeta)
[PROOF STATE]
proof (state)
this:
fds liouville_lambda * fds_zeta * fds moebius_mu = fds_ind is_square * fds moebius_mu

goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fds liouville_lambda * fds_zeta * fds moebius_mu = fds_ind is_square * fds moebius_mu

goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
have "fds liouville_lambda * fds_zeta * fds moebius_mu = fds liouville_lambda"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds liouville_lambda * fds_zeta * fds moebius_mu = fds liouville_lambda
[PROOF STEP]
by (simp only: mult.assoc fds_zeta_times_moebius_mu mult_1_right)
[PROOF STATE]
proof (state)
this:
fds liouville_lambda * fds_zeta * fds moebius_mu = fds liouville_lambda

goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fds liouville_lambda = fds_ind is_square * fds moebius_mu

goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fds liouville_lambda = fds_ind is_square * fds moebius_mu

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma liouville_lambda_altdef:
  "liouville_lambda n = (\<Sum>d | d ^ 2 dvd n. moebius_mu (n div d ^ 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
have "liouville_lambda n = fds_nth (fds liouville_lambda) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liouville_lambda n = fds_nth (fds liouville_lambda) n
[PROOF STEP]
by (simp add: fds_nth_fds)
[PROOF STATE]
proof (state)
this:
liouville_lambda n = fds_nth (fds liouville_lambda) n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
liouville_lambda n = fds_nth (fds liouville_lambda) n

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
have "fds liouville_lambda = fds_ind is_square * (fds moebius_mu :: 'a fds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds liouville_lambda = fds_ind is_square * fds moebius_mu
[PROOF STEP]
by (rule fds_liouville_lambda)
[PROOF STATE]
proof (state)
this:
fds liouville_lambda = fds_ind is_square * fds moebius_mu

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fds liouville_lambda = fds_ind is_square * fds moebius_mu

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
have "fds_nth \<dots> n = (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_nth (fds_ind is_square * fds moebius_mu) n = (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d))
[PROOF STEP]
by (simp add: fds_nth_mult dirichlet_prod_def)
[PROOF STATE]
proof (state)
this:
fds_nth (fds_ind is_square * fds moebius_mu) n = (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fds_nth (fds_ind is_square * fds moebius_mu) n = (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
have "\<dots> = (\<Sum>d \<in> (\<lambda>d. d^2) ` {d. d ^ 2 dvd n}. moebius_mu (n div d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d)) = (\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d)) = (\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d))
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) (auto simp: ind_def is_nth_power_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d)) = (\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>d | d dvd n. ind is_square d * moebius_mu (n div d)) = (\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
have "\<dots> = (\<Sum>d | d ^ 2 dvd n. moebius_mu (n div d ^ 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d)) = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
by (subst sum.reindex) (auto simp: inj_on_def dest: power2_eq_imp_eq)
[PROOF STATE]
proof (state)
this:
(\<Sum>d\<in>power2 ` {d. d\<^sup>2 dvd n}. moebius_mu (n div d)) = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
 2. n \<noteq> 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))

goal (1 subgoal):
 1. liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> liouville_lambda n = (\<Sum>d | d\<^sup>2 dvd n. moebius_mu (n div d\<^sup>2))
[PROOF STEP]
qed auto


[STATEMENT]
lemma abs_moebius_mu: "abs (moebius_mu n :: 'a :: linordered_idom) = ind squarefree n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>moebius_mu n\<bar> = ind squarefree n
[PROOF STEP]
by (auto simp: ind_def moebius_mu_def)


[STATEMENT]
lemma fset_of_list_remdups [simp]: "fset_of_list (remdups l) = fset_of_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_of_list (remdups l) = fset_of_list l
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fset_of_list (remdups []) = fset_of_list []
 2. \<And>a l. fset_of_list (remdups l) = fset_of_list l \<Longrightarrow> fset_of_list (remdups (a # l)) = fset_of_list (a # l)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. fset_of_list (remdups l) = fset_of_list l \<Longrightarrow> fset_of_list (remdups (a # l)) = fset_of_list (a # l)
[PROOF STEP]
by (simp add: finsert_absorb fset_of_list_elem)


[STATEMENT]
lemma fset_both_sides: "(Abs_fset s = f) = (fset (Abs_fset s) = fset f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_fset s = f) = (fset (Abs_fset s) = fset f)
[PROOF STEP]
by (simp add: fset_inject)


[STATEMENT]
lemma Abs_ffilter: "(ffilter f s = s') = ({e \<in> (fset s). f e} = (fset s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ffilter f s = s') = ({e \<in> fset s. f e} = fset s')
[PROOF STEP]
by (simp add: ffilter_def fset_both_sides Abs_fset_inverse Set.filter_def)


[STATEMENT]
lemma size_ffilter_card: "size (ffilter f s) = card ({e \<in> (fset s). f e})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (ffilter f s) = card {e \<in> fset s. f e}
[PROOF STEP]
by (simp add: ffilter_def fset_both_sides Abs_fset_inverse Set.filter_def)


[STATEMENT]
lemma ffilter_empty [simp]: "ffilter f {||} = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffilter f {||} = {||}
[PROOF STEP]
by auto


[STATEMENT]
lemma ffilter_finsert:
  "ffilter f (finsert a s) = (if f a then finsert a (ffilter f s) else (ffilter f s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffilter f (finsert a s) = (if f a then finsert a (ffilter f s) else ffilter f s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f a \<longrightarrow> ffilter f (finsert a s) = finsert a (ffilter f s)) \<and> (\<not> f a \<longrightarrow> ffilter f (finsert a s) = ffilter f s)
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f a \<longrightarrow> ffilter f (finsert a s) = finsert a (ffilter f s)
 2. \<not> f a \<longrightarrow> ffilter f (finsert a s) = ffilter f s
[PROOF STEP]
apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f a \<longrightarrow> Set.filter f (insert a (fset s)) = insert a (Set.filter f (fset s))
 2. \<not> f a \<longrightarrow> ffilter f (finsert a s) = ffilter f s
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f a \<longrightarrow> ffilter f (finsert a s) = ffilter f s
[PROOF STEP]
apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f a \<longrightarrow> Set.filter f (insert a (fset s)) = Set.filter f (fset s)
[PROOF STEP]
by auto


[STATEMENT]
lemma fset_equiv: "(f1 = f2) = (fset f1 = fset f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f1 = f2) = (fset f1 = fset f2)
[PROOF STEP]
by (simp add: fset_inject)


[STATEMENT]
lemma finsert_equiv: "(finsert e f = f') = (insert e (fset f) = (fset f'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finsert e f = f') = (insert e (fset f) = fset f')
[PROOF STEP]
by (simp add: finsert_def fset_both_sides Abs_fset_inverse)


[STATEMENT]
lemma filter_elements:
  "x |\<in>| Abs_fset (Set.filter f (fset s)) = (x \<in> (Set.filter f (fset s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x |\<in>| Abs_fset (Set.filter f (fset s))) = (x \<in> Set.filter f (fset s))
[PROOF STEP]
by (metis ffilter.rep_eq fset_inverse notin_fset)


[STATEMENT]
lemma sorted_list_of_fempty [simp]: "sorted_list_of_fset {||} = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_fset {||} = []
[PROOF STEP]
by (simp add: sorted_list_of_fset_def)


[STATEMENT]
lemma fold_union_ffUnion: "fold (|\<union>|) l {||} = ffUnion (fset_of_list l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (|\<union>|) l {||} = ffUnion (fset_of_list l)
[PROOF STEP]
by(induct l rule: rev_induct, auto)


[STATEMENT]
lemma filter_filter:
  "ffilter P (ffilter Q xs) = ffilter (\<lambda>x. Q x \<and> P x) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffilter P (ffilter Q xs) = ffilter (\<lambda>x. Q x \<and> P x) xs
[PROOF STEP]
by auto


[STATEMENT]
lemma fsubset_strict:
  "x2 |\<subset>| x1 \<Longrightarrow> \<exists>e. e |\<in>| x1 \<and> e |\<notin>| x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 |\<subset>| x1 \<Longrightarrow> \<exists>e. e |\<in>| x1 \<and> e |\<notin>| x2
[PROOF STEP]
by auto


[STATEMENT]
lemma fsubset:
  "x2 |\<subset>| x1 \<Longrightarrow> \<nexists>e. e |\<in>| x2 \<and> e |\<notin>| x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 |\<subset>| x1 \<Longrightarrow> \<nexists>e. e |\<in>| x2 \<and> e |\<notin>| x1
[PROOF STEP]
by auto


[STATEMENT]
lemma size_fsubset_elem:
  assumes "\<exists>e. e |\<in>| x1 \<and> e |\<notin>| x2"
      and "\<nexists>e. e |\<in>| x2 \<and> e |\<notin>| x1"
    shows "size x2 < size x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size x2 < size x1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>e. e |\<in>| x1 \<and> e |\<notin>| x2
\<nexists>e. e |\<in>| x2 \<and> e |\<notin>| x1

goal (1 subgoal):
 1. size x2 < size x1
[PROOF STEP]
apply (simp add: fmember_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>e. e \<in> fset x1 \<and> e \<notin> fset x2; \<forall>e. e \<in> fset x2 \<longrightarrow> e \<in> fset x1\<rbrakk> \<Longrightarrow> card (fset x2) < card (fset x1)
[PROOF STEP]
by (metis card_seteq finite_fset linorder_not_le subsetI)


[STATEMENT]
lemma size_fsubset: "x2 |\<subset>| x1 \<Longrightarrow> size x2 < size x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2 |\<subset>| x1 \<Longrightarrow> size x2 < size x1
[PROOF STEP]
by (metis fsubset fsubset_strict size_fsubset_elem)


[STATEMENT]
lemma arg_cong_ffilter:
  "\<forall>e |\<in>| f. p e = p' e \<Longrightarrow> ffilter p f = ffilter p' f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e|\<in>|f. p e = p' e \<Longrightarrow> ffilter p f = ffilter p' f
[PROOF STEP]
by auto


[STATEMENT]
lemma ffilter_singleton: "f e \<Longrightarrow> ffilter f {|e|} = {|e|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e \<Longrightarrow> ffilter f {|e|} = {|e|}
[PROOF STEP]
apply (simp add: ffilter_def fset_both_sides Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e \<Longrightarrow> Set.filter f {e} = {e}
[PROOF STEP]
by auto


[STATEMENT]
lemma fset_eq_alt: "(x = y) = (x |\<subseteq>| y \<and> size x = size y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = y) = (x |\<subseteq>| y \<and> size x = size y)
[PROOF STEP]
by (metis exists_least_iff le_less size_fsubset)


[STATEMENT]
lemma ffold_empty [simp]: "ffold f b {||} = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold f b {||} = b
[PROOF STEP]
by (simp add: ffold_def)


[STATEMENT]
lemma sorted_list_of_fset_sort:
  "sorted_list_of_fset (fset_of_list l) = sort (remdups l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_fset (fset_of_list l) = sort (remdups l)
[PROOF STEP]
by (simp add: fset_of_list.rep_eq sorted_list_of_fset.rep_eq sorted_list_of_set_sort_remdups)


[STATEMENT]
lemma fMin_Min: "fMin (fset_of_list l) = Min (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fMin (fset_of_list l) = Min (set l)
[PROOF STEP]
by (simp add: fMin.F.rep_eq fset_of_list.rep_eq)


[STATEMENT]
lemma sorted_hd_Min:
  "sorted l \<Longrightarrow>
   l \<noteq> [] \<Longrightarrow>
   hd l = Min (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted l; l \<noteq> []\<rbrakk> \<Longrightarrow> hd l = Min (set l)
[PROOF STEP]
by (metis List.finite_set Min_eqI eq_iff hd_Cons_tl insertE list.set_sel(1) list.simps(15) sorted_simps(2))


[STATEMENT]
lemma hd_sort_remdups: "hd (sort (remdups l)) = hd (sort l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (sort (remdups l)) = hd (sort l)
[PROOF STEP]
by (metis hd_sort_Min remdups_eq_nil_iff set_remdups)


[STATEMENT]
lemma hd_sorted_list_of_fset:
  "s \<noteq> {||} \<Longrightarrow> hd (sorted_list_of_fset s) = (fMin s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> {||} \<Longrightarrow> hd (sorted_list_of_fset s) = fMin s
[PROOF STEP]
apply (insert exists_fset_of_list[of s])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> {||}; \<exists>l. s = fset_of_list l\<rbrakk> \<Longrightarrow> hd (sorted_list_of_fset s) = fMin s
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>s \<noteq> {||}; s = fset_of_list l\<rbrakk> \<Longrightarrow> hd (sorted_list_of_fset s) = fMin s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>fset_of_list l \<noteq> {||}; s = fset_of_list l\<rbrakk> \<Longrightarrow> hd (sorted_list_of_fset (fset_of_list l)) = fMin (fset_of_list l)
[PROOF STEP]
apply (simp add: sorted_list_of_fset_sort fMin_Min hd_sort_remdups)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>fset_of_list l \<noteq> {||}; s = fset_of_list l\<rbrakk> \<Longrightarrow> hd (sort l) = Min (set l)
[PROOF STEP]
by (metis fset_of_list_simps(1) hd_sort_Min)


[STATEMENT]
lemma fminus_filter_singleton:
  "fset_of_list l |-| {|x|} = fset_of_list (filter (\<lambda>e. e \<noteq> x) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_of_list l |-| {|x|} = fset_of_list (filter (\<lambda>e. e \<noteq> x) l)
[PROOF STEP]
by auto


[STATEMENT]
lemma card_minus_fMin:
  "s \<noteq> {||} \<Longrightarrow> card (fset s - {fMin s}) < card (fset s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> {||} \<Longrightarrow> card (fset s - {fMin s}) < card (fset s)
[PROOF STEP]
by (metis Min_in bot_fset.rep_eq card_Diff1_less fMin.F.rep_eq finite_fset fset_equiv)


[STATEMENT]
lemma sorted_list_of_fset_Cons:
  "\<exists>h t. (sorted_list_of_fset (finsert s ss)) = h#t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h t. sorted_list_of_fset (finsert s ss) = h # t
[PROOF STEP]
apply (simp add: sorted_list_of_fset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h t. insort s (sorted_list_of_set (fset ss - {s})) = h # t
[PROOF STEP]
by (cases "insort s (sorted_list_of_set (fset ss - {s}))", auto)


[STATEMENT]
lemma list_eq_hd_tl:
  "l \<noteq> [] \<Longrightarrow>
   hd l = h \<Longrightarrow>
   tl l = t \<Longrightarrow>
   l = (h#t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<noteq> []; hd l = h; tl l = t\<rbrakk> \<Longrightarrow> l = h # t
[PROOF STEP]
by auto


[STATEMENT]
lemma fset_of_list_sort: "fset_of_list l = fset_of_list (sort l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_of_list l = fset_of_list (sort l)
[PROOF STEP]
by (simp add: fset_of_list.abs_eq)


[STATEMENT]
lemma exists_sorted_distinct_fset_of_list:
  "\<exists>l. sorted l \<and> distinct l \<and> f = fset_of_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. sorted l \<and> distinct l \<and> f = fset_of_list l
[PROOF STEP]
by (metis distinct_sorted_list_of_set sorted_list_of_fset.rep_eq sorted_list_of_fset_simps(2) sorted_sorted_list_of_set)


[STATEMENT]
lemma fset_of_list_empty [simp]: "(fset_of_list l = {||}) = (l = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fset_of_list l = {||}) = (l = [])
[PROOF STEP]
by (metis fset_of_list.rep_eq fset_of_list_simps(1) set_empty)


[STATEMENT]
lemma ffold_ord_cons: assumes sorted: "sorted (h#t)"
    and distinct: "distinct (h#t)"
  shows "ffold_ord f (fset_of_list (h#t)) b = ffold_ord f (fset_of_list t) (f h b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
have h_is_min: "h = fMin (fset_of_list (h#t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = fMin (fset_of_list (h # t))
[PROOF STEP]
by (metis sorted fMin_Min list.sel(1) list.simps(3) sorted_hd_Min)
[PROOF STATE]
proof (state)
this:
h = fMin (fset_of_list (h # t))

goal (1 subgoal):
 1. ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
have remove_min: "fset_of_list t = (fset_of_list (h#t)) - {|h|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset_of_list t = fset_of_list (h # t) |-| {|h|}
[PROOF STEP]
using distinct fset_of_list_elem
[PROOF STATE]
proof (prove)
using this:
distinct (h # t)
(?x |\<in>| fset_of_list ?xs) = (?x \<in> set ?xs)

goal (1 subgoal):
 1. fset_of_list t = fset_of_list (h # t) |-| {|h|}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fset_of_list t = fset_of_list (h # t) |-| {|h|}

goal (1 subgoal):
 1. ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
apply (simp only: ffold_ord.simps[of f "fset_of_list (h#t)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if fset_of_list (h # t) = {||} then b else let ha = fMin (fset_of_list (h # t)); t = fset_of_list (h # t) |-| {|ha|} in ffold_ord f t (f ha b)) = ffold_ord f (fset_of_list t) (f h b)
[PROOF STEP]
by (metis h_is_min remove_min fset_of_list_empty list.distinct(1))
[PROOF STATE]
proof (state)
this:
ffold_ord f (fset_of_list (h # t)) b = ffold_ord f (fset_of_list t) (f h b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_distinct_ffold_ord: assumes "sorted l"
      and "distinct l"
    shows "ffold_ord f (fset_of_list l) b = fold f l b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold_ord f (fset_of_list l) b = fold f l b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted l
distinct l

goal (1 subgoal):
 1. ffold_ord f (fset_of_list l) b = fold f l b
[PROOF STEP]
apply (induct l arbitrary: b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>sorted []; distinct []\<rbrakk> \<Longrightarrow> ffold_ord f (fset_of_list []) b = fold f [] b
 2. \<And>a l b. \<lbrakk>\<And>b. \<lbrakk>sorted l; distinct l\<rbrakk> \<Longrightarrow> ffold_ord f (fset_of_list l) b = fold f l b; sorted (a # l); distinct (a # l)\<rbrakk> \<Longrightarrow> ffold_ord f (fset_of_list (a # l)) b = fold f (a # l) b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l b. \<lbrakk>\<And>b. \<lbrakk>sorted l; distinct l\<rbrakk> \<Longrightarrow> ffold_ord f (fset_of_list l) b = fold f l b; sorted (a # l); distinct (a # l)\<rbrakk> \<Longrightarrow> ffold_ord f (fset_of_list (a # l)) b = fold f (a # l) b
[PROOF STEP]
by (metis distinct.simps(2) ffold_ord_cons fold_simps(2) sorted_simps(2))


[STATEMENT]
lemma ffold_ord_fold_sorted: "ffold_ord f s b = fold f (sorted_list_of_fset s) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffold_ord f s b = fold f (sorted_list_of_fset s) b
[PROOF STEP]
by (metis exists_sorted_distinct_fset_of_list sorted_distinct_ffold_ord distinct_remdups_id sorted_list_of_fset_sort sorted_sort_id)


[STATEMENT]
lemma fprod_empty_l: "{||} |\<times>| a = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {||} |\<times>| a = {||}
[PROOF STEP]
using bot_fset_def fprod.abs_eq
[PROOF STATE]
proof (prove)
using this:
{||} \<equiv> Abs_fset {}
?xa |\<times>| ?x = Abs_fset (fset ?xa \<times> fset ?x)

goal (1 subgoal):
 1. {||} |\<times>| a = {||}
[PROOF STEP]
by force


[STATEMENT]
lemma fprod_empty_r: "a |\<times>| {||} = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a |\<times>| {||} = {||}
[PROOF STEP]
by (simp add: fprod_def bot_fset_def Abs_fset_inverse)


[STATEMENT]
lemma fprod_finsert: "(finsert a as) |\<times>| (finsert b bs) =
   finsert (a, b) (fimage (\<lambda>b. (a, b)) bs |\<union>| fimage (\<lambda>a. (a, b)) as |\<union>| (as |\<times>| bs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsert a as |\<times>| finsert b bs = finsert (a, b) (Pair a |`| bs |\<union>| (\<lambda>a. (a, b)) |`| as |\<union>| as |\<times>| bs)
[PROOF STEP]
apply (simp add: fprod_def fset_both_sides Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (a, b) (fset as \<times> insert b (fset bs) \<union> insert a (fset as) \<times> fset bs) = insert (a, b) (Pair a ` fset bs \<union> (\<lambda>a. (a, b)) ` fset as \<union> fset as \<times> fset bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma fprod_member:
  "x |\<in>| xs \<Longrightarrow>
   y |\<in>| ys \<Longrightarrow>
   (x, y) |\<in>| xs |\<times>| ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x |\<in>| xs; y |\<in>| ys\<rbrakk> \<Longrightarrow> (x, y) |\<in>| xs |\<times>| ys
[PROOF STEP]
by (simp add: fmember_def fprod_def Abs_fset_inverse)


[STATEMENT]
lemma fprod_subseteq:
  "x |\<subseteq>| x' \<and> y |\<subseteq>| y' \<Longrightarrow> x |\<times>| y |\<subseteq>| x' |\<times>| y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x |\<subseteq>| x' \<and> y |\<subseteq>| y' \<Longrightarrow> x |\<times>| y |\<subseteq>| x' |\<times>| y'
[PROOF STEP]
apply (simp add: fprod_def less_eq_fset_def Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fset x \<subseteq> fset x' \<and> fset y \<subseteq> fset y' \<Longrightarrow> fset x \<times> fset y \<subseteq> fset x' \<times> fset y'
[PROOF STEP]
by auto


[STATEMENT]
lemma fimage_fprod:
  "(a, b) |\<in>| A |\<times>| B \<Longrightarrow> f a b |\<in>| (\<lambda>(x, y). f x y) |`| (A |\<times>| B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) |\<in>| A |\<times>| B \<Longrightarrow> f a b |\<in>| (\<lambda>(x, y). f x y) |`| (A |\<times>| B)
[PROOF STEP]
by force


[STATEMENT]
lemma fprod_singletons: "{|a|} |\<times>| {|b|} = {|(a, b)|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {|a|} |\<times>| {|b|} = {|(a, b)|}
[PROOF STEP]
apply (simp add: fprod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_fset {(a, b)} = {|(a, b)|}
[PROOF STEP]
by (metis fset_inverse fset_simps(1) fset_simps(2))


[STATEMENT]
lemma fprod_equiv:
  "(fset (f |\<times>| f') = s) = (((fset f) \<times> (fset f')) = s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fset (f |\<times>| f') = s) = (fset f \<times> fset f' = s)
[PROOF STEP]
by (simp add: fprod_def Abs_fset_inverse)


[STATEMENT]
lemma fis_singleton_alt: "fis_singleton f = (\<exists>e. f = {|e|})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fis_singleton f = (\<exists>e. f = {|e|})
[PROOF STEP]
by (metis fis_singleton.rep_eq fset_inverse fset_simps(1) fset_simps(2) is_singleton_def)


[STATEMENT]
lemma singleton_singleton [simp]: "fis_singleton {|a|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fis_singleton {|a|}
[PROOF STEP]
by (simp add: fis_singleton_def)


[STATEMENT]
lemma not_singleton_empty [simp]: "\<not> fis_singleton {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> fis_singleton {||}
[PROOF STEP]
apply (simp add: fis_singleton_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_singleton {}
[PROOF STEP]
by (simp add: is_singleton_altdef)


[STATEMENT]
lemma fis_singleton_fthe_elem:
  "fis_singleton A \<longleftrightarrow> A = {|fthe_elem A|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fis_singleton A = (A = {|fthe_elem A|})
[PROOF STEP]
by (metis fis_singleton_alt fthe_felem_eq)


[STATEMENT]
lemma fBall_ffilter:
  "\<forall>x |\<in>| X. f x \<Longrightarrow> ffilter f X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fBall X f \<Longrightarrow> ffilter f X = X
[PROOF STEP]
by auto


[STATEMENT]
lemma fBall_ffilter2:
  "X = Y \<Longrightarrow>
   \<forall>x |\<in>| X. f x \<Longrightarrow>
   ffilter f X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X = Y; fBall X f\<rbrakk> \<Longrightarrow> ffilter f X = Y
[PROOF STEP]
by auto


[STATEMENT]
lemma size_fset_of_list: "size (fset_of_list l) = length (remdups l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (fset_of_list l) = length (remdups l)
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. size (fset_of_list []) = length (remdups [])
 2. \<And>a l. size (fset_of_list l) = length (remdups l) \<Longrightarrow> size (fset_of_list (a # l)) = length (remdups (a # l))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. size (fset_of_list l) = length (remdups l) \<Longrightarrow> size (fset_of_list (a # l)) = length (remdups (a # l))
[PROOF STEP]
by (simp add: fset_of_list.rep_eq insert_absorb)


[STATEMENT]
lemma size_fsingleton: "(size f = 1) = (\<exists>e. f = {|e|})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (size f = 1) = (\<exists>e. f = {|e|})
[PROOF STEP]
apply (insert exists_fset_of_list[of f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. f = fset_of_list l \<Longrightarrow> (size f = 1) = (\<exists>e. f = {|e|})
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. f = fset_of_list l \<Longrightarrow> (size (fset_of_list l) = 1) = (\<exists>e. fset_of_list l = {|e|})
[PROOF STEP]
apply (simp only: size_fset_of_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. f = fset_of_list l \<Longrightarrow> (length (remdups l) = 1) = (\<exists>e. fset_of_list l = {|e|})
[PROOF STEP]
apply (simp add: fset_of_list_def fset_both_sides Abs_fset_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. f = Abs_fset (set l) \<Longrightarrow> (length (remdups l) = Suc 0) = (\<exists>e. set l = {e})
[PROOF STEP]
by (metis List.card_set One_nat_def card.insert card_1_singletonE card.empty empty_iff finite.intros(1))


[STATEMENT]
lemma ffilter_mono: "(ffilter X xs = f) \<Longrightarrow> \<forall>x |\<in>| xs. X x = Y x \<Longrightarrow> (ffilter Y xs = f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ffilter X xs = f; \<forall>x|\<in>|xs. X x = Y x\<rbrakk> \<Longrightarrow> ffilter Y xs = f
[PROOF STEP]
by auto


[STATEMENT]
lemma size_fimage: "size (fimage f s) \<le> size s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (f |`| s) \<le> size s
[PROOF STEP]
apply (induct s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. size (f |`| {||}) \<le> size {||}
 2. \<And>x s. \<lbrakk>x |\<notin>| s; size (f |`| s) \<le> size s\<rbrakk> \<Longrightarrow> size (f |`| finsert x s) \<le> size (finsert x s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x |\<notin>| s; size (f |`| s) \<le> size s\<rbrakk> \<Longrightarrow> size (f |`| finsert x s) \<le> size (finsert x s)
[PROOF STEP]
by (simp add: card_insert_if)


[STATEMENT]
lemma size_ffilter: "size (ffilter P f) \<le> size f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (ffilter P f) \<le> size f
[PROOF STEP]
apply (induct f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. size (ffilter P {||}) \<le> size {||}
 2. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f\<rbrakk> \<Longrightarrow> size (ffilter P (finsert x f)) \<le> size (finsert x f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f\<rbrakk> \<Longrightarrow> size (ffilter P (finsert x f)) \<le> size (finsert x f)
[PROOF STEP]
apply (simp only: ffilter_finsert)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f\<rbrakk> \<Longrightarrow> size (if P x then finsert x (ffilter P f) else ffilter P f) \<le> size (finsert x f)
[PROOF STEP]
apply (case_tac "P x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f; P x\<rbrakk> \<Longrightarrow> size (if P x then finsert x (ffilter P f) else ffilter P f) \<le> size (finsert x f)
 2. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f; \<not> P x\<rbrakk> \<Longrightarrow> size (if P x then finsert x (ffilter P f) else ffilter P f) \<le> size (finsert x f)
[PROOF STEP]
apply (simp add: fmember.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; size (ffilter P f) \<le> size f; \<not> P x\<rbrakk> \<Longrightarrow> size (if P x then finsert x (ffilter P f) else ffilter P f) \<le> size (finsert x f)
[PROOF STEP]
by (simp add: card_insert_if)


[STATEMENT]
lemma ffilter_size_le: "\<And>f s. size s \<le> n \<Longrightarrow> size (ffilter f s) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f s. size s \<le> n \<Longrightarrow> size (ffilter f s) \<le> n
[PROOF STEP]
using dual_order.trans size_ffilter
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
size (ffilter ?P ?f) \<le> size ?f

goal (1 subgoal):
 1. \<And>f s. size s \<le> n \<Longrightarrow> size (ffilter f s) \<le> n
[PROOF STEP]
by blast


[STATEMENT]
lemma set_membership_eq: "A = B \<longleftrightarrow> (\<lambda>x. Set.member x A) = (\<lambda>x. Set.member x B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A = B) = ((\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> B))
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A = B \<Longrightarrow> (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> B)
 2. (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> B) \<Longrightarrow> A = B
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> B) \<Longrightarrow> A = B
[PROOF STEP]
by (meson equalityI subsetI)


[STATEMENT]
lemma size_le_1: "size f \<le> 1 = (f = {||} \<or> (\<exists>e. f = {|e|}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (size f \<le> 1) = (f = {||} \<or> (\<exists>e. f = {|e|}))
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. size f \<le> 1 \<Longrightarrow> f = {||} \<or> (\<exists>e. f = {|e|})
 2. f = {||} \<or> (\<exists>e. f = {|e|}) \<Longrightarrow> size f \<le> 1
[PROOF STEP]
apply (metis bot.not_eq_extremum gr_implies_not0 le_neq_implies_less less_one size_fsingleton size_fsubset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = {||} \<or> (\<exists>e. f = {|e|}) \<Longrightarrow> size f \<le> 1
[PROOF STEP]
by auto


[STATEMENT]
lemma size_gt_1: "1 < size f \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> f = finsert e1 (finsert e2 f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < size f \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> f = finsert e1 (finsert e2 f')
[PROOF STEP]
apply (induct f)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1 < size {||} \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> {||} = finsert e1 (finsert e2 f')
 2. \<And>x f. \<lbrakk>x |\<notin>| f; 1 < size f \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> f = finsert e1 (finsert e2 f'); 1 < size (finsert x f)\<rbrakk> \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> finsert x f = finsert e1 (finsert e2 f')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; 1 < size f \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> f = finsert e1 (finsert e2 f'); 1 < size (finsert x f)\<rbrakk> \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> finsert x f = finsert e1 (finsert e2 f')
[PROOF STEP]
apply (rule_tac x=x in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>x |\<notin>| f; 1 < size f \<Longrightarrow> \<exists>e1 e2 f'. e1 \<noteq> e2 \<and> f = finsert e1 (finsert e2 f'); 1 < size (finsert x f)\<rbrakk> \<Longrightarrow> \<exists>e2 f'. x \<noteq> e2 \<and> finsert x f = finsert x (finsert e2 f')
[PROOF STEP]
by (metis finsertCI leD not_le_imp_less size_le_1)


[STATEMENT]
lemma subst_hfml_Conj[simp]:
  "(HConj A B)(i:::=x) = HConj (A(i:::=x)) (B(i:::=x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A HAND B)(i:::=x) = A(i:::=x) HAND B(i:::=x)
[PROOF STEP]
unfolding HConj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HNeg (A HIMP HNeg B))(i:::=x) = HNeg (A(i:::=x) HIMP HNeg (B(i:::=x)))
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_quot_hfm[simp]: "subst i \<guillemotleft>P\<guillemotright> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A(i:::=P)\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst i \<guillemotleft>P\<guillemotright> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A(i:::=P)\<guillemotright>
[PROOF STEP]
by (induction A) auto


[STATEMENT]
lemma hfm_to_fm_Conj[simp]:
  "hfm_to_fm (HConj A B) = Conj (hfm_to_fm A) (hfm_to_fm B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfm_to_fm (A HAND B) = hfm_to_fm A AND hfm_to_fm B
[PROOF STEP]
unfolding HConj_def Conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfm_to_fm (HNeg (A HIMP HNeg B)) = Neg (hfm_to_fm A IMP Neg (hfm_to_fm B))
[PROOF STEP]
by simp


[STATEMENT]
lemma closed_hfm_Conj[simp]:
  "closed_hfm (HConj A B) \<longleftrightarrow> closed_hfm A \<and> closed_hfm B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_hfm (A HAND B) = (closed_hfm A \<and> closed_hfm B)
[PROOF STEP]
unfolding HConj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_hfm (HNeg (A HIMP HNeg B)) = (closed_hfm A \<and> closed_hfm B)
[PROOF STEP]
by simp


[STATEMENT]
lemma quot_closed_hfm[simp]: "closed_hfm A \<Longrightarrow> \<guillemotleft>A\<guillemotright> = \<guillemotleft>hfm_to_fm A\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_hfm A \<Longrightarrow> \<guillemotleft>A\<guillemotright> = \<guillemotleft>hfm_to_fm A\<guillemotright>
[PROOF STEP]
by (induction A) (auto simp add: quot_fm_def)


[STATEMENT]
lemma P': "{} \<turnstile> P IFF H(X0 ::= \<guillemotleft>P\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)
[PROOF STEP]
from diagonal[where \<alpha> = "H" and i = X0]
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<delta>. \<lbrakk>{} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>); supp \<delta> = supp local.H - {atom X0}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<delta> where "{} \<turnstile> \<delta> IFF H(X0 ::= \<guillemotleft>\<delta>\<guillemotright>)"
[PROOF STATE]
proof (prove)
using this:
(\<And>\<delta>. \<lbrakk>{} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>); supp \<delta> = supp local.H - {atom X0}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<delta>. {} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>)

goal (1 subgoal):
 1. {} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>)

goal (1 subgoal):
 1. {} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> \<delta> IFF local.H(X0::=\<guillemotleft>\<delta>\<guillemotright>)

goal (1 subgoal):
 1. {} \<turnstile> (SOME P. {} \<turnstile> P IFF local.H(X0::=\<guillemotleft>P\<guillemotright>)) IFF local.H(X0::=\<guillemotleft>SOME P. {} \<turnstile> P IFF local.H(X0::=\<guillemotleft>P\<guillemotright>)\<guillemotright>)
[PROOF STEP]
by (rule someI)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma 7: "{} \<turnstile> P IFF
     (Q\<^sub>1 AND Neg (PfP \<guillemotleft>P IMP Q\<^sub>1\<guillemotright>) XOR
      Q\<^sub>2 AND Neg (PfP \<guillemotleft>P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> local.P IFF (Q\<^sub>1 AND Neg (PfP \<guillemotleft>local.P IMP Q\<^sub>1\<guillemotright>) XOR Q\<^sub>2 AND Neg (PfP \<guillemotleft>local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>))
[PROOF STEP]
using P'
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> local.P IFF local.H(X0::=\<guillemotleft>local.P\<guillemotright>)

goal (1 subgoal):
 1. {} \<turnstile> local.P IFF (Q\<^sub>1 AND Neg (PfP \<guillemotleft>local.P IMP Q\<^sub>1\<guillemotright>) XOR Q\<^sub>2 AND Neg (PfP \<guillemotleft>local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>))
[PROOF STEP]
unfolding H_def
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> local.P IFF (Q\<^sub>1 AND Neg (PfP \<guillemotleft>HVar X0 HIMP HFm Q\<^sub>1\<guillemotright>) XOR Q\<^sub>2 AND Neg (PfP \<guillemotleft>HVar X0 HAND HNeg (HFm Q\<^sub>1) HIMP HFm Q\<^sub>2\<guillemotright>))(X0::=\<guillemotleft>local.P\<guillemotright>)

goal (1 subgoal):
 1. {} \<turnstile> local.P IFF (Q\<^sub>1 AND Neg (PfP \<guillemotleft>local.P IMP Q\<^sub>1\<guillemotright>) XOR Q\<^sub>2 AND Neg (PfP \<guillemotleft>local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>))
[PROOF STEP]
by (simp add: Q_closed forget_subst_fm[unfolded fresh_def])


[STATEMENT]
lemma 8: "{} \<turnstile> (P AND Neg Q\<^sub>1) IMP Q\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2
[PROOF STEP]
by (intro propositional_calculus "7_E")


[STATEMENT]
lemma 10: "{} \<turnstile> PfP \<guillemotleft>(P AND Neg Q\<^sub>1) IMP Q\<^sub>2\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>
[PROOF STEP]
using 8
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2

goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>local.P AND Neg Q\<^sub>1 IMP Q\<^sub>2\<guillemotright>
[PROOF STEP]
by (rule proved_imp_proved_PfP)


[STATEMENT]
lemma 11: "{} \<turnstile> P IMP Q\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> local.P IMP Q\<^sub>1
[PROOF STEP]
by (intro propositional_calculus "7_E" "10_I")


[STATEMENT]
lemma 12: "{} \<turnstile> PfP \<guillemotleft>P IMP Q\<^sub>1\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>local.P IMP Q\<^sub>1\<guillemotright>
[PROOF STEP]
using 11
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> local.P IMP Q\<^sub>1

goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>local.P IMP Q\<^sub>1\<guillemotright>
[PROOF STEP]
by (rule proved_imp_proved_PfP)


[STATEMENT]
lemma 13: "{} \<turnstile> Neg P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Neg local.P
[PROOF STEP]
by (intro propositional_calculus "7_E" "10_I" "12_I")


[STATEMENT]
lemma trans_tm_forgets: "atom ` set is \<sharp>* t \<Longrightarrow> trans_tm is t = trans_tm [] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` set is \<sharp>* t \<Longrightarrow> trans_tm is t = trans_tm [] t
[PROOF STEP]
by (induct t rule: tm.induct)
     (auto simp: lookup_notin fresh_star_def fresh_at_base)


[STATEMENT]
lemma vquot_dbtm_fresh: "atom ` V \<sharp>* t \<Longrightarrow> vquot_dbtm V t = quot_dbtm t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` V \<sharp>* t \<Longrightarrow> vquot_dbtm V t = quot_dbtm t
[PROOF STEP]
by (nominal_induct t rule: dbtm.strong_induct)
     (auto simp add: fresh_star_def fresh_at_base)


[STATEMENT]
lemma subst_vquot_dbtm_trans_tm[simp]:
  "atom i \<sharp> is \<Longrightarrow> atom ` set is \<sharp>* t \<Longrightarrow>
   subst i \<guillemotleft>t\<guillemotright> (vquot_dbtm {i} (trans_tm is t')) =
   quot_dbtm (trans_tm is (subst i t t'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> is; atom ` set is \<sharp>* t\<rbrakk> \<Longrightarrow> subst i \<guillemotleft>t\<guillemotright> (vquot_dbtm {i} (trans_tm is t')) = quot_dbtm (trans_tm is (subst i t t'))
[PROOF STEP]
by (nominal_induct t' avoiding: "is" i t rule: tm.strong_induct)
     (auto simp add:  quot_tm_def lookup_notin fresh_imp_notin_env
                      vquot_dbtm_fresh lookup_fresh
           intro: trans_tm_forgets[symmetric])


[STATEMENT]
lemma subst_vquot_dbtm_trans_fm[simp]:
  "atom i \<sharp> is \<Longrightarrow> atom ` set is \<sharp>* t \<Longrightarrow>
   subst i \<guillemotleft>t\<guillemotright> (vquot_dbfm {i} (trans_fm is A)) =
   quot_dbfm (trans_fm is (subst_fm A i t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> is; atom ` set is \<sharp>* t\<rbrakk> \<Longrightarrow> subst i \<guillemotleft>t\<guillemotright> (vquot_dbfm {i} (trans_fm is A)) = quot_dbfm (trans_fm is (A(i::=t)))
[PROOF STEP]
by (nominal_induct A avoiding: "is" i t rule: fm.strong_induct)
     (auto simp add: quot_fm_def fresh_Cons)


[STATEMENT]
lemma subst_vquot[simp]:
  "subst i \<guillemotleft>t\<guillemotright> \<lfloor>A\<rfloor>{i} = \<guillemotleft>A(i ::= t)\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst i \<guillemotleft>t\<guillemotright> \<lfloor>A\<rfloor>{i} = \<guillemotleft>A(i::=t)\<guillemotright>
[PROOF STEP]
by (nominal_induct A avoiding: i t rule: fm.strong_induct)
     (auto simp add: vquot_fm_def quot_fm_def fresh_Cons)


[STATEMENT]
lemma rmshadow_sound:
    "p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p
[PROOF STEP]
proof(induction rs arbitrary: P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow [] P) p = simple_fw [] p
 2. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p \<in> P

goal (2 subgoals):
 1. \<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow [] P) p = simple_fw [] p
 2. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> P

goal (1 subgoal):
 1. simple_fw (rmshadow [] P) p = simple_fw [] p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow [] P) p = simple_fw [] p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
p \<in> ?P \<Longrightarrow> simple_fw (rmshadow rs ?P) p = simple_fw rs p
p \<in> P

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.IH Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<in> ?P \<Longrightarrow> simple_fw (rmshadow rs ?P) p = simple_fw rs p
p \<in> P
[PROOF STEP]
have IH1: "simple_fw (rmshadow rs P) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
using this:
p \<in> ?P \<Longrightarrow> simple_fw (rmshadow rs ?P) p = simple_fw rs p
p \<in> P

goal (1 subgoal):
 1. simple_fw (rmshadow rs P) p = simple_fw rs p
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow rs P) p = simple_fw rs p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
let ?P'="{p \<in> P. \<not> simple_matches (match_sel r) p}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.IH Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<in> ?P \<Longrightarrow> simple_fw (rmshadow rs ?P) p = simple_fw rs p
p \<in> P
[PROOF STEP]
have IH2: "\<And>m. p \<in> ?P' \<Longrightarrow> simple_fw (rmshadow rs ?P') p = simple_fw rs p"
[PROOF STATE]
proof (prove)
using this:
p \<in> ?P \<Longrightarrow> simple_fw (rmshadow rs ?P) p = simple_fw rs p
p \<in> P

goal (1 subgoal):
 1. \<And>m. p \<in> {p \<in> P. \<not> simple_matches (match_sel r) p} \<Longrightarrow> simple_fw (rmshadow rs {p \<in> P. \<not> simple_matches (match_sel r) p}) p = simple_fw rs p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<in> {p \<in> P. \<not> simple_matches (match_sel r) p} \<Longrightarrow> simple_fw (rmshadow rs {p \<in> P. \<not> simple_matches (match_sel r) p}) p = simple_fw rs p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<in> P \<Longrightarrow> simple_fw (rmshadow rs P) p = simple_fw rs p; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<in> P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> P

goal (1 subgoal):
 1. simple_fw (rmshadow (r # rs) P) p = simple_fw (r # rs) p
[PROOF STEP]
apply(cases r, rename_tac m a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>p \<in> P; r = SimpleRule m a; p \<in> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow (r # rs) P) p = simple_fw (r # rs) p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(case_tac "\<forall>p\<in>P. \<not> simple_matches m p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<forall>p\<in>P. \<not> simple_matches m p\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p)\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp add: IH1 nomatch)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p)\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(case_tac "p \<in> ?P'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p); p \<in> {p \<in> P. \<not> simple_matches (match_sel r) p}\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p); p \<notin> {p \<in> P. \<not> simple_matches (match_sel r) p}\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(frule IH2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p); p \<in> {p \<in> P. \<not> simple_matches (match_sel r) p}; simple_fw (rmshadow rs {p \<in> P. \<not> simple_matches (match_sel r) p}) p = simple_fw rs p\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p); p \<notin> {p \<in> P. \<not> simple_matches (match_sel r) p}\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp add: nomatch IH1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<not> (\<forall>p\<in>P. \<not> simple_matches m p); p \<notin> {p \<in> P. \<not> simple_matches (match_sel r) p}\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> ((\<exists>p\<in>P. simple_matches m p) \<longrightarrow> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<exists>p\<in>P. simple_matches m p; simple_matches m p\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<exists>p\<in>P. simple_matches m p; simple_matches m p; a = Accept\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<in> P; \<exists>p\<in>P. simple_matches m p; simple_matches m p; a = Drop\<rbrakk> \<Longrightarrow> ((\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> simple_fw (SimpleRule m a # rmshadow rs {p \<in> P. \<not> simple_matches m p}) p = simple_fw (SimpleRule m a # rs) p
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m Accept; p \<in> P; \<exists>p\<in>P. simple_matches m p; simple_matches m p; a = Accept\<rbrakk> \<Longrightarrow> (\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = Decision FinalAllow
 2. \<And>m a. \<lbrakk>r = SimpleRule m Drop; p \<in> P; \<exists>p\<in>P. simple_matches m p; simple_matches m p; a = Drop\<rbrakk> \<Longrightarrow> (\<forall>p\<in>P. \<not> simple_matches m p) \<longrightarrow> simple_fw (rmshadow rs P) p = Decision FinalDeny
[PROOF STEP]
by fast+
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow (r # rs) P) p = simple_fw (r # rs) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rmshadow'_sound:
    "p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p
[PROOF STEP]
proof(induction rs arbitrary: P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' [] P) p = simple_fw [] p
 2. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p \<notin> P

goal (2 subgoals):
 1. \<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' [] P) p = simple_fw [] p
 2. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p \<notin> P

goal (1 subgoal):
 1. simple_fw (rmshadow' [] P) p = simple_fw [] p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow' [] P) p = simple_fw [] p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
p \<notin> ?P \<Longrightarrow> simple_fw (rmshadow' rs ?P) p = simple_fw rs p
p \<notin> P

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.IH Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<notin> ?P \<Longrightarrow> simple_fw (rmshadow' rs ?P) p = simple_fw rs p
p \<notin> P
[PROOF STEP]
have IH1: "simple_fw (rmshadow' rs P) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
using this:
p \<notin> ?P \<Longrightarrow> simple_fw (rmshadow' rs ?P) p = simple_fw rs p
p \<notin> P

goal (1 subgoal):
 1. simple_fw (rmshadow' rs P) p = simple_fw rs p
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow' rs P) p = simple_fw rs p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
let ?P'="{p. simple_matches (match_sel r) p}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.IH Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<notin> ?P \<Longrightarrow> simple_fw (rmshadow' rs ?P) p = simple_fw rs p
p \<notin> P
[PROOF STEP]
have IH2: "\<And>m. p \<notin> (Collect (simple_matches m)) \<Longrightarrow> simple_fw (rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw rs p"
[PROOF STATE]
proof (prove)
using this:
p \<notin> ?P \<Longrightarrow> simple_fw (rmshadow' rs ?P) p = simple_fw rs p
p \<notin> P

goal (1 subgoal):
 1. \<And>m. p \<notin> Collect (simple_matches m) \<Longrightarrow> simple_fw (rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw rs p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<notin> Collect (simple_matches ?m1) \<Longrightarrow> simple_fw (rmshadow' rs (P \<union> Collect (simple_matches ?m1))) p = simple_fw rs p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
have nomatch_m: "\<And>m. p \<notin> P \<Longrightarrow> {p. simple_matches m p} \<subseteq> P \<Longrightarrow> \<not> simple_matches m p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>p \<notin> P; {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> \<not> simple_matches m p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>p \<notin> P; {p. simple_matches ?m1 p} \<subseteq> P\<rbrakk> \<Longrightarrow> \<not> simple_matches ?m1 p

goal (1 subgoal):
 1. \<And>a rs P. \<lbrakk>\<And>P. p \<notin> P \<Longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw rs p; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (a # rs) P) p = simple_fw (a # rs) p
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
p \<notin> P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<notin> P

goal (1 subgoal):
 1. simple_fw (rmshadow' (r # rs) P) p = simple_fw (r # rs) p
[PROOF STEP]
apply(cases r, rename_tac m a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>p \<notin> P; r = SimpleRule m a; p \<notin> P\<rbrakk> \<Longrightarrow> simple_fw (rmshadow' (r # rs) P) p = simple_fw (r # rs) p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(case_tac "{p. simple_matches m p} \<subseteq> P")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp add: IH1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> simple_fw rs p = simple_fw (SimpleRule m a # rs) p
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(drule nomatch_m)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> {p. simple_matches (?m8 m a) p} \<subseteq> P
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; {p. simple_matches m p} \<subseteq> P; \<not> simple_matches (?m8 m a) p\<rbrakk> \<Longrightarrow> simple_fw rs p = simple_fw (SimpleRule m a # rs) p
 3. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; {p. simple_matches m p} \<subseteq> P; \<not> simple_matches m p\<rbrakk> \<Longrightarrow> simple_fw rs p = simple_fw (SimpleRule m a # rs) p
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp add: nomatch)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> (Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (rmshadow' rs P) p = simple_fw (SimpleRule m a # rs) p) \<and> (\<not> Collect (simple_matches m) \<subseteq> P \<longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P; a = Accept\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p
 2. \<And>m a. \<lbrakk>r = SimpleRule m a; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P; a = Drop\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw (SimpleRule m a # rs) p
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>r = SimpleRule m Accept; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P; a = Accept\<rbrakk> \<Longrightarrow> \<not> simple_matches m p \<longrightarrow> simple_fw (rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw rs p
 2. \<And>m a. \<lbrakk>r = SimpleRule m Drop; p \<notin> P; \<not> {p. simple_matches m p} \<subseteq> P; a = Drop\<rbrakk> \<Longrightarrow> \<not> simple_matches m p \<longrightarrow> simple_fw (rmshadow' rs (P \<union> Collect (simple_matches m))) p = simple_fw rs p
[PROOF STEP]
apply(simp_all add: IH2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
simple_fw (rmshadow' (r # rs) P) p = simple_fw (r # rs) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simple_packet_set_toSet_alt: "simple_packet_set_toSet ms = (\<Union> m \<in> set ms. {p. simple_matches m p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_packet_set_toSet ms = (\<Union>m\<in>set ms. {p. simple_matches m p})
[PROOF STEP]
unfolding simple_packet_set_toSet_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. \<exists>m\<in>set ms. simple_matches m p} = (\<Union>m\<in>set ms. {p. simple_matches m p})
[PROOF STEP]
by blast


[STATEMENT]
lemma "simple_packet_set_toSet (simple_packet_set_union ps m) = simple_packet_set_toSet ps \<union> {p. simple_matches m p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_packet_set_toSet (simple_packet_set_union ps m) = simple_packet_set_toSet ps \<union> {p. simple_matches m p}
[PROOF STEP]
unfolding simple_packet_set_toSet_def simple_packet_set_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. \<exists>m\<in>set (m # ps). simple_matches m p} = {p. \<exists>m\<in>set ps. simple_matches m p} \<union> {p. simple_matches m p}
[PROOF STEP]
by simp blast


[STATEMENT]
lemma "(\<exists>m' \<in> set ms.
        {i. match_iface iif i} \<subseteq> {i. match_iface (iiface m') i} \<and>
        {i. match_iface oif i} \<subseteq> {i. match_iface (oiface m') i} \<and>
        {ip. simple_match_ip sip ip} \<subseteq> {ip. simple_match_ip (src m') ip} \<and>
        {ip. simple_match_ip dip ip} \<subseteq> {ip. simple_match_ip (dst m') ip} \<and>
        {p. match_proto protocol p} \<subseteq> {p. match_proto (proto m') p} \<and>
        {p. simple_match_port sps p} \<subseteq> {p. simple_match_port (sports m') p} \<and>
        {p. simple_match_port dps p} \<subseteq> {p. simple_match_port (dports m') p}
      )
    \<Longrightarrow> {p. simple_matches \<lparr>iiface=iif, oiface=oif, src=sip, dst=dip, proto=protocol, sports=sps, dports=dps \<rparr> p} \<subseteq> (simple_packet_set_toSet ms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m'\<in>set ms. {i. match_iface iif i} \<subseteq> {i. match_iface (iiface m') i} \<and> {i. match_iface oif i} \<subseteq> {i. match_iface (oiface m') i} \<and> {ip. simple_match_ip sip ip} \<subseteq> {ip. simple_match_ip (src m') ip} \<and> {ip. simple_match_ip dip ip} \<subseteq> {ip. simple_match_ip (dst m') ip} \<and> {p. match_proto protocol p} \<subseteq> {p. match_proto (proto m') p} \<and> {p. simple_match_port sps p} \<subseteq> {p. simple_match_port (sports m') p} \<and> {p. simple_match_port dps p} \<subseteq> {p. simple_match_port (dports m') p} \<Longrightarrow> {p. simple_matches \<lparr>iiface = iif, oiface = oif, src = sip, dst = dip, proto = protocol, sports = sps, dports = dps\<rparr> p} \<subseteq> simple_packet_set_toSet ms
[PROOF STEP]
unfolding simple_packet_set_toSet_def simple_packet_set_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m'\<in>set ms. {i. match_iface iif i} \<subseteq> {i. match_iface (iiface m') i} \<and> {i. match_iface oif i} \<subseteq> {i. match_iface (oiface m') i} \<and> {ip. simple_match_ip sip ip} \<subseteq> {ip. simple_match_ip (src m') ip} \<and> {ip. simple_match_ip dip ip} \<subseteq> {ip. simple_match_ip (dst m') ip} \<and> {p. match_proto protocol p} \<subseteq> {p. match_proto (proto m') p} \<and> {p. simple_match_port sps p} \<subseteq> {p. simple_match_port (sports m') p} \<and> {p. simple_match_port dps p} \<subseteq> {p. simple_match_port (dports m') p} \<Longrightarrow> {p. simple_matches \<lparr>iiface = iif, oiface = oif, src = sip, dst = dip, proto = protocol, sports = sps, dports = dps\<rparr> p} \<subseteq> {p. \<exists>m\<in>set ms. simple_matches m p}
[PROOF STEP]
apply(simp add: simple_matches.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m'\<in>set ms. {i. match_iface iif i} \<subseteq> {i. match_iface (iiface m') i} \<and> {i. match_iface oif i} \<subseteq> {i. match_iface (oiface m') i} \<and> {ip. simple_match_ip sip ip} \<subseteq> {ip. simple_match_ip (src m') ip} \<and> {ip. simple_match_ip dip ip} \<subseteq> {ip. simple_match_ip (dst m') ip} \<and> {p. match_proto protocol p} \<subseteq> {p. match_proto (proto m') p} \<and> {p. simple_match_port sps p} \<subseteq> {p. simple_match_port (sports m') p} \<and> {p. simple_match_port dps p} \<subseteq> {p. simple_match_port (dports m') p} \<Longrightarrow> {p. match_iface iif (p_iiface p) \<and> match_iface oif (p_oiface p) \<and> simple_match_ip sip (p_src p) \<and> simple_match_ip dip (p_dst p) \<and> match_proto protocol (p_proto p) \<and> simple_match_port sps (p_sport p) \<and> simple_match_port dps (p_dport p)} \<subseteq> {p. \<exists>m\<in>set ms. match_iface (iiface m) (p_iiface p) \<and> match_iface (oiface m) (p_oiface p) \<and> simple_match_ip (src m) (p_src p) \<and> simple_match_ip (dst m) (p_dst p) \<and> match_proto (proto m) (p_proto p) \<and> simple_match_port (sports m) (p_sport p) \<and> simple_match_port (dports m) (p_dport p)}
[PROOF STEP]
apply(simp add: Set.Collect_mono_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m'\<in>set ms. (\<forall>x. match_iface iif x \<longrightarrow> match_iface (iiface m') x) \<and> (\<forall>x. match_iface oif x \<longrightarrow> match_iface (oiface m') x) \<and> (\<forall>x. simple_match_ip sip x \<longrightarrow> simple_match_ip (src m') x) \<and> (\<forall>x. simple_match_ip dip x \<longrightarrow> simple_match_ip (dst m') x) \<and> (\<forall>x. match_proto protocol x \<longrightarrow> match_proto (proto m') x) \<and> (\<forall>x. simple_match_port sps x \<longrightarrow> simple_match_port (sports m') x) \<and> (\<forall>x. simple_match_port dps x \<longrightarrow> simple_match_port (dports m') x) \<Longrightarrow> \<forall>x. match_iface iif (p_iiface x) \<and> match_iface oif (p_oiface x) \<and> simple_match_ip sip (p_src x) \<and> simple_match_ip dip (p_dst x) \<and> match_proto protocol (p_proto x) \<and> simple_match_port sps (p_sport x) \<and> simple_match_port dps (p_dport x) \<longrightarrow> (\<exists>m\<in>set ms. match_iface (iiface m) (p_iiface x) \<and> match_iface (oiface m) (p_oiface x) \<and> simple_match_ip (src m) (p_src x) \<and> simple_match_ip (dst m) (p_dst x) \<and> match_proto (proto m) (p_proto x) \<and> simple_match_port (sports m) (p_sport x) \<and> simple_match_port (dports m) (p_dport x))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' x. \<lbrakk>m' \<in> set ms; \<forall>x. match_iface iif x \<longrightarrow> match_iface (iiface m') x; \<forall>x. match_iface oif x \<longrightarrow> match_iface (oiface m') x; \<forall>x. simple_match_ip sip x \<longrightarrow> simple_match_ip (src m') x; \<forall>x. simple_match_ip dip x \<longrightarrow> simple_match_ip (dst m') x; \<forall>x. match_proto protocol x \<longrightarrow> match_proto (proto m') x; \<forall>x. simple_match_port sps x \<longrightarrow> simple_match_port (sports m') x; \<forall>x. simple_match_port dps x \<longrightarrow> simple_match_port (dports m') x; match_iface iif (p_iiface x); match_iface oif (p_oiface x); simple_match_ip sip (p_src x); simple_match_ip dip (p_dst x); match_proto protocol (p_proto x); simple_match_port sps (p_sport x); simple_match_port dps (p_dport x)\<rbrakk> \<Longrightarrow> \<exists>m\<in>set ms. match_iface (iiface m) (p_iiface x) \<and> match_iface (oiface m) (p_oiface x) \<and> simple_match_ip (src m) (p_src x) \<and> simple_match_ip (dst m) (p_dst x) \<and> match_proto (proto m) (p_proto x) \<and> simple_match_port (sports m) (p_sport x) \<and> simple_match_port (dports m) (p_dport x)
[PROOF STEP]
apply meson
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "{p:: 'i::len simple_packet. simple_matches m p} \<subseteq> (simple_packet_set_toSet ms) \<longleftrightarrow>
      {p:: 'i::len simple_packet. simple_matches m p} \<inter> (\<Inter> m \<in> set ms. {p. \<not> simple_matches m p}) = {}" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
have "?l \<longleftrightarrow> {p. simple_matches m p} - (simple_packet_set_toSet ms) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} - simple_packet_set_toSet ms = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} - simple_packet_set_toSet ms = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} - simple_packet_set_toSet ms = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
have "\<dots> \<longleftrightarrow> {p. simple_matches m p} - (\<Union> m \<in> set ms. {p:: 'i::len simple_packet. simple_matches m p}) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({p. simple_matches m p} - simple_packet_set_toSet ms = {}) = ({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {})
[PROOF STEP]
using simple_packet_set_toSet_alt
[PROOF STATE]
proof (prove)
using this:
simple_packet_set_toSet ?ms = (\<Union>m\<in>set ?ms. {p. simple_matches m p})

goal (1 subgoal):
 1. ({p. simple_matches m p} - simple_packet_set_toSet ms = {}) = ({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} - simple_packet_set_toSet ms = {}) = ({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} - simple_packet_set_toSet ms = {}) = ({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {}) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} - (\<Union>m\<in>set ms. {p. simple_matches m p}) = {}) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})

goal (1 subgoal):
 1. ({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
({p. simple_matches m p} \<subseteq> simple_packet_set_toSet ms) = ({p. simple_matches m p} \<inter> (\<Inter>m\<in>set ms. {p. \<not> simple_matches m p}) = {})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma msg_sender_simps [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip.
                          msg_sender (Rreq hops rreqid dip dsn dsk oip osn sip) = sip"
  "\<And>hops dip dsn oip sip. msg_sender (Rrep hops dip dsn oip sip) = sip"
  "\<And>dests sip.            msg_sender (Rerr dests sip) = sip"
  "\<And>d dip sip.            msg_sender (Pkt d dip sip) = sip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. msg_sender (Rreq hops rreqid dip dsn dsk oip osn sip) = sip) &&& (\<And>hops dip dsn oip sip. msg_sender (Rrep hops dip dsn oip sip) = sip)) &&& (\<And>dests sip. msg_sender (Rerr dests sip) = sip) &&& (\<And>d dip sip. msg_sender (Pkt d dip sip) = sip)
[PROOF STEP]
unfolding msg_sender_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. (case Rreq hops rreqid dip dsn dsk oip osn sip of Rreq x xa xb xc xd xe xf ipc \<Rightarrow> ipc | Rrep x xa xb xc ipc \<Rightarrow> ipc | Rerr x ipc \<Rightarrow> ipc | Pkt x xa ipc \<Rightarrow> ipc) = sip) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rreq x xa xb xc xd xe xf ipc \<Rightarrow> ipc | Rrep x xa xb xc ipc \<Rightarrow> ipc | Rerr x ipc \<Rightarrow> ipc | Pkt x xa ipc \<Rightarrow> ipc) = sip)) &&& (\<And>dests sip. (case Rerr dests sip of Rreq x xa xb xc xd xe xf ipc \<Rightarrow> ipc | Rrep x xa xb xc ipc \<Rightarrow> ipc | Rerr x ipc \<Rightarrow> ipc | Pkt x xa ipc \<Rightarrow> ipc) = sip) &&& (\<And>d dip sip. (case Pkt d dip sip of Rreq x xa xb xc xd xe xf ipc \<Rightarrow> ipc | Rrep x xa xb xc ipc \<Rightarrow> ipc | Rerr x ipc \<Rightarrow> ipc | Pkt x xa ipc \<Rightarrow> ipc) = sip)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma msg_zhops_simps [simp]:
  "\<And>hops rreqid dip dsn dsk oip osn sip.
           msg_zhops (Rreq hops rreqid dip dsn dsk oip osn sip) = (hops = 0 \<longrightarrow> oip = sip)"
  "\<And>hops dip dsn oip sip. msg_zhops (Rrep hops dip dsn oip sip) = (hops = 0 \<longrightarrow> dip = sip)"
  "\<And>dests sip.            msg_zhops (Rerr dests sip)        = True"
  "\<And>d dip.                msg_zhops (Newpkt d dip)          = True"
  "\<And>d dip sip.            msg_zhops (Pkt d dip sip)         = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. msg_zhops (Rreq hops rreqid dip dsn dsk oip osn sip) = (hops = 0 \<longrightarrow> oip = sip)) &&& (\<And>hops dip dsn oip sip. msg_zhops (Rrep hops dip dsn oip sip) = (hops = 0 \<longrightarrow> dip = sip))) &&& (\<And>dests sip. msg_zhops (Rerr dests sip) = True) &&& (\<And>d dip. msg_zhops (Newpkt d dip) = True) &&& (\<And>d dip sip. msg_zhops (Pkt d dip sip) = True)
[PROOF STEP]
unfolding msg_zhops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>hops rreqid dip dsn dsk oip osn sip. (case Rreq hops rreqid dip dsn dsk oip osn sip of Rreq hopsc x dipc xa xb oipc xc sipc \<Rightarrow> hopsc = 0 \<longrightarrow> oipc = sipc | Rrep hopsc dipc x xa sipc \<Rightarrow> hopsc = 0 \<longrightarrow> dipc = sipc | _ \<Rightarrow> True) = (hops = 0 \<longrightarrow> oip = sip)) &&& (\<And>hops dip dsn oip sip. (case Rrep hops dip dsn oip sip of Rreq hopsc x dipc xa xb oipc xc sipc \<Rightarrow> hopsc = 0 \<longrightarrow> oipc = sipc | Rrep hopsc dipc x xa sipc \<Rightarrow> hopsc = 0 \<longrightarrow> dipc = sipc | _ \<Rightarrow> True) = (hops = 0 \<longrightarrow> dip = sip))) &&& (\<And>dests sip. (case Rerr dests sip of Rreq hopsc x dipc xa xb oipc xc sipc \<Rightarrow> hopsc = 0 \<longrightarrow> oipc = sipc | Rrep hopsc dipc x xa sipc \<Rightarrow> hopsc = 0 \<longrightarrow> dipc = sipc | _ \<Rightarrow> True) = True) &&& (\<And>d dip. (case Newpkt d dip of Rreq hopsc x dipc xa xb oipc xc sipc \<Rightarrow> hopsc = 0 \<longrightarrow> oipc = sipc | Rrep hopsc dipc x xa sipc \<Rightarrow> hopsc = 0 \<longrightarrow> dipc = sipc | _ \<Rightarrow> True) = True) &&& (\<And>d dip sip. (case Pkt d dip sip of Rreq hopsc x dipc xa xb oipc xc sipc \<Rightarrow> hopsc = 0 \<longrightarrow> oipc = sipc | Rrep hopsc dipc x xa sipc \<Rightarrow> hopsc = 0 \<longrightarrow> dipc = sipc | _ \<Rightarrow> True) = True)
[PROOF STEP]
by simp_all