# HG changeset patch # User Cezary Kaliszyk # Date 1332852966 -7200 # Node ID 5179ff4806c5267928a666afb1d76bbc387a2d26 # Parent e05c033d69c1e0da882e5ff7a4d848a93219c692 Define 'aux' 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) \ 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 \ (xs, Lam [y]. s) \ atom y \ (x, xs, Lam [x]. t) \ + (\x' y' t' s'. atom x' \ (xs, Lam [y']. s') \ atom y' \ (x', xs, Lam [x']. t') \ Lam [x]. t = Lam [x']. t' \ Lam [y]. s = Lam [y']. s' + \ fll x t y s = fll x' t' y' s')) \ + lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s" +| "(atom x \ (xs, Lam [y]. s) \ atom y \ (x, xs, Lam [x]. t) \ + \(\x' y' t' s'. atom x' \ (xs, Lam [y']. s') \ atom y' \ (x', xs, Lam [x']. t') \ Lam [x]. t = Lam [x']. t' \ Lam [y]. s = Lam [y']. s' + \ fll x t y s = fll x' t' y' s')) \ + 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 "\faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \ P") + apply (thin_tac "\faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \ P") + apply (thin_tac "\faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \ P") + apply (thin_tac "\faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \ P") + apply (thin_tac "\faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \ P") + apply (thin_tac "\faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \ P") + apply (thin_tac "\faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \ P") + apply (thin_tac "\faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \ 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 " +(\x' y' t' s'. + atom x' \ (c, Lam [y']. s') \ + atom y' \ (x', c, Lam [x']. t') \ + Lam [name]. lam = Lam [x']. t' \ + Lam [namea]. lama = Lam [y']. s' \ b name lam namea lama = b x' t' y' s') + ") + apply clarify + apply (simp add: fresh_star_def) + apply (thin_tac "\atom name \ (c, Lam [namea]. lama) \ + atom namea \ (name, c, Lam [name]. lam) \ + (\x' y' t' s'. + atom x' \ (c, Lam [y']. s') \ + atom y' \ (x', c, Lam [x']. t') \ + Lam [name]. lam = Lam [x']. t' \ + Lam [namea]. lama = Lam [y']. s' \ b name lam namea lama = b x' t' y' s'); + x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\ + \ P") + apply (simp add: fresh_star_def) + done + +termination (eqvt) by lexicographic_order + +lemma lam_rec2_cong[fundef_cong]: + "(\s1 s2 s3 s4. l = App s1 s2 \ l2 = App s3 s4 \ faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \ + (\n t n' t'. l = Lam [n]. t \ l2 = Lam [n']. t' \ fll n t n' t' = fll' n t n' t') \ + 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 "(\x' y' t' s'. + atom x' \ (xs, Lam [y']. s') \ + atom y' \ (x', xs, Lam [x']. t') \ + Lam [name]. lam = Lam [x']. t' \ + Lam [namea]. lama = Lam [y']. s' \ + 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 \ lam \ (name \ name) list \ bool" + where +[simp del]: "aux l r xs = lam2_rec + (%t1 t2 t3 t4. (aux t1 t3 xs) \ (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 (\(l, r, xs). size l + size r)") simp_all + +lemma aux_simps: + "aux (Var x) (Var y) xs = ((x, y) \ set xs)" + "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \ 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" + "\atom x \ (s, xs); atom y \ (x, t, xs)\ \ 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 \ atom a) \ t) s ((a, y) # xs)" in trans) + apply (rule_tac s="(atom x \ atom a) \ 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 \ atom a) \ t) ((atom y \ atom b) \ s) ((a, b) # xs)" in trans) + apply (rule_tac s="(atom y \ atom b) \ aux ((atom x \ atom a) \ 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' \ atom a) \ t') s' ((a, y') # xs)" in trans) + apply (rule_tac s="(atom x' \ atom a) \ 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' \ atom a) \ t') ((atom y' \ atom b) \ s') ((a, b) # xs)" in trans) + apply (rule_tac s="(atom y' \ atom b) \ aux ((atom x' \ atom a) \ 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' \ atom a) \ t' = (atom x \ atom a) \ t") + apply (subgoal_tac "(atom y' \ atom b) \ s' = (atom y \ atom b) \ s") + apply simp + apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \ atom b) \ s)") + apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \ atom b) \ 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 \ atom a) \ t)") + apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \ atom a) \ 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 + + +