--- a/Nominal/Ex/AuxNoFCB.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,402 +0,0 @@
-theory Lambda imports "../Nominal2" begin
-
-atom_decl name
-
-nominal_datatype lam =
- Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-
-nominal_primrec lookup where
- "lookup (n :: name) m [] \<longleftrightarrow> (n = m)"
-| "lookup n m ((hn, hm) # t) \<longleftrightarrow>
- (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)"
- apply (simp add: eqvt_def lookup_graph_def)
- apply (rule, perm_simp, rule, rule)
- by pat_completeness auto
-
-termination (eqvt) by lexicographic_order
-
-nominal_primrec lam2_rec where
- "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
-| "lam2_rec faa fll xs (Var n) (App l r) = False"
-| "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
-| "lam2_rec faa fll xs (App l r) (Var n) = False"
-| "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2"
-| "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False"
-| "lam2_rec faa fll xs (Lam [x]. t) (Var n) = False"
-| "lam2_rec faa fll xs (Lam [x]. t) (App l1 r1) = False"
-| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
- (\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
- \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
- lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s"
-| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
- \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
- \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
- lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False"
- apply (simp add: eqvt_def lam2_rec_graph_def)
- apply (rule, perm_simp, rule, rule)
- apply (case_tac x)
- apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust)
- apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
- apply simp_all[3] apply (metis, metis, metis)
- apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
- apply simp_all[3] apply (metis, metis, metis)
- apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust)
- apply simp_all[2] apply (metis, metis)
- unfolding fresh_star_def
- apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \<Longrightarrow> P")
- apply (thin_tac "\<And>faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \<Longrightarrow> P")
- apply (drule_tac x="name" in meta_spec)+
- apply (drule_tac x="c" in meta_spec)+
- apply (drule_tac x="namea" in meta_spec)+
- apply (drule_tac x="lama" in meta_spec)
- apply (drule_tac x="lama" in meta_spec)
- apply (drule_tac x="lam" in meta_spec)+
- apply (drule_tac x="b" in meta_spec)+
- apply (drule_tac x="a" in meta_spec)+
- apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
- atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow>
- Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')")
- apply clarify
- apply (simp)
- apply (simp only: fresh_Pair_elim)
- apply blast
- apply (simp_all)[53]
- apply clarify
- apply metis
- apply simp
- done
-
-termination (eqvt) by lexicographic_order
-
-lemma lam_rec2_cong[fundef_cong]:
- "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4 \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow>
- (\<And>n t n' t'. l = Lam [n]. t \<Longrightarrow> l2 = Lam [n']. t' \<Longrightarrow> fll n t n' t' = fll' n t n' t') \<Longrightarrow>
- lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2"
- apply (rule_tac y="l" and c="(xs, l2)" in lam.strong_exhaust)
- apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
- apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
- apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust)
- apply auto[2]
- apply clarify
- apply (case_tac "(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow>
- atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [name]. lam = Lam [x']. t' \<longrightarrow>
- Lam [namea]. lama = Lam [y']. s' \<longrightarrow> fll name lam namea lama = fll x' t' y' s')")
- unfolding fresh_star_def
- apply (subst lam2_rec.simps) apply simp
- apply (subst lam2_rec.simps) apply simp
- apply metis
- apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
- apply (subst lam2_rec.simps(10)) apply (simp_all add: fresh_star_def)
- done
-
-nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
- where
-[simp del]: "aux l r xs = lam2_rec
- (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs))
- (%x t y s. aux t s ((x, y) # xs)) xs l r"
- unfolding eqvt_def aux_graph_def
- apply (rule, perm_simp, rule, rule)
- by pat_completeness auto
-
-termination (eqvt)
- by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all
-
-lemma aux_simps[simp]:
- "aux (Var x) (Var y) xs = lookup x y xs"
- "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
- "aux (Var x) (App t1 t2) xs = False"
- "aux (Var x) (Lam [y].t) xs = False"
- "aux (App t1 t2) (Var x) xs = False"
- "aux (App t1 t2) (Lam [x].t) xs = False"
- "aux (Lam [x].t) (Var y) xs = False"
- "aux (Lam [x].t) (App t1 t2) xs = False"
- "\<lbrakk>atom x \<sharp> (s, xs); atom y \<sharp> (x, t, xs)\<rbrakk> \<Longrightarrow> aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps, simp)
- apply (subst aux.simps)
- apply (subst lam2_rec.simps)
- apply (rule, simp add: lam.fresh)
- apply (rule, simp add: lam.fresh)
- apply (intro allI impI)
- apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
- apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
- apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
- apply (rule_tac s="(atom x \<rightleftharpoons> atom a) \<bullet> aux t s ((x, y) # xs)" in trans)
- apply (rule permute_pure[symmetric])
- apply (simp add: eqvts swap_fresh_fresh)
- apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
- apply (rename_tac b)
- apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) ((atom y \<rightleftharpoons> atom b) \<bullet> s) ((a, b) # xs)" in trans)
- apply (rule_tac s="(atom y \<rightleftharpoons> atom b) \<bullet> aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
- apply (rule permute_pure[symmetric])
- apply (simp add: eqvts swap_fresh_fresh)
- apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
- apply (subst permute_eqvt)
- apply (simp add: eqvts swap_fresh_fresh)
- apply (rule sym)
- apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
- apply (rule_tac s="(atom x' \<rightleftharpoons> atom a) \<bullet> aux t' s' ((x', y') # xs)" in trans)
- apply (rule permute_pure[symmetric])
- apply (simp add: eqvts swap_fresh_fresh)
- apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
- apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') ((atom y' \<rightleftharpoons> atom b) \<bullet> s') ((a, b) # xs)" in trans)
- apply (rule_tac s="(atom y' \<rightleftharpoons> atom b) \<bullet> aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
- apply (rule permute_pure[symmetric])
- apply (simp add: eqvts swap_fresh_fresh)
- apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
- apply (subst permute_eqvt)
- apply (simp add: eqvts swap_fresh_fresh)
- apply (subgoal_tac "(atom x' \<rightleftharpoons> atom a) \<bullet> t' = (atom x \<rightleftharpoons> atom a) \<bullet> t")
- apply (subgoal_tac "(atom y' \<rightleftharpoons> atom b) \<bullet> s' = (atom y \<rightleftharpoons> atom b) \<bullet> s")
- apply simp
- apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \<rightleftharpoons> atom b) \<bullet> s)")
- apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \<rightleftharpoons> atom b) \<bullet> s')")
- apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
- apply (rule sym)
- apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
- apply (rule sym)
- apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
- apply (subgoal_tac "Lam [x]. t = Lam [a]. ((atom x \<rightleftharpoons> atom a) \<bullet> t)")
- apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \<rightleftharpoons> atom a) \<bullet> t')")
- apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
- apply (rule sym)
- apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
- apply (rule sym)
- apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
- apply (rule refl)
- done
-
-lemma aux_induct: "\<lbrakk>\<And>xs n m. P xs (Var n) (Var m); \<And>xs n l r. P xs (Var n) (App l r);
- \<And>xs n x t. P xs (Var n) (Lam [x]. t);
- \<And>xs l r n. P xs (App l r) (Var n);
- (\<And>xs l1 r1 l2 r2. P xs l1 l2 \<Longrightarrow> P xs r1 r2 \<Longrightarrow> P xs (App l1 r1) (App l2 r2));
- \<And>xs l r x t. P xs (App l r) (Lam [x]. t);
- \<And>xs x t n. P xs (Lam [x]. t) (Var n);
- \<And>xs x t l1 r1. P xs (Lam [x]. t) (App l1 r1);
- \<And>x xs y s t.
- atom x \<sharp> (xs, Lam [y]. s) \<and>
- atom y \<sharp> (x, xs, Lam [x]. t) \<Longrightarrow> P ((x, y) # xs) t s \<Longrightarrow> P xs (Lam [x]. t) (Lam [y]. s)\<rbrakk>
-\<Longrightarrow> P (a :: (name \<times> name) list) b c"
- apply (induction_schema)
- apply (rule_tac y="b" and c="(a, c)" in lam.strong_exhaust)
- apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
- apply simp_all[3] apply (metis)
- apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
- apply simp_all[3] apply (metis, metis, metis)
- apply (rule_tac y="c" and c="(name, a, b)" in lam.strong_exhaust)
- apply simp_all[3] apply (metis)
- apply (simp add: fresh_star_def)
- apply metis
- apply lexicographic_order
- done
-
-nominal_primrec swapequal :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" where
- "swapequal l r [] \<longleftrightarrow> l = r"
-| "atom x \<sharp> (l, r, hl, hr, t) \<Longrightarrow>
- swapequal l r ((hl, hr) # t) \<longleftrightarrow> swapequal ((hl \<leftrightarrow> x) \<bullet> l) ((hr \<leftrightarrow> x) \<bullet> r) t"
- unfolding eqvt_def swapequal_graph_def
- apply (rule, perm_simp, rule, rule TrueI)
- apply (case_tac x)
- apply (case_tac c)
- apply metis
- apply (case_tac aa)
- apply (rename_tac l r lst h t hl hr)
- apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh)
- apply simp
- apply simp
- apply simp
- apply clarify
- apply (rule_tac s="(x \<leftrightarrow> xa) \<bullet> swapequal_sumC ((hla \<leftrightarrow> x) \<bullet> la, (hra \<leftrightarrow> x) \<bullet> ra, ta)" in trans)
- apply (simp only: permute_pure)
- apply (simp add: eqvt_at_def fresh_Pair_elim)
- apply (simp add: flip_fresh_fresh)
- apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hla \<leftrightarrow> x) \<bullet> la = (hla \<leftrightarrow> xa) \<bullet> la")
- apply (subgoal_tac "(x \<leftrightarrow> xa) \<bullet> (hra \<leftrightarrow> x) \<bullet> ra = (hra \<leftrightarrow> xa) \<bullet> ra")
- apply simp
- apply (subst permute_eqvt)
- apply (simp add: flip_fresh_fresh flip_eqvt)
- apply (subst permute_eqvt)
- apply (simp add: flip_fresh_fresh flip_eqvt)
- done
-
-termination (eqvt) by lexicographic_order
-
-lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs"
- apply (induct xs)
- apply simp
- apply (case_tac a)
- apply (simp add: fresh_Cons)
- apply (rule_tac x="(ab, aa, b, xs)" and ?'a="name" in obtain_fresh)
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair lam.fresh)
- apply (simp add: fresh_Pair_elim)
- by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2))
-
-lemma var_neq_swapequal:
- "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs"
- "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs"
- apply (induct xs arbitrary: m)
- apply simp_all[2]
- apply (case_tac [!] a)
- apply (simp_all add: fresh_Cons)
- apply (rule_tac [!] x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh)
- apply (subst swapequal.simps)
- apply (auto simp add: fresh_Pair lam.fresh)[1]
- apply (elim conjE)
- apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
- apply (subst swapequal.simps)
- apply (auto simp add: fresh_Pair lam.fresh)[1]
- apply (elim conjE)
- apply (simp add: fresh_Pair_elim fresh_at_base permute_flip_at)
- done
-
-lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs"
- apply (induct xs arbitrary: m n)
- apply simp
- apply (case_tac a)
- apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh)
- apply simp
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair lam.fresh fresh_Nil)
- by (metis (hide_lams, mono_tags) flip_at_base_simps(3) flip_at_simps(1) fresh_Pair fresh_at_base(2) lam.perm_simps(1) var_eq_swapequal var_neq_swapequal(1) var_neq_swapequal(2))
-
-lemma swapequal_reorder: "
- a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow>
- swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)"
- apply (rule_tac x="(a, b, x, y, t, s, xs)" and ?'a="name" in obtain_fresh)
- apply (rule_tac x="(a, b, x, y, t, s, xs, aa)" and ?'a="name" in obtain_fresh)
- apply (rename_tac f g)
- apply (simp add: fresh_Pair_elim fresh_at_base)
- apply (subst swapequal.simps)
- apply (auto simp add: fresh_Pair fresh_Cons fresh_at_base)[1]
- apply (subgoal_tac "(x \<leftrightarrow> f) \<bullet> atom g \<sharp> t")
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair fresh_Cons fresh_permute_left)
- apply rule apply assumption
- apply (simp add: flip_at_base_simps fresh_at_base flip_def)
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
- apply rule apply (rotate_tac 12)
- apply assumption
- apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair fresh_Cons fresh_at_base fresh_permute_left)
- apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> atom f \<sharp> t")
- apply rule apply assumption
- apply (simp add: flip_at_base_simps fresh_at_base flip_def)
- apply (simp add: flip_at_base_simps fresh_at_base flip_def)
- apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
- apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
- apply simp
- apply (subst permute_eqvt) apply (simp add: flip_eqvt)
- apply (subst permute_eqvt) apply (simp add: flip_eqvt)
- apply (simp add: flip_at_base_simps fresh_at_base flip_def)
- done
-
-lemma swapequal_lambda:
- assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs"
- shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)"
- using assms
- apply (induct xs arbitrary: t s x y)
- apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh)
- apply (simp add: fresh_Pair_elim fresh_Nil)
- apply (subst swapequal.simps)
- apply (simp add: fresh_Pair fresh_Nil)
- apply auto[1]
- apply simp
- apply (subgoal_tac "[[atom x]]lst. t = [[atom a]]lst. ((x \<leftrightarrow> a) \<bullet> t)")
- apply (subgoal_tac "[[atom y]]lst. s = [[atom a]]lst. ((y \<leftrightarrow> a) \<bullet> s)")
- apply simp
- apply (simp add: Abs1_eq_iff)
- apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2]
- apply (simp add: fresh_permute_left)
- apply (simp add: fresh_permute_left)
- apply clarify
- apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
- apply clarify
- apply (simp add: swapequal_reorder)
- apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh)
- apply (rename_tac f)
- apply (subst (2) swapequal.simps)
- apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
- apply (subst swapequal.simps)
- apply (auto simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons)[1]
- apply (simp add: flip_def fresh_Pair_elim fresh_at_base)
- done
-
-lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs"
- apply (induct xs rule:swapequal.induct)
- apply auto[1]
- apply (simp add: fresh_Pair_elim)
- apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r")
- apply simp
- apply (intro allI)
- apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec)
- apply (drule_tac x="q + (hr \<leftrightarrow> x)" in spec)
- apply simp
- done
-
-lemma swapequal_app: "(swapequal l1 l2 xs \<and> swapequal r1 r2 xs) = swapequal (App l1 r1) (App l2 r2) xs"
- apply (induct xs arbitrary: l1 l2 r1 r2)
- apply simp
- apply (case_tac a)
- apply simp
- apply (rule_tac x="(l1, l2, r1, r2, aa, b, xs)" and ?'a="name" in obtain_fresh)
- apply (simp add: fresh_Pair_elim)
- apply (subst swapequal.simps) apply (auto simp add: fresh_Pair)[1]
- apply (subst swapequal.simps) apply (auto simp add: fresh_Pair lam.fresh)
- done
-
-lemma [simp]: "distinct (map fst xs) \<Longrightarrow> distinct xs"
- by (induct xs) auto
-
-lemma [simp]:
- "atom x \<sharp> xs \<Longrightarrow> x \<notin> fst ` set xs"
- "atom x \<sharp> xs \<Longrightarrow> x \<notin> snd ` set xs"
- apply (induct xs)
- apply simp_all
- apply (case_tac [!] a)
- apply (simp_all add: fresh_Cons fresh_Pair fresh_at_base)
- done
-
-lemma aux_alphaish:
- assumes "distinct (map fst xs @ map snd xs)"
- shows "aux x y xs \<longleftrightarrow> swapequal x y xs"
- using assms
- apply (induct xs x y rule: aux_induct)
- apply (simp add: lookup_swapequal)
- apply (simp, rule distinct_swapequal, simp)+
- apply (simp add: swapequal_app)
- apply (simp, rule distinct_swapequal, simp)+
- apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base conjE)
- apply (elim conjE)
- apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base)
- apply (subgoal_tac "x \<notin> fst ` set xs \<and>
- x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs")
- apply (subst swapequal_lambda)
- apply auto[2]
- apply simp
- done
-
-lemma aux_is_alpha:
- "aux x y [] \<longleftrightarrow> (x = y)"
- by (simp_all add: supp_Nil aux_alphaish)
-
-end
-
-
-