
diff -r e05c033d69c1 -r 5179ff4806c5 Nominal/Ex/AuxNoFCB.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/AuxNoFCB.thy	Tue Mar 27 14:56:06 2012 +0200
@@ -0,0 +1,194 @@
+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 lam2_rec where
+  "lam2_rec faa fll xs (Var n) (Var m) = ((n, m) \<in> set 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)
+  defer
+  apply (simp_all)[53]
+  apply clarify
+  apply metis
+  apply simp
+  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)
+  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 add: fresh_star_def)
+  apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and>
+         atom namea \<sharp> (name, c, Lam [name]. lam) \<and>
+         (\<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');
+         x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk>
+        \<Longrightarrow> P")
+  apply (simp add: fresh_star_def)
+  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')")
+  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
+  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
+  using Abs1_eq_iff lam.eq_iff apply metis
+  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
+  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
+  apply rule
+  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:
+  "aux (Var x) (Var y) xs = ((x, y) \<in> set 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)
+  prefer 2 apply rule
+  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)
+  done
+
+end
+
+
+




