--- /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
+
+
+