# HG changeset patch # User Christian Urban # Date 1310944911 -3600 # Node ID d629240f0f63bdb04e6b137a5a87193a6ac6eb11 # Parent 374e2f90140c4f6e2c5dea6f861b4578d003e7aa some tuning diff -r 374e2f90140c -r d629240f0f63 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Sun Jul 17 11:33:09 2011 +0100 +++ b/Nominal/Ex/Let.thy Mon Jul 18 00:21:51 2011 +0100 @@ -79,9 +79,6 @@ done -lemma max_eqvt[eqvt]: "p \ (max (a :: _ :: pure) b) = max (p \ a) (p \ b)" - by (simp add: permute_pure) - function apply_assn :: "(trm \ nat) \ assn \ nat" where diff -r 374e2f90140c -r d629240f0f63 Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Sun Jul 17 11:33:09 2011 +0100 +++ b/Nominal/Ex/LetRec.thy Mon Jul 18 00:21:51 2011 +0100 @@ -27,8 +27,6 @@ thm let_rec.fv_bn_eqvt thm let_rec.size_eqvt -lemma max_eqvt[eqvt]: "p \ (max (a :: _ :: pure) b) = max (p \ a) (p \ b)" - by (simp add: permute_pure) nominal_primrec height_trm :: "trm \ nat" @@ -56,8 +54,9 @@ apply (rule trans) apply(rule_tac p="p" in supp_perm_eq[symmetric]) apply (simp add: pure_supp fresh_star_def) - apply (simp only: eqvts) - apply (simp add: eqvt_at_def) + apply(simp add: eqvt_at_def) + apply(perm_simp) + apply (simp add: permute_fun_def) done termination by lexicographic_order diff -r 374e2f90140c -r d629240f0f63 Nominal/Ex/LetRecB.thy --- a/Nominal/Ex/LetRecB.thy Sun Jul 17 11:33:09 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,196 +0,0 @@ -theory LetRecB -imports "../Nominal2" -begin - -atom_decl name - -nominal_datatype let_rec: - trm = - Var "name" -| App "trm" "trm" -| Lam x::"name" t::"trm" binds x in t -| Let_Rec bp::"bp" t::"trm" binds "bn bp" in bp t -and bp = - Bp "name" "trm" -binder - bn::"bp \ atom list" -where - "bn (Bp x t) = [atom x]" - -thm let_rec.distinct -thm let_rec.induct -thm let_rec.exhaust -thm let_rec.fv_defs -thm let_rec.bn_defs -thm let_rec.perm_simps -thm let_rec.eq_iff -thm let_rec.fv_bn_eqvt -thm let_rec.size_eqvt - - -lemma Abs_lst_fcb2: - fixes as bs :: "'a :: fs" - and x y :: "'b :: fs" - and c::"'c::fs" - assumes eq: "[ba as]lst. x = [ba bs]lst. y" - and fcb1: "(set (ba as)) \* f as x c" - and fresh1: "set (ba as) \* c" - and fresh2: "set (ba bs) \* c" - and perm1: "\p. supp p \* c \ p \ (f as x c) = f (p \ as) (p \ x) c" - and perm2: "\p. supp p \* c \ p \ (f bs y c) = f (p \ bs) (p \ y) c" - and props: "eqvt ba" "inj ba" - shows "f as x c = f bs y c" -proof - - have "supp (as, x, c) supports (f as x c)" - unfolding supports_def fresh_def[symmetric] - by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) - then have fin1: "finite (supp (f as x c))" - by (auto intro: supports_finite simp add: finite_supp) - have "supp (bs, y, c) supports (f bs y c)" - unfolding supports_def fresh_def[symmetric] - by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) - then have fin2: "finite (supp (f bs y c))" - by (auto intro: supports_finite simp add: finite_supp) - obtain q::"perm" where - fr1: "(q \ (set (ba as))) \* (x, c, f as x c, f bs y c)" and - fr2: "supp q \* ([ba as]lst. x)" and - inc: "supp q \ (set (ba as)) \ q \ (set (ba as))" - using at_set_avoiding3[where xs="set (ba as)" and c="(x, c, f as x c, f bs y c)" and x="[ba as]lst. x"] - fin1 fin2 - by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) - have "[q \ (ba as)]lst. (q \ x) = q \ ([ba as]lst. x)" by simp - also have "\ = [ba as]lst. x" - by (simp only: fr2 perm_supp_eq) - finally have "[q \ (ba as)]lst. (q \ x) = [ba bs]lst. y" using eq by simp - then obtain r::perm where - qq1: "q \ x = r \ y" and - qq2: "q \ (ba as) = r \ (ba bs)" and - qq3: "supp r \ (q \ (set (ba as))) \ set (ba bs)" - apply(drule_tac sym) - apply(simp only: Abs_eq_iff2 alphas) - apply(erule exE) - apply(erule conjE)+ - apply(drule_tac x="p" in meta_spec) - apply(simp add: set_eqvt) - apply(blast) - done - have qq4: "q \ as = r \ bs" using qq2 props unfolding eqvt_def inj_on_def - apply(perm_simp) - apply(simp) - done - have "(set (ba as)) \* f as x c" by (rule fcb1) - then have "q \ ((set (ba as)) \* f as x c)" - by (simp add: permute_bool_def) - then have "set (q \ (ba as)) \* f (q \ as) (q \ x) c" - apply(simp add: fresh_star_eqvt set_eqvt) - apply(subst (asm) perm1) - using inc fresh1 fr1 - apply(auto simp add: fresh_star_def fresh_Pair) - done - then have "set (r \ (ba bs)) \* f (r \ bs) (r \ y) c" using qq1 qq2 qq4 - by simp - then have "r \ ((set (ba bs)) \* f bs y c)" - apply(simp add: fresh_star_eqvt set_eqvt) - apply(subst (asm) perm2[symmetric]) - using qq3 fresh2 fr1 - apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) - done - then have fcb2: "(set (ba bs)) \* f bs y c" by (simp add: permute_bool_def) - have "f as x c = q \ (f as x c)" - apply(rule perm_supp_eq[symmetric]) - using inc fcb1 fr1 by (auto simp add: fresh_star_def) - also have "\ = f (q \ as) (q \ x) c" - apply(rule perm1) - using inc fresh1 fr1 by (auto simp add: fresh_star_def) - also have "\ = f (r \ bs) (r \ y) c" using qq1 qq4 by simp - also have "\ = r \ (f bs y c)" - apply(rule perm2[symmetric]) - using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) - also have "... = f bs y c" - apply(rule perm_supp_eq) - using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) - finally show ?thesis by simp -qed - - -lemma max_eqvt[eqvt]: "p \ (max (a :: _ :: pure) b) = max (p \ a) (p \ b)" - by (simp add: permute_pure) - -nominal_primrec - height_trm :: "trm \ nat" -and height_bp :: "bp \ nat" -where - "height_trm (Var x) = 1" -| "height_trm (App l r) = max (height_trm l) (height_trm r)" -| "height_trm (Lam v b) = 1 + (height_trm b)" -| "height_trm (Let_Rec bp b) = max (height_bp bp) (height_trm b)" -| "height_bp (Bp v t) = height_trm t" - --"eqvt" - apply (simp only: eqvt_def height_trm_height_bp_graph_def) - apply (rule, perm_simp, rule, rule TrueI) - --"completeness" - apply (case_tac x) - apply (case_tac a rule: let_rec.exhaust(1)) - apply (auto)[4] - apply (case_tac b rule: let_rec.exhaust(2)) - apply blast - apply(simp_all) - apply (erule_tac c="()" in Abs_lst_fcb2) - apply (simp_all add: fresh_star_def pure_fresh)[3] - apply (simp add: eqvt_at_def) - apply (simp add: eqvt_at_def) - apply(simp add: eqvt_def) - apply(perm_simp) - apply(simp) - apply(simp add: inj_on_def) - --"The following could be done by nominal" - apply (simp add: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) - apply (simp add: meta_eq_to_obj_eq[OF height_bp_def, symmetric, unfolded fun_eq_iff]) - apply (subgoal_tac "eqvt_at height_bp bp") - apply (subgoal_tac "eqvt_at height_bp bpa") - apply (subgoal_tac "eqvt_at height_trm b") - apply (subgoal_tac "eqvt_at height_trm ba") - apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bp)") - apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inr bpa)") - apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl b)") - apply (thin_tac "eqvt_at height_trm_height_bp_sumC (Inl ba)") - defer - apply (simp add: eqvt_at_def height_trm_def) - apply (simp add: eqvt_at_def height_trm_def) - apply (simp add: eqvt_at_def height_bp_def) - apply (simp add: eqvt_at_def height_bp_def) - apply (subgoal_tac "height_bp bp = height_bp bpa") - apply (subgoal_tac "height_trm b = height_trm ba") - apply simp - apply (subgoal_tac "(\as x c. height_trm (snd (bp, b))) as x c = (\as x c. height_trm (snd (bpa, ba))) as x c") - apply simp - apply (erule_tac c="()" in Abs_lst_fcb2) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: eqvt_at_def) - apply (simp add: eqvt_at_def) - defer defer - apply (subgoal_tac "(\as x c. height_bp (fst (bp, b))) as x c = (\as x c. height_bp (fst (bpa, ba))) as x c") - apply simp - apply (erule_tac c="()" in Abs_lst_fcb2) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: fresh_star_def pure_fresh) - apply (simp add: eqvt_at_def) - apply (simp add: eqvt_at_def) ---"" - apply(simp_all add: eqvt_def inj_on_def) - apply(perm_simp) - apply(simp) - apply(perm_simp) - apply(simp) - done - -termination by lexicographic_order - -end - - - diff -r 374e2f90140c -r d629240f0f63 Nominal/Ex/LetSimple2.thy --- a/Nominal/Ex/LetSimple2.thy Sun Jul 17 11:33:09 2011 +0100 +++ b/Nominal/Ex/LetSimple2.thy Mon Jul 18 00:21:51 2011 +0100 @@ -62,8 +62,6 @@ lemma k: "A \ A \ A" by blast -lemma max_eqvt[eqvt]: "p \ (max (a :: _ :: pure) b) = max (p \ a) (p \ b)" - by (simp add: permute_pure) section {* definition with helper functions *} @@ -261,6 +259,7 @@ apply(simp add: eqvt_at_def perm_supp_eq) done +termination by lexicographic_order lemma ww1: shows "finite (fv_trm t)" @@ -324,7 +323,7 @@ where "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" -| "(set (bn as)) \* (y, s) \ (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" +| "(set (bn as)) \* (y, s, fv_bn as) \ (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" | "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])" apply(subgoal_tac "\p x r. subst_trm2_subst_assn2_graph x r \ subst_trm2_subst_assn2_graph (p \ x) (p \ r)") apply(simp add: eqvt_def) @@ -348,9 +347,23 @@ apply(simp) apply(case_tac a) apply(simp) - apply(rule_tac y="aa" and c="(b, c)" in trm_assn.strong_exhaust(1)) + apply(rule_tac y="aa" and c="(b, c, aa)" in trm_assn.strong_exhaust(1)) apply(blast)+ apply(simp) + apply(drule_tac x="assn" in meta_spec) + apply(drule_tac x="b" in meta_spec) + apply(drule_tac x="c" in meta_spec) + apply(drule_tac x="trm" in meta_spec) + apply(simp add: trm_assn.alpha_refl) + apply(rotate_tac 5) + apply(drule meta_mp) + apply(simp add: fresh_star_Pair) + apply(simp add: fresh_star_def trm_assn.fresh) + apply(simp add: fresh_def) + apply(subst supp_finite_atom_set) + apply(simp) + apply(simp) + apply(simp) apply(case_tac b) apply(simp) apply(rule_tac y="a" in trm_assn.exhaust(2)) @@ -362,7 +375,6 @@ apply(simp) prefer 2 apply(simp) - thm Inl_inject apply(drule Inl_inject) apply(rule arg_cong) back @@ -376,39 +388,20 @@ apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))") apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))") apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))") - defer - apply(simp add: Abs_eq_iff alphas) - apply(clarify) - apply(rule eqvt_at_perm) apply(simp) - apply(simp add: subst_trm2_def) - apply(simp add: eqvt_at_def) - defer - defer - defer - defer - defer - apply(rule conjI) - apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa") - apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa") + (* HERE *) + apply (subgoal_tac "subst_assn2 ast y s= subst_assn2 asta ya sa") + apply (subgoal_tac "subst_trm2 t y s = subst_trm2 ta ya sa") + apply(simp) apply(simp) apply(erule_tac conjE)+ apply(erule alpha_bn_cases) apply(simp add: trm_assn.bn_defs) apply(rotate_tac 7) - apply(drule k) - apply(erule conjE) - apply(subst (asm) Abs1_eq_iff) - apply(rule sort_of_atom_eq) - apply(rule sort_of_atom_eq) - apply(erule disjE) - apply(simp) - apply(rotate_tac 12) - apply(drule sym) - apply(rule sym) apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) apply(erule fresh_eqvt_at) + thm fresh_eqvt_at apply(simp add: Abs_fresh_iff) apply(simp add: fresh_star_def fresh_Pair)