[STATEMENT]
lemma conflictFlagOrQEmptyAfterExhaustiveUnitPropagate:
assumes
"exhaustiveUnitPropagate_dom state"
shows
"let state' = exhaustiveUnitPropagate state in
    (getConflictFlag state') \<or> (getQ state' = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate_dom state

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
proof (induct state rule: exhaustiveUnitPropagate_dom.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in getConflictFlag state' \<or> getQ state' = []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
case (step state')
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in getConflictFlag state' \<or> getQ state' = []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
note ih = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. \<And>state. \<lbrakk>\<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state); \<lbrakk>\<not> getConflictFlag state; getQ state \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state) in getConflictFlag state' \<or> getQ state' = []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate state in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
proof (cases "(getConflictFlag state') \<or> (getQ state') = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
getConflictFlag state' \<or> getQ state' = []

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
with exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (chain)
picking this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
have "exhaustiveUnitPropagate state' = state'"
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = state'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = state'

goal (2 subgoals):
 1. getConflictFlag state' \<or> getQ state' = [] \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
 2. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = state'

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = state'
getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
by (simp only: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
let ?state'' = "applyUnitPropagate state'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
have "exhaustiveUnitPropagate state' = exhaustiveUnitPropagate ?state''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using exhaustiveUnitPropagate.simps[of "state'"]
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = (if getConflictFlag state' \<or> getQ state' = [] then state' else exhaustiveUnitPropagate (applyUnitPropagate state'))
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')

goal (1 subgoal):
 1. \<not> (getConflictFlag state' \<or> getQ state' = []) \<Longrightarrow> let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in getConflictFlag state' \<or> getQ state' = []

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
exhaustiveUnitPropagate state' = exhaustiveUnitPropagate (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state')
\<lbrakk>\<not> getConflictFlag state'; getQ state' \<noteq> []\<rbrakk> \<Longrightarrow> let state' = exhaustiveUnitPropagate (applyUnitPropagate state') in getConflictFlag state' \<or> getQ state' = []
\<not> (getConflictFlag state' \<or> getQ state' = [])

goal (1 subgoal):
 1. let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
let state' = exhaustiveUnitPropagate state' in getConflictFlag state' \<or> getQ state' = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma perm_rel_lemma:
  assumes "\<And> \<pi> x y. r (\<pi> \<bullet> x) (\<pi> \<bullet> y) \<Longrightarrow> r x y"
  shows "r (\<pi> \<bullet> x) (\<pi> \<bullet> y) \<longleftrightarrow> r x y" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r (\<pi> \<bullet> x) (\<pi> \<bullet> y) = r x y
[PROOF STEP]
by (metis (full_types) assms permute_minus_cancel(2))


[STATEMENT]
lemma perm_rel_lemma2:
  assumes "\<And> \<pi> x y. r x y \<Longrightarrow> r (\<pi> \<bullet> x) (\<pi> \<bullet> y)"
  shows "r x y \<longleftrightarrow> r (\<pi> \<bullet> x) (\<pi> \<bullet> y)" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r x y = r (\<pi> \<bullet> x) (\<pi> \<bullet> y)
[PROOF STEP]
by (metis (full_types) assms permute_minus_cancel(2))


[STATEMENT]
lemma fun_eqvtI:
  assumes f_eqvt[eqvt]: "(\<And> p x. p \<bullet> (f x) = f (p \<bullet> x))"
  shows "p \<bullet> f = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> f = f
[PROOF STEP]
by perm_simp rule


[STATEMENT]
lemma eqvt_at_apply:
  assumes "eqvt_at f x"
  shows "(p \<bullet> f) x = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> f) x = f x
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))


[STATEMENT]
lemma eqvt_at_apply':
  assumes "eqvt_at f x"
  shows "p \<bullet> f x = f (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> f x = f (p \<bullet> x)
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms eqvt_at_def)


[STATEMENT]
lemma eqvt_at_apply'':
  assumes "eqvt_at f x"
  shows "(p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> f) (p \<bullet> x) = f (p \<bullet> x)
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))


[STATEMENT]
lemma size_list_eqvt[eqvt]: "p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x)
[PROOF STEP]
proof (induction x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
 2. \<And>a x. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x) \<Longrightarrow> p \<bullet> size_list f (a # x) = size_list (p \<bullet> f) (p \<bullet> (a # x))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
p \<bullet> size_list f xs = size_list (p \<bullet> f) (p \<bullet> xs)

goal (2 subgoals):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
 2. \<And>a x. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x) \<Longrightarrow> p \<bullet> size_list f (a # x) = size_list (p \<bullet> f) (p \<bullet> (a # x))
[PROOF STEP]
have "f x = p \<bullet> (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = p \<bullet> f x
[PROOF STEP]
by (simp add: permute_pure)
[PROOF STATE]
proof (state)
this:
f x = p \<bullet> f x

goal (2 subgoals):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
 2. \<And>a x. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x) \<Longrightarrow> p \<bullet> size_list f (a # x) = size_list (p \<bullet> f) (p \<bullet> (a # x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f x = p \<bullet> f x

goal (2 subgoals):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
 2. \<And>a x. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x) \<Longrightarrow> p \<bullet> size_list f (a # x) = size_list (p \<bullet> f) (p \<bullet> (a # x))
[PROOF STEP]
have "... = (p \<bullet> f) (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> f x = (p \<bullet> f) (p \<bullet> x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<bullet> f x = (p \<bullet> f) (p \<bullet> x)

goal (2 subgoals):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
 2. \<And>a x. p \<bullet> size_list f x = size_list (p \<bullet> f) (p \<bullet> x) \<Longrightarrow> p \<bullet> size_list f (a # x) = size_list (p \<bullet> f) (p \<bullet> (a # x))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> size_list f xs = size_list (p \<bullet> f) (p \<bullet> xs)
p \<bullet> f x = (p \<bullet> f) (p \<bullet> x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<bullet> size_list f xs = size_list (p \<bullet> f) (p \<bullet> xs)
p \<bullet> f x = (p \<bullet> f) (p \<bullet> x)

goal (1 subgoal):
 1. p \<bullet> size_list f (x # xs) = size_list (p \<bullet> f) (p \<bullet> (x # xs))
[PROOF STEP]
by (auto simp add: permute_pure)
[PROOF STATE]
proof (state)
this:
p \<bullet> size_list f (x # xs) = size_list (p \<bullet> f) (p \<bullet> (x # xs))

goal (1 subgoal):
 1. p \<bullet> size_list f [] = size_list (p \<bullet> f) (p \<bullet> [])
[PROOF STEP]
qed simp


[STATEMENT]
lemma eqvt_fresh_cong1: "(\<And>p x. p \<bullet> (f x) = f (p \<bullet> x)) \<Longrightarrow> a \<sharp> x \<Longrightarrow> a \<sharp> f x "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> f x
[PROOF STEP]
apply (rule fresh_fun_eqvt_app[of f])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> eqvt f
 2. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> x
[PROOF STEP]
apply (rule eqvtI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> p \<bullet> f \<equiv> f
 2. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> x
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> p \<bullet> f = f
 2. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> x
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p xa. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> (p \<bullet> f) xa = f xa
 2. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> x
[PROOF STEP]
apply (metis permute_fun_def permute_minus_cancel(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p x. p \<bullet> f x = f (p \<bullet> x); a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eqvt_fresh_cong2:
  assumes eqvt: "(\<And>p x y. p \<bullet> (f x y) = f (p \<bullet> x) (p \<bullet> y))"
  and fresh1: "a \<sharp> x" and fresh2: "a \<sharp> y"
  shows "a \<sharp> f x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
have "eqvt (\<lambda> (x,y). f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (\<lambda>(x, y). f x y)
[PROOF STEP]
using eqvt
[PROOF STATE]
proof (prove)
using this:
?p \<bullet> f ?x ?y = f (?p \<bullet> ?x) (?p \<bullet> ?y)

goal (1 subgoal):
 1. eqvt (\<lambda>(x, y). f x y)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p x y. p \<bullet> f x y = f (p \<bullet> x) (p \<bullet> y)) \<Longrightarrow> eqvt (\<lambda>(x, y). f x y)
[PROOF STEP]
apply (auto simp add: eqvt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. (\<And>p x y. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) = f (p \<bullet> x) (p \<bullet> y)) \<Longrightarrow> (\<lambda>(x, y). (p \<bullet> f) x y) = (\<lambda>(x, y). f x y)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p x. (\<And>p x y. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) = f (p \<bullet> x) (p \<bullet> y)) \<Longrightarrow> (case x of (x, xa) \<Rightarrow> (p \<bullet> f) x xa) = (case x of (x, xa) \<Rightarrow> f x xa)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p a b. (\<And>p x y. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) = f (p \<bullet> x) (p \<bullet> y)) \<Longrightarrow> (p \<bullet> f) a b = f a b
[PROOF STEP]
by (metis permute_minus_cancel(1))
[PROOF STATE]
proof (state)
this:
eqvt (\<lambda>(x, y). f x y)

goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt (\<lambda>(x, y). f x y)

goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
have "a \<sharp> (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> (x, y)
[PROOF STEP]
using fresh1 fresh2
[PROOF STATE]
proof (prove)
using this:
a \<sharp> x
a \<sharp> y

goal (1 subgoal):
 1. a \<sharp> (x, y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<sharp> (x, y)

goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eqvt (\<lambda>(x, y). f x y)
a \<sharp> (x, y)
[PROOF STEP]
have "a \<sharp> (\<lambda> (x,y). f x y) (x, y)"
[PROOF STATE]
proof (prove)
using this:
eqvt (\<lambda>(x, y). f x y)
a \<sharp> (x, y)

goal (1 subgoal):
 1. a \<sharp> (case (x, y) of (x, y) \<Rightarrow> f x y)
[PROOF STEP]
by (rule fresh_fun_eqvt_app)
[PROOF STATE]
proof (state)
this:
a \<sharp> (case (x, y) of (x, y) \<Rightarrow> f x y)

goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<sharp> (case (x, y) of (x, y) \<Rightarrow> f x y)

goal (1 subgoal):
 1. a \<sharp> f x y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sharp> f x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvt_fresh_star_cong1:
  assumes eqvt: "(\<And>p x. p \<bullet> (f x) = f (p \<bullet> x))"
  and fresh1: "a \<sharp>* x"
  shows "a \<sharp>* f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* f x
[PROOF STEP]
by (metis fresh_star_def eqvt_fresh_cong1 assms)


[STATEMENT]
lemma eqvt_fresh_star_cong2:
  assumes eqvt: "(\<And>p x y. p \<bullet> (f x y) = f (p \<bullet> x) (p \<bullet> y))"
  and fresh1: "a \<sharp>* x" and fresh2: "a \<sharp>* y"
  shows "a \<sharp>* f x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* f x y
[PROOF STEP]
by (metis fresh_star_def eqvt_fresh_cong2 assms)


[STATEMENT]
lemma eqvt_fresh_cong3:
  assumes eqvt: "(\<And>p x y z. p \<bullet> (f x y z) = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z))"
  and fresh1: "a \<sharp> x" and fresh2: "a \<sharp> y" and fresh3: "a \<sharp> z"
  shows "a \<sharp> f x y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
have "eqvt (\<lambda> (x,y,z). f x y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (\<lambda>(x, y, z). f x y z)
[PROOF STEP]
using eqvt
[PROOF STATE]
proof (prove)
using this:
?p \<bullet> f ?x ?y ?z = f (?p \<bullet> ?x) (?p \<bullet> ?y) (?p \<bullet> ?z)

goal (1 subgoal):
 1. eqvt (\<lambda>(x, y, z). f x y z)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p x y z. p \<bullet> f x y z = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)) \<Longrightarrow> eqvt (\<lambda>(x, y, z). f x y z)
[PROOF STEP]
apply (auto simp add: eqvt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. (\<And>p x y z. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) (p \<bullet> z) = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)) \<Longrightarrow> (\<lambda>(x, xa, y). (p \<bullet> f) x xa y) = (\<lambda>(x, xa, y). f x xa y)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p x. (\<And>p x y z. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) (p \<bullet> z) = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)) \<Longrightarrow> (case x of (x, xb, xc) \<Rightarrow> (p \<bullet> f) x xb xc) = (case x of (x, xb, xc) \<Rightarrow> f x xb xc)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p a aa b. (\<And>p x y z. (p \<bullet> f) (p \<bullet> x) (p \<bullet> y) (p \<bullet> z) = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)) \<Longrightarrow> (p \<bullet> f) a aa b = f a aa b
[PROOF STEP]
by (metis permute_minus_cancel(1))
[PROOF STATE]
proof (state)
this:
eqvt (\<lambda>(x, y, z). f x y z)

goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt (\<lambda>(x, y, z). f x y z)

goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
have "a \<sharp> (x, y, z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> (x, y, z)
[PROOF STEP]
using fresh1 fresh2 fresh3
[PROOF STATE]
proof (prove)
using this:
a \<sharp> x
a \<sharp> y
a \<sharp> z

goal (1 subgoal):
 1. a \<sharp> (x, y, z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<sharp> (x, y, z)

goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eqvt (\<lambda>(x, y, z). f x y z)
a \<sharp> (x, y, z)
[PROOF STEP]
have "a \<sharp> (\<lambda> (x,y,z). f x y z) (x, y, z)"
[PROOF STATE]
proof (prove)
using this:
eqvt (\<lambda>(x, y, z). f x y z)
a \<sharp> (x, y, z)

goal (1 subgoal):
 1. a \<sharp> (case (x, y, z) of (x, y, z) \<Rightarrow> f x y z)
[PROOF STEP]
by (rule fresh_fun_eqvt_app)
[PROOF STATE]
proof (state)
this:
a \<sharp> (case (x, y, z) of (x, y, z) \<Rightarrow> f x y z)

goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<sharp> (case (x, y, z) of (x, y, z) \<Rightarrow> f x y z)

goal (1 subgoal):
 1. a \<sharp> f x y z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sharp> f x y z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvt_fresh_star_cong3:
  assumes eqvt: "(\<And>p x y z. p \<bullet> (f x y z) = f (p \<bullet> x) (p \<bullet> y) (p \<bullet> z))"
  and fresh1: "a \<sharp>* x" and fresh2: "a \<sharp>* y" and fresh3: "a \<sharp>* z"
  shows "a \<sharp>* f x y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* f x y z
[PROOF STEP]
by (metis fresh_star_def eqvt_fresh_cong3 assms)


[STATEMENT]
lemma not_self_fresh[simp]: "atom x \<sharp> x \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> x = False
[PROOF STEP]
by (metis fresh_at_base(2))


[STATEMENT]
lemma fresh_star_singleton: "{ x } \<sharp>* e \<longleftrightarrow> x \<sharp> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} \<sharp>* e = x \<sharp> e
[PROOF STEP]
by (simp add: fresh_star_def)


[STATEMENT]
lemma eqvt_cases:
  fixes f x \<pi>
  assumes eqvt: "\<And>x. \<pi> \<bullet> f x = f (\<pi> \<bullet> x)"
  obtains "f x" "f (\<pi> \<bullet> x)" | "\<not> f x " " \<not> f (\<pi> \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>f x; f (\<pi> \<bullet> x)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> f x; \<not> f (\<pi> \<bullet> x)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms[symmetric]
[PROOF STATE]
proof (prove)
using this:
f (\<pi> \<bullet> ?x) = \<pi> \<bullet> f ?x

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>f x; f (\<pi> \<bullet> x)\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> f x; \<not> f (\<pi> \<bullet> x)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases "f x") auto


[STATEMENT]
lemma range_eqvt: "\<pi> \<bullet> range Y = range (\<pi> \<bullet> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> range Y = range (\<pi> \<bullet> Y)
[PROOF STEP]
unfolding image_eqvt UNIV_eqvt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<pi> \<bullet> Y) = range (\<pi> \<bullet> Y)
[PROOF STEP]
..


[STATEMENT]
lemma case_option_eqvt[eqvt]:
  "\<pi> \<bullet> case_option d f x = case_option (\<pi> \<bullet> d) (\<pi> \<bullet> f) (\<pi> \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> (case x of None \<Rightarrow> d | Some x \<Rightarrow> f x) = (case \<pi> \<bullet> x of None \<Rightarrow> \<pi> \<bullet> d | Some x \<Rightarrow> (\<pi> \<bullet> f) x)
[PROOF STEP]
by(cases x)(simp_all)


[STATEMENT]
lemma supp_option_eqvt:
  "supp (case_option d f x) \<subseteq> supp d \<union> supp f \<union> supp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (case x of None \<Rightarrow> d | Some x \<Rightarrow> f x) \<subseteq> supp d \<union> supp f \<union> supp x
[PROOF STEP]
apply (cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x = None \<Longrightarrow> supp (case x of None \<Rightarrow> d | Some x \<Rightarrow> f x) \<subseteq> supp d \<union> supp f \<union> supp x
 2. \<And>a. x = Some a \<Longrightarrow> supp (case x of None \<Rightarrow> d | Some x \<Rightarrow> f x) \<subseteq> supp d \<union> supp f \<union> supp x
[PROOF STEP]
apply (auto simp add: supp_Some )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xa. \<lbrakk>x = Some a; xa \<in> supp (f a); xa \<notin> supp a; xa \<notin> supp f\<rbrakk> \<Longrightarrow> xa \<in> supp d
[PROOF STEP]
apply (metis (mono_tags) Un_iff subsetCE supp_fun_app)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma funpow_eqvt[simp,eqvt]:
  "\<pi> \<bullet> ((f :: 'a \<Rightarrow> 'a::pt) ^^ n) = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> f ^^ n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n)
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<pi> \<bullet> f ^^ 0 = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> 0)
 2. \<And>n. \<pi> \<bullet> f ^^ n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n) \<Longrightarrow> \<pi> \<bullet> f ^^ Suc n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<pi> \<bullet> f ^^ n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n) \<Longrightarrow> \<pi> \<bullet> f ^^ Suc n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> Suc n)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<pi> \<bullet> f ^^ n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n) \<Longrightarrow> (\<pi> \<bullet> f ^^ Suc n) x = ((\<pi> \<bullet> f) ^^ (\<pi> \<bullet> Suc n)) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. \<pi> \<bullet> f ^^ n = (\<pi> \<bullet> f) ^^ (\<pi> \<bullet> n) \<Longrightarrow> (\<pi> \<bullet> (\<lambda>a. f ((f ^^ n) a))) x = (\<pi> \<bullet> f) (((\<pi> \<bullet> f) ^^ n) x)
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x. (\<pi> \<bullet> compow) n (\<pi> \<bullet> f) = (\<pi> \<bullet> f) ^^ n \<Longrightarrow> (\<pi> \<bullet> f) ((\<pi> \<bullet> compow) n (\<pi> \<bullet> f) x) = (\<pi> \<bullet> f) (((\<pi> \<bullet> f) ^^ n) x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma delete_eqvt[eqvt]:
  "\<pi> \<bullet> AList.delete x \<Gamma> = AList.delete (\<pi> \<bullet> x) (\<pi> \<bullet> \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> AList.delete x \<Gamma> = AList.delete (\<pi> \<bullet> x) (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
by (induct \<Gamma>, auto)


[STATEMENT]
lemma restrict_eqvt[eqvt]:
  "\<pi> \<bullet> AList.restrict S \<Gamma> = AList.restrict (\<pi> \<bullet> S) (\<pi> \<bullet> \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> AList.restrict S \<Gamma> = AList.restrict (\<pi> \<bullet> S) (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
unfolding AList.restrict_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> filter (\<lambda>(k, v). k \<in> S) \<Gamma> = filter (\<lambda>(k, v). k \<in> \<pi> \<bullet> S) (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
by perm_simp rule


[STATEMENT]
lemma supp_restrict:
  "supp (AList.restrict S \<Gamma>) \<subseteq> supp \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (AList.restrict S \<Gamma>) \<subseteq> supp \<Gamma>
[PROOF STEP]
by (induction \<Gamma>) (auto simp add: supp_Pair supp_Cons)


[STATEMENT]
lemma clearjunk_eqvt[eqvt]:
  "\<pi> \<bullet> AList.clearjunk \<Gamma> = AList.clearjunk (\<pi> \<bullet> \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> AList.clearjunk \<Gamma> = AList.clearjunk (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
by (induction \<Gamma> rule: clearjunk.induct) auto


[STATEMENT]
lemma map_ran_eqvt[eqvt]:
  "\<pi> \<bullet> map_ran f \<Gamma> = map_ran (\<pi> \<bullet> f) (\<pi> \<bullet> \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> map_ran f \<Gamma> = map_ran (\<pi> \<bullet> f) (\<pi> \<bullet> \<Gamma>)
[PROOF STEP]
by (induct \<Gamma>, auto)


[STATEMENT]
lemma dom_perm:
  "dom (\<pi> \<bullet> f) = \<pi> \<bullet> (dom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<pi> \<bullet> f) = \<pi> \<bullet> dom f
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. (\<pi> \<bullet> f) a \<noteq> None} = \<pi> \<bullet> {a. f a \<noteq> None}
[PROOF STEP]
by (perm_simp) (simp)


[STATEMENT]
lemma ran_perm[simp]:
  "\<pi> \<bullet> (ran f) = ran (\<pi> \<bullet> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> ran f = ran (\<pi> \<bullet> f)
[PROOF STEP]
unfolding ran_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> {b. \<exists>a. f a = Some b} = {b. \<exists>a. (\<pi> \<bullet> f) a = Some b}
[PROOF STEP]
by (perm_simp) (simp)


[STATEMENT]
lemma map_add_eqvt[eqvt]:
  "\<pi> \<bullet> (m1 ++ m2) = (\<pi> \<bullet> m1) ++ (\<pi> \<bullet> m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> m1 ++ m2 = (\<pi> \<bullet> m1) ++ (\<pi> \<bullet> m2)
[PROOF STEP]
unfolding map_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some x \<Rightarrow> Some x) = (\<lambda>x. case (\<pi> \<bullet> m2) x of None \<Rightarrow> (\<pi> \<bullet> m1) x | Some x \<Rightarrow> Some x)
[PROOF STEP]
by (perm_simp, rule)


[STATEMENT]
lemma map_of_eqvt[eqvt]:
  "\<pi> \<bullet> map_of l = map_of (\<pi> \<bullet> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> map_of l = map_of (\<pi> \<bullet> l)
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<pi> \<bullet> map_of [] = map_of (\<pi> \<bullet> [])
 2. \<And>a l. \<pi> \<bullet> map_of l = map_of (\<pi> \<bullet> l) \<Longrightarrow> \<pi> \<bullet> map_of (a # l) = map_of (\<pi> \<bullet> (a # l))
[PROOF STEP]
apply (simp add: permute_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<pi> \<bullet> map_of l = map_of (\<pi> \<bullet> l) \<Longrightarrow> \<pi> \<bullet> map_of (a # l) = map_of (\<pi> \<bullet> (a # l))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<pi> \<bullet> map_of l = map_of (\<pi> \<bullet> l) \<Longrightarrow> \<pi> \<bullet> (\<lambda>b. if b = fst a then Some (snd a) else map_of l b) = (\<lambda>b. if b = fst (\<pi> \<bullet> a) then Some (snd (\<pi> \<bullet> a)) else map_of (\<pi> \<bullet> l) b)
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. (\<pi> \<bullet> map_of) (\<pi> \<bullet> l) = map_of (\<pi> \<bullet> l) \<Longrightarrow> (\<lambda>x. if x = fst (\<pi> \<bullet> a) then Some (snd (\<pi> \<bullet> a)) else (\<pi> \<bullet> map_of) (\<pi> \<bullet> l) x) = (\<lambda>b. if b = fst (\<pi> \<bullet> a) then Some (snd (\<pi> \<bullet> a)) else map_of (\<pi> \<bullet> l) b)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma concat_eqvt[eqvt]: "\<pi> \<bullet> concat l = concat (\<pi> \<bullet> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> concat l = concat (\<pi> \<bullet> l)
[PROOF STEP]
by (induction l)(auto simp add: append_eqvt)


[STATEMENT]
lemma tranclp_eqvt[eqvt]: "\<pi> \<bullet> tranclp P v\<^sub>1 v\<^sub>2 = tranclp (\<pi> \<bullet> P) (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> P\<^sup>+\<^sup>+ v\<^sub>1 v\<^sub>2 = (\<pi> \<bullet> P)\<^sup>+\<^sup>+ (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)
[PROOF STEP]
unfolding tranclp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> lfp (\<lambda>p x1 x2. (\<exists>a b. x1 = a \<and> x2 = b \<and> P a b) \<or> (\<exists>a b c. x1 = a \<and> x2 = c \<and> p a b \<and> P b c)) v\<^sub>1 v\<^sub>2 = lfp (\<lambda>p x1 x2. (\<exists>a b. x1 = a \<and> x2 = b \<and> (\<pi> \<bullet> P) a b) \<or> (\<exists>a b c. x1 = a \<and> x2 = c \<and> p a b \<and> (\<pi> \<bullet> P) b c)) (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)
[PROOF STEP]
by perm_simp rule


[STATEMENT]
lemma rtranclp_eqvt[eqvt]: "\<pi> \<bullet> rtranclp P v\<^sub>1 v\<^sub>2 = rtranclp (\<pi> \<bullet> P) (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> P\<^sup>*\<^sup>* v\<^sub>1 v\<^sub>2 = (\<pi> \<bullet> P)\<^sup>*\<^sup>* (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)
[PROOF STEP]
unfolding rtranclp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> lfp (\<lambda>p x1 x2. (\<exists>a. x1 = a \<and> x2 = a) \<or> (\<exists>a b c. x1 = a \<and> x2 = c \<and> p a b \<and> P b c)) v\<^sub>1 v\<^sub>2 = lfp (\<lambda>p x1 x2. (\<exists>a. x1 = a \<and> x2 = a) \<or> (\<exists>a b c. x1 = a \<and> x2 = c \<and> p a b \<and> (\<pi> \<bullet> P) b c)) (\<pi> \<bullet> v\<^sub>1) (\<pi> \<bullet> v\<^sub>2)
[PROOF STEP]
by perm_simp rule


[STATEMENT]
lemma Set_filter_eqvt[eqvt]: "\<pi> \<bullet> Set.filter P S = Set.filter (\<pi> \<bullet> P) (\<pi> \<bullet> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> Set.filter P S = Set.filter (\<pi> \<bullet> P) (\<pi> \<bullet> S)
[PROOF STEP]
unfolding Set.filter_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> {a \<in> S. P a} = {a \<in> \<pi> \<bullet> S. (\<pi> \<bullet> P) a}
[PROOF STEP]
by perm_simp rule


[STATEMENT]
lemma Sigma_eqvt'[eqvt]: "\<pi> \<bullet> Sigma = Sigma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> Sigma = Sigma
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<pi> \<bullet> Sigma) x = Sigma x
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<pi> \<bullet> Sigma) x xa = Sigma x xa
[PROOF STEP]
apply (subst permute_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<pi> \<bullet> Sigma (- \<pi> \<bullet> x)) xa = Sigma x xa
[PROOF STEP]
apply (subst permute_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<pi> \<bullet> Sigma (- \<pi> \<bullet> x) (- \<pi> \<bullet> xa) = Sigma x xa
[PROOF STEP]
unfolding Sigma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<pi> \<bullet> (\<Union>x\<in>- \<pi> \<bullet> x. \<Union>y\<in>(- \<pi> \<bullet> xa) x. {(x, y)}) = (\<Union>x\<in>x. \<Union>y\<in>xa x. {(x, y)})
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<Union>x\<in>- (\<pi> \<bullet> \<pi>) \<bullet> \<pi> \<bullet> x. \<Union>xa\<in>(- (\<pi> \<bullet> \<pi>) \<bullet> \<pi> \<bullet> xa) x. {(x, xa)}) = (\<Union>x\<in>x. \<Union>y\<in>xa x. {(x, y)})
[PROOF STEP]
apply (simp add: permute_self)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma override_on_eqvt[eqvt]:
  "\<pi> \<bullet> (override_on m1 m2 S) = override_on (\<pi> \<bullet> m1) (\<pi> \<bullet> m2) (\<pi> \<bullet> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> override_on m1 m2 S = override_on (\<pi> \<bullet> m1) (\<pi> \<bullet> m2) (\<pi> \<bullet> S)
[PROOF STEP]
by (auto simp add: override_on_def )


[STATEMENT]
lemma card_eqvt[eqvt]:
  "\<pi> \<bullet> (card S) = card (\<pi> \<bullet> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> card S = card (\<pi> \<bullet> S)
[PROOF STEP]
by (cases "finite S", induct rule: finite_induct) (auto simp add: card_insert_if mem_permute_iff permute_pure)


[STATEMENT]
lemma Projl_permute:
  assumes a: "\<exists>y. f = Inl y"
  shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> projl f = projl (p \<bullet> f)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<exists>y. f = Inl y

goal (1 subgoal):
 1. p \<bullet> projl f = projl (p \<bullet> f)
[PROOF STEP]
by auto


[STATEMENT]
lemma Projr_permute:
  assumes a: "\<exists>y. f = Inr y"
  shows "(p \<bullet> (Sum_Type.projr f)) = Sum_Type.projr (p \<bullet> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> projr f = projr (p \<bullet> f)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<exists>y. f = Inr y

goal (1 subgoal):
 1. p \<bullet> projr f = projr (p \<bullet> f)
[PROOF STEP]
by auto


[STATEMENT]
lemma fresh_list_elem:
  assumes "a \<sharp> \<Gamma>"
  and "e \<in> set \<Gamma>"
  shows "a \<sharp> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<sharp> \<Gamma>
e \<in> set \<Gamma>

goal (1 subgoal):
 1. a \<sharp> e
[PROOF STEP]
by(induct \<Gamma>)(auto simp add: fresh_Cons)


[STATEMENT]
lemma set_not_fresh:
  "x \<in> set L \<Longrightarrow> \<not>(atom x \<sharp> L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set L \<Longrightarrow> \<not> atom x \<sharp> L
[PROOF STEP]
by (metis fresh_list_elem not_self_fresh)


[STATEMENT]
lemma pure_fresh_star[simp]: "a \<sharp>* (x :: 'a :: pure)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* x
[PROOF STEP]
by (simp add: fresh_star_def pure_fresh)


[STATEMENT]
lemma supp_set_mem: "x \<in> set L \<Longrightarrow> supp x \<subseteq> supp L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set L \<Longrightarrow> supp x \<subseteq> supp L
[PROOF STEP]
by (induct L) (auto simp add: supp_Cons)


[STATEMENT]
lemma set_supp_mono: "set L \<subseteq> set L2 \<Longrightarrow> supp L \<subseteq> supp L2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set L \<subseteq> set L2 \<Longrightarrow> supp L \<subseteq> supp L2
[PROOF STEP]
by (induct L)(auto simp add: supp_Cons supp_Nil dest:supp_set_mem)


[STATEMENT]
lemma fresh_star_at_base:
  fixes x :: "'a :: at_base"
  shows "S \<sharp>* x \<longleftrightarrow> atom x \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<sharp>* x = (atom x \<notin> S)
[PROOF STEP]
by (metis fresh_at_base(2) fresh_star_def)


[STATEMENT]
lemma supp_mono: "finite (B::'a::fs set) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> supp A \<subseteq> supp B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite B; A \<subseteq> B\<rbrakk> \<Longrightarrow> supp A \<subseteq> supp B
[PROOF STEP]
by (metis infinite_super subset_Un_eq supp_of_finite_union)


[STATEMENT]
lemma fresh_subset:
  "finite B \<Longrightarrow> x \<sharp> (B :: 'a::at_base set) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<sharp> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite B; x \<sharp> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> x \<sharp> A
[PROOF STEP]
by (auto dest:supp_mono simp add: fresh_def)


[STATEMENT]
lemma fresh_star_subset:
  "finite B \<Longrightarrow> x \<sharp>* (B :: 'a::at_base set) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<sharp>* A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite B; x \<sharp>* B; A \<subseteq> B\<rbrakk> \<Longrightarrow> x \<sharp>* A
[PROOF STEP]
by (metis fresh_star_def fresh_subset)


[STATEMENT]
lemma fresh_star_set_subset:
  "x \<sharp>* (B :: 'a::at_base list) \<Longrightarrow> set A \<subseteq> set B \<Longrightarrow> x \<sharp>* A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sharp>* B; set A \<subseteq> set B\<rbrakk> \<Longrightarrow> x \<sharp>* A
[PROOF STEP]
by (metis fresh_star_set fresh_star_subset[OF finite_set])


[STATEMENT]
lemma fv_eqvt[simp,eqvt]: "\<pi> \<bullet> (fv e) = fv (\<pi> \<bullet> e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> fv e = fv (\<pi> \<bullet> e)
[PROOF STEP]
unfolding fv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<bullet> {v. atom v \<in> supp e} = {v. atom v \<in> supp (\<pi> \<bullet> e)}
[PROOF STEP]
by simp


[STATEMENT]
lemma fv_Nil[simp]: "fv [] = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv [] = {}
[PROOF STEP]
by (auto simp add: fv_def supp_Nil)


[STATEMENT]
lemma fv_Pair[simp]: "fv (x, y) = fv x \<union> fv y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (x, y) = fv x \<union> fv y
[PROOF STEP]
by (auto simp add: fv_def supp_Pair)


[STATEMENT]
lemma fv_append[simp]: "fv (x @ y) = fv x \<union> fv y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (x @ y) = fv x \<union> fv y
[PROOF STEP]
by (auto simp add: fv_def supp_append)


[STATEMENT]
lemma fv_at_base[simp]: "fv a = {a::'a::at_base}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv a = {a}
[PROOF STEP]
by (auto simp add: fv_def supp_at_base)


[STATEMENT]
lemma fv_pure[simp]: "fv (a::'a::pure) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv a = {}
[PROOF STEP]
by (auto simp add: fv_def pure_supp)


[STATEMENT]
lemma fv_set_at_base[simp]: "fv (l :: ('a :: at_base) list) = set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv l = set l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma flip_not_fv: "a \<notin> fv x \<Longrightarrow> b \<notin> fv x \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> fv x; b \<notin> fv x\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x
[PROOF STEP]
by (metis flip_def fresh_def fv_def mem_Collect_eq swap_fresh_fresh)


[STATEMENT]
lemma fv_not_fresh: "atom x \<sharp> e \<longleftrightarrow> x \<notin> fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> e = (x \<notin> fv e)
[PROOF STEP]
unfolding fv_def fresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom x \<notin> supp e) = (x \<notin> {v. atom v \<in> supp e})
[PROOF STEP]
by blast


[STATEMENT]
lemma fresh_fv: "finite (fv e :: 'a set) \<Longrightarrow>  atom (x :: ('a::at_base)) \<sharp> (fv e :: 'a set) \<longleftrightarrow> atom x \<sharp> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (fv e) \<Longrightarrow> atom x \<sharp> fv e = atom x \<sharp> e
[PROOF STEP]
unfolding fv_def fresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {v. atom v \<in> supp e} \<Longrightarrow> (atom x \<notin> supp {v. atom v \<in> supp e}) = (atom x \<notin> supp e)
[PROOF STEP]
by (auto simp add: supp_finite_set_at_base)


[STATEMENT]
lemma finite_fv[simp]: "finite (fv (e::'a::fs) :: ('b::at_base) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
have "finite (supp e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (supp e)
[PROOF STEP]
by (metis finite_supp)
[PROOF STATE]
proof (state)
this:
finite (supp e)

goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
hence "finite (atom -` supp e :: 'b set)"
[PROOF STATE]
proof (prove)
using this:
finite (supp e)

goal (1 subgoal):
 1. finite (atom -` supp e)
[PROOF STEP]
apply (rule finite_vimageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj atom
[PROOF STEP]
apply (rule inj_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; atom x = atom y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
finite (atom -` supp e)

goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (atom -` supp e)

goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
have "(atom -` supp e  :: 'b set) = fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom -` supp e = fv e
[PROOF STEP]
unfolding fv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom -` supp e = {v. atom v \<in> supp e}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom -` supp e = fv e

goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (atom -` supp e)
atom -` supp e = fv e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (atom -` supp e)
atom -` supp e = fv e

goal (1 subgoal):
 1. finite (fv e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (fv e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pure_permute_id: "permute p = (\<lambda> x. (x::'a::pure))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permute p = (\<lambda>x. x)
[PROOF STEP]
by rule (simp add: permute_pure)


[STATEMENT]
lemma supp_set_elem_finite:
  assumes "finite S"
  and "(m::'a::fs) \<in> S"
  and "y \<in> supp m"
  shows "y \<in> supp S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> supp S
[PROOF STEP]
using assms supp_of_finite_sets
[PROOF STATE]
proof (prove)
using this:
finite S
m \<in> S
y \<in> supp m
finite ?S \<Longrightarrow> supp ?S = \<Union> (supp ` ?S)

goal (1 subgoal):
 1. y \<in> supp S
[PROOF STEP]
by auto


[STATEMENT]
lemma mem_permute_set:
  shows "x \<in> p \<bullet> S \<longleftrightarrow> (- p \<bullet> x) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> p \<bullet> S) = (- p \<bullet> x \<in> S)
[PROOF STEP]
by (metis mem_permute_iff permute_minus_cancel(2))


[STATEMENT]
lemma flip_set_both_not_in:
  assumes "x \<notin> S" and "x' \<notin> S"
  shows "((x' \<leftrightarrow> x) \<bullet> S) = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x' \<leftrightarrow> x) \<bullet> S = S
[PROOF STEP]
unfolding permute_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x' \<leftrightarrow> x) \<bullet> xa |xa. xa \<in> S} = S
[PROOF STEP]
by (auto) (metis assms flip_at_base_simps(3))+


[STATEMENT]
lemma inj_atom: "inj atom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj atom
[PROOF STEP]
by (metis atom_eq_iff injI)


[STATEMENT]
lemma eqvt_uncurry: "eqvt f \<Longrightarrow> eqvt (case_prod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt f \<Longrightarrow> eqvt (\<lambda>(x, y). f x y)
[PROOF STEP]
unfolding eqvt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. p \<bullet> f = f \<Longrightarrow> \<forall>p. p \<bullet> (\<lambda>(x, y). f x y) = (\<lambda>(x, y). f x y)
[PROOF STEP]
by perm_simp simp


[STATEMENT]
lemma supp_fun_app_eqvt2:
  assumes a: "eqvt f"
  shows "supp (f x y) \<subseteq> supp x \<union> supp y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (f x y) \<subseteq> supp x \<union> supp y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supp (f x y) \<subseteq> supp x \<union> supp y
[PROOF STEP]
from supp_fun_app_eqvt[OF eqvt_uncurry [OF a]]
[PROOF STATE]
proof (chain)
picking this:
supp (case ?x of (x, xa) \<Rightarrow> f x xa) \<subseteq> supp ?x
[PROOF STEP]
have "supp (case_prod f (x,y)) \<subseteq> supp (x,y)"
[PROOF STATE]
proof (prove)
using this:
supp (case ?x of (x, xa) \<Rightarrow> f x xa) \<subseteq> supp ?x

goal (1 subgoal):
 1. supp (case (x, y) of (x, xa) \<Rightarrow> f x xa) \<subseteq> supp (x, y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
supp (case (x, y) of (x, xa) \<Rightarrow> f x xa) \<subseteq> supp (x, y)

goal (1 subgoal):
 1. supp (f x y) \<subseteq> supp x \<union> supp y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
supp (case (x, y) of (x, xa) \<Rightarrow> f x xa) \<subseteq> supp (x, y)

goal (1 subgoal):
 1. supp (f x y) \<subseteq> supp x \<union> supp y
[PROOF STEP]
by (simp add: supp_Pair)
[PROOF STATE]
proof (state)
this:
supp (f x y) \<subseteq> supp x \<union> supp y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_fun_app_eqvt3:
  assumes a: "eqvt f"
  shows "supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z
[PROOF STEP]
from supp_fun_app_eqvt2[OF eqvt_uncurry [OF a]]
[PROOF STATE]
proof (chain)
picking this:
supp ((case ?x of (x, xa) \<Rightarrow> f x xa) ?y) \<subseteq> supp ?x \<union> supp ?y
[PROOF STEP]
have "supp (case_prod f (x,y) z) \<subseteq> supp (x,y) \<union> supp z"
[PROOF STATE]
proof (prove)
using this:
supp ((case ?x of (x, xa) \<Rightarrow> f x xa) ?y) \<subseteq> supp ?x \<union> supp ?y

goal (1 subgoal):
 1. supp ((case (x, y) of (x, xa) \<Rightarrow> f x xa) z) \<subseteq> supp (x, y) \<union> supp z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
supp ((case (x, y) of (x, xa) \<Rightarrow> f x xa) z) \<subseteq> supp (x, y) \<union> supp z

goal (1 subgoal):
 1. supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
supp ((case (x, y) of (x, xa) \<Rightarrow> f x xa) z) \<subseteq> supp (x, y) \<union> supp z

goal (1 subgoal):
 1. supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z
[PROOF STEP]
by (simp add: supp_Pair)
[PROOF STATE]
proof (state)
this:
supp (f x y z) \<subseteq> supp x \<union> supp y \<union> supp z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permute_0[simp]: "permute 0 = (\<lambda> x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permute 0 = (\<lambda>x. x)
[PROOF STEP]
by auto


[STATEMENT]
lemma permute_comp[simp]: "permute x \<circ> permute y = permute (x + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permute x \<circ> permute y = permute (x + y)
[PROOF STEP]
by auto


[STATEMENT]
lemma map_permute: "map (permute p) = permute p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (permute p) = permute p
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map (permute p) x = p \<bullet> x
[PROOF STEP]
apply (induct_tac x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. map (permute p) [] = p \<bullet> []
 2. \<And>x a list. map (permute p) list = p \<bullet> list \<Longrightarrow> map (permute p) (a # list) = p \<bullet> (a # list)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fresh_star_restrictA[intro]: "a \<sharp>* \<Gamma> \<Longrightarrow> a \<sharp>* AList.restrict V \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* \<Gamma> \<Longrightarrow> a \<sharp>* AList.restrict V \<Gamma>
[PROOF STEP]
by (induction \<Gamma>) (auto simp add: fresh_star_Cons)


[STATEMENT]
lemma Abs_lst_Nil_eq[simp]: "[[]]lst. (x::'a::fs) = [xs]lst. x' \<longleftrightarrow> (([],x) = (xs, x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]]lst. x = [xs]lst. x') = (([], x) = (xs, x'))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [[]]lst. x = [xs]lst. x' \<Longrightarrow> ([], x) = (xs, x')
 2. ([], x) = (xs, x') \<Longrightarrow> [[]]lst. x = [xs]lst. x'
[PROOF STEP]
apply (frule Abs_lst_fcb2[where f = "\<lambda> x y _ . (x,y)" and as = "[]" and bs = "xs" and c = "()"])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. [[]]lst. x = [xs]lst. x' \<Longrightarrow> set [] \<sharp>* ([], x)
 2. [[]]lst. x = [xs]lst. x' \<Longrightarrow> set [] \<sharp>* ()
 3. [[]]lst. x = [xs]lst. x' \<Longrightarrow> set xs \<sharp>* ()
 4. \<And>p. \<lbrakk>[[]]lst. x = [xs]lst. x'; supp p \<sharp>* ()\<rbrakk> \<Longrightarrow> p \<bullet> ([], x) = (p \<bullet> [], p \<bullet> x)
 5. \<And>p. \<lbrakk>[[]]lst. x = [xs]lst. x'; supp p \<sharp>* ()\<rbrakk> \<Longrightarrow> p \<bullet> (xs, x') = (p \<bullet> xs, p \<bullet> x')
 6. \<lbrakk>[[]]lst. x = [xs]lst. x'; ([], x) = (xs, x')\<rbrakk> \<Longrightarrow> ([], x) = (xs, x')
 7. ([], x) = (xs, x') \<Longrightarrow> [[]]lst. x = [xs]lst. x'
[PROOF STEP]
apply (auto simp add: fresh_star_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Abs_lst_Nil_eq2[simp]: "[xs]lst. (x::'a::fs) = [[]]lst. x' \<longleftrightarrow> ((xs,x) = ([], x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([xs]lst. x = [[]]lst. x') = ((xs, x) = ([], x'))
[PROOF STEP]
by (subst eq_commute) auto


[STATEMENT]
lemma shift_eq [simp]: \<open>n = m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = x
[PROOF STEP]
by (simp add: shift_def)


[STATEMENT]
lemma shift_gt [simp]: \<open>m < n \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E m
[PROOF STEP]
by (simp add: shift_def)


[STATEMENT]
lemma shift_lt [simp]: \<open>n < m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E (m-1)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> (E\<langle>n:x\<rangle>) m = E (m - 1)
[PROOF STEP]
by (simp add: shift_def)


[STATEMENT]
lemma shift_commute [simp]: \<open>E\<langle>n:y\<rangle>\<langle>0:x\<rangle> = E\<langle>0:x\<rangle>\<langle>n+1:y\<rangle>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E\<langle>n:y\<rangle>\<langle>0:x\<rangle> = E\<langle>0:x\<rangle>\<langle>n + 1:y\<rangle>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. (E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) xa = (E\<langle>0:x\<rangle>\<langle>n + 1:y\<rangle>) xa
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. (E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) xa = (E\<langle>0:x\<rangle>\<langle>n + 1:y\<rangle>) xa
[PROOF STEP]
show \<open>(E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) m = (E\<langle>0:x\<rangle>\<langle>n+1:y\<rangle>) m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) m = (E\<langle>0:x\<rangle>\<langle>n + 1:y\<rangle>) m
[PROOF STEP]
unfolding shift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if m < 0 then if m < n then E m else if m = n then y else E (m - 1) else if m = 0 then x else if m - 1 < n then E (m - 1) else if m - 1 = n then y else E (m - 1 - 1)) = (if m < n + 1 then if m < 0 then E m else if m = 0 then x else E (m - 1) else if m = n + 1 then y else if m - 1 < 0 then E (m - 1) else if m - 1 = 0 then x else E (m - 1 - 1))
[PROOF STEP]
by (cases m) simp_all
[PROOF STATE]
proof (state)
this:
(E\<langle>n:y\<rangle>\<langle>0:x\<rangle>) m = (E\<langle>0:x\<rangle>\<langle>n + 1:y\<rangle>) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_list_append: \<open>max_list (xs @ ys) = max (max_list xs) (max_list ys)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (xs @ ys) = max (max_list xs) (max_list ys)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma upd_vars_tm [simp]: \<open>n \<notin> set (vars_tm t) \<Longrightarrow> \<lparr>E(n := x), F\<rparr> t = \<lparr>E, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> set (vars_tm t) \<Longrightarrow> \<lparr>E(n := x), F\<rparr> t = \<lparr>E, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma shift_upd_commute: \<open>m \<le> n \<Longrightarrow> (E(n := x)\<langle>m:y\<rangle>) = ((E\<langle>m:y\<rangle>)(n + 1 := x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> E(n := x)\<langle>m:y\<rangle> = (E\<langle>m:y\<rangle>)(n + 1 := x)
[PROOF STEP]
unfolding shift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> (\<lambda>ma. if ma < m then (E(n := x)) ma else if ma = m then y else (E(n := x)) (ma - 1)) = (\<lambda>ma. if ma < m then E ma else if ma = m then y else E (ma - 1))(n + 1 := x)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma max_list_concat: \<open>xs \<in> set xss \<Longrightarrow> max_list xs \<le> max_list (concat xss)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> set xss \<Longrightarrow> max_list xs \<le> max_list (concat xss)
[PROOF STEP]
by (induct xss) (auto simp: max_list_append)


[STATEMENT]
lemma max_list_in: \<open>max_list xs < n \<Longrightarrow> n \<notin> set xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list xs < n \<Longrightarrow> n \<notin> set xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma upd_vars_fm [simp]: \<open>max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
proof (induct p arbitrary: E n)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
case (Pre P ts)
[PROOF STATE]
proof (state)
this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>max_list (concat (map vars_tm ts)) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
using Pre.prems max_list_concat
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
?xs \<in> set ?xss \<Longrightarrow> max_list ?xs \<le> max_list (concat ?xss)

goal (1 subgoal):
 1. max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_list (concat (map vars_tm ts)) < n

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max_list (concat (map vars_tm ts)) < n
[PROOF STEP]
have \<open>n \<notin> set (concat (map vars_tm ts))\<close>
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_tm ts)) < n

goal (1 subgoal):
 1. n \<notin> set (concat (map vars_tm ts))
[PROOF STEP]
using max_list_in
[PROOF STATE]
proof (prove)
using this:
max_list (concat (map vars_tm ts)) < n
max_list ?xs < ?n \<Longrightarrow> ?n \<notin> set ?xs

goal (1 subgoal):
 1. n \<notin> set (concat (map vars_tm ts))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<notin> set (concat (map vars_tm ts))

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<notin> set (concat (map vars_tm ts))
[PROOF STEP]
have \<open>\<forall>t \<in> set ts. n \<notin> set (vars_tm t)\<close>
[PROOF STATE]
proof (prove)
using this:
n \<notin> set (concat (map vars_tm ts))

goal (1 subgoal):
 1. \<forall>t\<in>set ts. n \<notin> set (vars_tm t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. n \<notin> set (vars_tm t)

goal (4 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>x1 x2 E n. max_list (vars_fm (\<^bold>\<ddagger> x1 x2)) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> x1 x2)
 3. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 4. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n \<notin> set (vars_tm t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n \<notin> set (vars_tm t)

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
using upd_vars_tm
[PROOF STATE]
proof (prove)
using this:
max_list (vars_fm (\<^bold>\<ddagger> P ts)) < n
\<forall>t\<in>set ts. n \<notin> set (vars_tm t)
?n \<notin> set (vars_tm ?t) \<Longrightarrow> \<lparr>?E(?n := ?x), ?F\<rparr> ?t = \<lparr>?E, ?F\<rparr> ?t

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)
[PROOF STEP]
by (metis list.map_cong semantics_fm.simps(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<ddagger> P ts) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<ddagger> P ts)

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
case (Uni p)
[PROOF STATE]
proof (state)
this:
max_list (vars_fm p) < ?n \<Longrightarrow> \<lbrakk>?E(?n := x), F, G\<rbrakk> p = \<lbrakk>?E, F, G\<rbrakk> p
max_list (vars_fm (\<^bold>\<forall> p)) < n

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>?case = ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))
[PROOF STEP]
by (simp add: fun_upd_def)
[PROOF STATE]
proof (state)
this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
have \<open>\<dots> = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p)) = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))
[PROOF STEP]
by (simp add: shift_upd_commute)
[PROOF STATE]
proof (state)
this:
((\<forall>y. \<lbrakk>E(n := x)\<langle>0:y\<rangle>, F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p)) = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))

goal (3 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
 3. \<And>p E n. \<lbrakk>\<And>E n. max_list (vars_fm p) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p; max_list (vars_fm (\<^bold>\<forall> p)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
using Uni
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)) = ((\<forall>y. \<lbrakk>(E\<langle>0:y\<rangle>)(n + 1 := x), F, G\<rbrakk> p) = (\<forall>y. \<lbrakk>E\<langle>0:y\<rangle>, F, G\<rbrakk> p))
max_list (vars_fm p) < ?n \<Longrightarrow> \<lbrakk>?E(?n := x), F, G\<rbrakk> p = \<lbrakk>?E, F, G\<rbrakk> p
max_list (vars_fm (\<^bold>\<forall> p)) < n

goal (1 subgoal):
 1. \<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>E(n := x), F, G\<rbrakk> (\<^bold>\<forall> p) = \<lbrakk>E, F, G\<rbrakk> (\<^bold>\<forall> p)

goal (2 subgoals):
 1. \<And>E n. max_list (vars_fm \<^bold>\<bottom>) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> \<^bold>\<bottom> = \<lbrakk>E, F, G\<rbrakk> \<^bold>\<bottom>
 2. \<And>p1 p2 E n. \<lbrakk>\<And>E n. max_list (vars_fm p1) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p1 = \<lbrakk>E, F, G\<rbrakk> p1; \<And>E n. max_list (vars_fm p2) < n \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> p2 = \<lbrakk>E, F, G\<rbrakk> p2; max_list (vars_fm (p1 \<^bold>\<longrightarrow> p2)) < n\<rbrakk> \<Longrightarrow> \<lbrakk>E(n := x), F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2) = \<lbrakk>E, F, G\<rbrakk> (p1 \<^bold>\<longrightarrow> p2)
[PROOF STEP]
qed (auto simp: max_list_append cong: map_cong)


[STATEMENT]
lemma inst_tm_semantics [simp]: \<open>\<lparr>E, F\<rparr> (t\<llangle>s/m\<rrangle>) = \<lparr>E\<langle>m:\<lparr>E, F\<rparr> s\<rangle>, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>E, F\<rparr> (t\<llangle>s/m\<rrangle>) = \<lparr>E\<langle>m:\<lparr>E, F\<rparr> s\<rangle>, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma inst_fm_semantics [simp]: \<open>\<lbrakk>E, F, G\<rbrakk> (p\<langle>t/m\<rangle>) = \<lbrakk>E\<langle>m:\<lparr>E, F\<rparr> t\<rangle>, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>E, F, G\<rbrakk> (p\<langle>t/m\<rangle>) = \<lbrakk>E\<langle>m:\<lparr>E, F\<rparr> t\<rangle>, F, G\<rbrakk> p
[PROOF STEP]
by (induct p arbitrary: E m t) (auto cong: map_cong)


[STATEMENT]
lemma size_inst_fm [simp]:
  \<open>size_fm (p\<langle>t/m\<rangle>) = size_fm p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOL_Axiomatic_Variant.size_fm (p\<langle>t/m\<rangle>) = FOL_Axiomatic_Variant.size_fm p
[PROOF STEP]
by (induct p arbitrary: m t) auto


[STATEMENT]
lemma boolean_semantics: \<open>boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> = \<lbrakk>E, F, G\<rbrakk>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> = \<lbrakk>E, F, G\<rbrakk>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> x = \<lbrakk>E, F, G\<rbrakk> x
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> x = \<lbrakk>E, F, G\<rbrakk> x
[PROOF STEP]
show \<open>boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
by (induct p) simp_all
[PROOF STATE]
proof (state)
this:
boolean (\<lambda>a. G a \<circ> map \<lparr>E, F\<rparr>) \<lbrakk>E, F, G\<rbrakk> p = \<lbrakk>E, F, G\<rbrakk> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tautology: \<open>tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
using boolean_semantics
[PROOF STATE]
proof (prove)
using this:
boolean (\<lambda>a. ?G a \<circ> map \<lparr>?E, ?F\<rparr>) \<lbrakk>?E, ?F, ?G\<rbrakk> = \<lbrakk>?E, ?F, ?G\<rbrakk>

goal (1 subgoal):
 1. tautology p \<Longrightarrow> \<lbrakk>E, F, G\<rbrakk> p
[PROOF STEP]
by metis