# HG changeset patch # User Christian Urban # Date 1342353827 -3600 # Node ID 14c7d7e29c4454c2a38930990d33108e622f55cc # Parent 0440bc1a243876b852bdf14d26246065b180fb24 added a simproc for alpha-equivalence to the simplifier diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/CPS1_Plotkin.thy --- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Sun Jul 15 13:03:47 2012 +0100 @@ -12,10 +12,12 @@ (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))" unfolding eqvt_def CPS_graph_def apply (rule, perm_simp, rule, rule) +using [[simproc del: alpha_lst]] apply (simp_all add: fresh_Pair_elim) apply (rule_tac y="x" in lt.exhaust) apply (auto)[3] apply (rule_tac x="name" and ?'a="name" in obtain_fresh) +using [[simproc del: alpha_lst]] apply (simp_all add: fresh_at_base)[3] apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh) apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh) @@ -81,6 +83,7 @@ unfolding convert_graph_def eqvt_def apply (rule, perm_simp, rule, rule) apply (erule lt.exhaust) + using [[simproc del: alpha_lst]] apply (simp_all) apply blast apply (simp add: Abs1_eq_iff CPS.eqvt) @@ -113,6 +116,7 @@ Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))" unfolding Kapply_graph_def eqvt_def apply (rule, perm_simp, rule, rule) +using [[simproc del: alpha_lst]] apply (simp_all) apply (case_tac x) apply (rule_tac y="a" in lt.exhaust) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy --- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Sun Jul 15 13:03:47 2012 +0100 @@ -18,8 +18,10 @@ | fill_abs : "atom x \ M \ (CAbs x C) = Lam x (C)" unfolding eqvt_def fill_graph_def apply perm_simp + using [[simproc del: alpha_lst]] apply auto apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) + using [[simproc del: alpha_lst]] apply (auto simp add: fresh_star_def) apply (erule Abs_lst1_fcb) apply (simp_all add: Abs_fresh_iff)[2] @@ -41,8 +43,10 @@ | "ccomp (CFun C N) C' = CFun (ccomp C C') N" unfolding eqvt_def ccomp_graph_def apply perm_simp + using [[simproc del: alpha_lst]] apply auto apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) + using [[simproc del: alpha_lst]] apply (auto simp add: fresh_star_def) apply blast+ apply (erule Abs_lst1_fcb) @@ -71,10 +75,12 @@ ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))" | "~isValue M \ ~isValue N \ atom a \ (N, b) \ CPS (M $$ N) = ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))" + using [[simproc del: alpha_lst]] apply auto defer apply (case_tac x) apply (rule_tac y="a" in lt.exhaust) + using [[simproc del: alpha_lst]] apply auto apply blast apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy --- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Sun Jul 15 13:03:47 2012 +0100 @@ -15,6 +15,7 @@ | "atom c \ (x, M) \ (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" apply (simp only: eqvt_def CPS1_CPS2_graph_def) apply (rule, perm_simp, rule) + using [[simproc del: alpha_lst]] apply auto apply (case_tac x) apply (case_tac a) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/Lt.thy --- a/Nominal/Ex/CPS/Lt.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/CPS/Lt.thy Sun Jul 15 13:03:47 2012 +0100 @@ -19,6 +19,7 @@ unfolding eqvt_def subst_graph_def apply (simp) apply(rule TrueI) + using [[simproc del: alpha_lst]] apply(auto simp add: lt.distinct lt.eq_iff) apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) apply blast @@ -60,7 +61,7 @@ inductive eval :: "[lt, lt] \ bool" (" _ \\<^isub>\ _" [80,80] 80) where - evbeta: "\atom x\V; isValue V\ \ ((Lam x M) $$ V) \\<^isub>\ (M[x ::= V])" + evbeta: "\atom x \ V; isValue V\ \ ((Lam x M) $$ V) \\<^isub>\ (M[x ::= V])" | ev1: "\isValue V; M \\<^isub>\ M' \ \ (V $$ M) \\<^isub>\ (V $$ M')" | ev2: "M \\<^isub>\ M' \ (M $$ N) \\<^isub>\ (M' $$ N)" diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/Classical.thy Sun Jul 15 13:03:47 2012 +0100 @@ -77,6 +77,7 @@ apply(metis)+ -- "compatibility" apply(all_trivials) + using [[simproc del: alpha_lst]] apply(simp_all) apply(rule conjI) apply(elim conjE) @@ -280,6 +281,7 @@ apply (simp_all add: fresh_star_def)[12] apply(metis)+ -- "compatibility" + using [[simproc del: alpha_lst]] apply(simp_all) apply(rule conjI) apply(elim conjE) @@ -479,18 +481,7 @@ apply(case_tac x) apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust) apply (simp_all add: fresh_star_def fresh_Pair)[12] - apply(metis)+ - apply(subgoal_tac "\x'::name. atom x' \ (trm, b, d)") - apply(auto simp add: fresh_Pair)[1] - apply(metis)+ - apply(subgoal_tac "\x'::name. atom x' \ (trm, b, d)") - apply(auto simp add: fresh_Pair)[1] - apply(rule obtain_fresh) - apply(auto)[1] - apply(metis)+ - -- "compatibility" - apply(all_trivials) - apply(simp) + apply(metis) oops end diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/Lambda.thy Sun Jul 15 13:03:47 2012 +0100 @@ -94,6 +94,7 @@ apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) apply(auto)[3] +using [[simproc del: alpha_lst]] apply(simp_all) apply(erule_tac c="()" in Abs_lst1_fcb2') apply(simp_all add: pure_fresh fresh_star_def)[3] @@ -124,6 +125,7 @@ apply(case_tac x) apply(rule_tac y="b" and c="a" in lam.strong_exhaust) apply(auto simp add: fresh_star_def)[3] +using [[simproc del: alpha_lst]] apply(simp_all) apply(erule conjE)+ apply(erule_tac Abs_lst1_fcb2) @@ -169,6 +171,7 @@ apply(case_tac x) apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) apply(auto simp add: fresh_star_def)[3] + using [[simproc del: alpha_lst]] apply(simp_all) apply(erule conjE)+ apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) @@ -202,6 +205,7 @@ apply(simp) apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) +using [[simproc del: alpha_lst]] apply(auto) apply (erule_tac c="()" in Abs_lst1_fcb2) apply(simp add: supp_removeAll fresh_def) @@ -229,6 +233,7 @@ apply(auto)[9] apply(rule_tac y="x" in lam.exhaust) apply(auto)[3] + using [[simproc del: alpha_lst]] apply(simp) apply(erule_tac c="()" in Abs_lst1_fcb2) apply(simp add: fresh_minus_atom_set) @@ -254,6 +259,7 @@ apply(simp add: eqvt_def height_graph_def) apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) + using [[simproc del: alpha_lst]] apply(auto) apply (erule_tac c="()" in Abs_lst1_fcb2) apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) @@ -276,9 +282,11 @@ unfolding eqvt_def subst_graph_def apply(simp) apply(rule TrueI) + using [[simproc del: alpha_lst]] apply(auto) apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) apply(blast)+ + using [[simproc del: alpha_lst]] apply(simp_all add: fresh_star_def fresh_Pair_elim) apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) apply(simp_all add: Abs_fresh_iff) @@ -306,8 +314,10 @@ text {* same lemma but with subst.induction *} lemma forget2: shows "atom x \ t \ t[x ::= s] = t" - by (induct t x s rule: subst.induct) - (auto simp add: fresh_at_base fresh_Pair) + apply(induct t x s rule: subst.induct) + using [[simproc del: alpha_lst]] + apply(auto simp add: flip_fresh_fresh fresh_Pair fresh_at_base) + done lemma fresh_fact: fixes z::"name" @@ -467,6 +477,7 @@ apply(auto)[1] apply (rule_tac y="a" and c="b" in lam.strong_exhaust) apply (auto simp add: fresh_star_def)[3] + using [[simproc del: alpha_lst]] apply(simp_all) apply(erule conjE)+ apply (erule_tac c="xsa" in Abs_lst1_fcb2') @@ -498,6 +509,7 @@ apply(auto)[3] apply(all_trivials) apply(simp) + using [[simproc del: alpha_lst]] apply(simp) apply(erule_tac c="()" in Abs_lst1_fcb2') apply(simp add: pure_fresh) @@ -526,6 +538,7 @@ apply(all_trivials) apply(simp) apply(simp) + using [[simproc del: alpha_lst]] apply(simp) apply(erule conjE) apply(erule Abs_lst1_fcb2') @@ -582,6 +595,7 @@ apply (case_tac x) apply (rule_tac y="a" and c="b" in lam.strong_exhaust) apply (auto simp add: fresh_star_def fresh_at_list)[3] + using [[simproc del: alpha_lst]] apply(simp_all) apply(elim conjE) apply (erule_tac c="xsa" in Abs_lst1_fcb2') @@ -641,6 +655,7 @@ apply(rule TrueI) apply (case_tac x) apply (case_tac a rule: lam.exhaust) + using [[simproc del: alpha_lst]] apply simp_all[3] apply blast apply (case_tac b) @@ -649,6 +664,7 @@ apply blast apply blast apply (simp add: Abs1_eq_iff fresh_star_def) + using [[simproc del: alpha_lst]] apply(simp_all) apply(erule_tac c="()" in Abs_lst1_fcb2) apply (simp add: Abs_fresh_iff) @@ -692,6 +708,7 @@ apply (rule TrueI) apply (case_tac x) apply (rule_tac y="a" in lam.exhaust) +using [[simproc del: alpha_lst]] apply simp_all apply blast apply blast @@ -718,6 +735,7 @@ apply (simp add: eqvt_def map_term_graph_def) apply(rule TrueI) apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust) + using [[simproc del: alpha_lst]] apply auto apply (erule Abs_lst1_fcb) apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) @@ -890,13 +908,16 @@ apply(rule_tac y="b" in lam.exhaust) apply(auto)[3] apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust) + using [[simproc del: alpha_lst]] apply(auto)[3] apply(drule_tac x="name" in meta_spec) apply(drule_tac x="name" in meta_spec) apply(drule_tac x="lam" in meta_spec) apply(drule_tac x="(name \ namea) \ lama" in meta_spec) + using [[simproc del: alpha_lst]] apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def) apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2)) + using [[simproc del: alpha_lst]] apply simp_all apply (simp add: abs_same_binder) apply (erule_tac c="()" in Abs_lst1_fcb2) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/Let.thy Sun Jul 15 13:03:47 2012 +0100 @@ -122,6 +122,7 @@ apply (drule_tac x="assn" in meta_spec) apply (drule_tac x="trm" in meta_spec) apply (simp add: alpha_bn_refl) + using [[simproc del: alpha_lst]] apply(simp_all) apply (erule_tac c="()" in Abs_lst1_fcb2) apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)[4] @@ -179,6 +180,7 @@ apply simp_all[7] prefer 2 apply(simp) + using [[simproc del: alpha_lst]] apply(simp) apply(erule conjE)+ apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/LetRec.thy --- a/Nominal/Ex/LetRec.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/LetRec.thy Sun Jul 15 13:03:47 2012 +0100 @@ -39,9 +39,11 @@ | "height_bp (Bp v t) = height_trm t" apply (simp only: eqvt_def height_trm_height_bp_graph_def) apply (rule, perm_simp, rule, rule TrueI) + using [[simproc del: alpha_set]] apply auto apply (case_tac x) apply (case_tac a rule: let_rec.exhaust(1)) + using [[simproc del: alpha_set]] apply auto apply (case_tac b rule: let_rec.exhaust(2)) apply blast diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Pi.thy --- a/Nominal/Ex/Pi.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Ex/Pi.thy Sun Jul 15 13:03:47 2012 +0100 @@ -179,6 +179,7 @@ | "(\\{xg})[x::=\y] = \\{(xg[x::=\\y])}" | "\atom b \ (x, y)\ \ (\a?\.P)[x::=\y] = \(a[x:::=y])?\.(P[x::=\y])" | "(succ\)[x::=\y] = succ\" + using [[simproc del: alpha_lst]] apply(auto simp add: piMix_distinct piMix_eq_iff) apply(subgoal_tac "\p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \ subsGuard_mix_subsList_mix_subs_mix_graph (p \ x) (p \ r)") unfolding eqvt_def @@ -294,10 +295,12 @@ apply(case_tac ba) apply(simp) apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3)) + using [[simproc del: alpha_lst]] apply(auto simp add: fresh_star_def)[1] apply(blast) apply(blast) apply(blast) + using [[simproc del: alpha_lst]] apply(auto simp add: fresh_star_def)[1] apply(blast) apply(simp) diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Nominal/Nominal2_Abs.thy Sun Jul 15 13:03:47 2012 +0100 @@ -801,7 +801,7 @@ apply(blast)+ done -lemma Abs1_eq_fresh: +lemma Abs1_eq_iff_fresh: fixes x y::"'a::fs" and a b c::"'b::at" assumes "atom c \ (a, b, x, y)" @@ -843,7 +843,7 @@ by (simp add: Abs1_eq) qed -lemma Abs1_eq_all: +lemma Abs1_eq_iff_all: fixes x y::"'a::fs" and z::"'c::fs" and a b::"'b::at" @@ -852,25 +852,25 @@ and "[[atom a]]lst. x = [[atom b]]lst. y \ (\c. atom c \ (a, b, x, y, z) \ (a \ c) \ x = (b \ c) \ y)" apply - apply(auto) -apply(simp add: Abs1_eq_fresh(1)[symmetric]) +apply(simp add: Abs1_eq_iff_fresh(1)[symmetric]) apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) apply(drule_tac x="aa" in spec) apply(simp) -apply(subst Abs1_eq_fresh(1)) +apply(subst Abs1_eq_iff_fresh(1)) apply(auto simp add: fresh_Pair)[1] apply(assumption) -apply(simp add: Abs1_eq_fresh(2)[symmetric]) +apply(simp add: Abs1_eq_iff_fresh(2)[symmetric]) apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) apply(drule_tac x="aa" in spec) apply(simp) -apply(subst Abs1_eq_fresh(2)) +apply(subst Abs1_eq_iff_fresh(2)) apply(auto simp add: fresh_Pair)[1] apply(assumption) -apply(simp add: Abs1_eq_fresh(3)[symmetric]) +apply(simp add: Abs1_eq_iff_fresh(3)[symmetric]) apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) apply(drule_tac x="aa" in spec) apply(simp) -apply(subst Abs1_eq_fresh(3)) +apply(subst Abs1_eq_iff_fresh(3)) apply(auto simp add: fresh_Pair)[1] apply(assumption) done @@ -964,6 +964,35 @@ using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) +ML {* +fun alpha_single_simproc thm _ ss ctrm = + let + val ctxt = Simplifier.the_context ss + val thy = Proof_Context.theory_of ctxt + val _ $ (_ $ x) $ (_ $ y) = term_of ctrm + val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) + |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) + |> map Free + |> HOLogic.mk_tuple + |> Thm.cterm_of thy + val cvrs_ty = ctyp_of_term cvrs + val thm' = thm + |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] + in + SOME thm' + end +*} + +simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") = + {* alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]} *} + +simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") = + {* alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]} *} + +simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") = + {* alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]} *} + + subsection {* Renaming of bodies of abstractions *} lemma Abs_rename_set: diff -r 0440bc1a2438 -r 14c7d7e29c44 Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Tutorial/Lambda.thy Sun Jul 15 13:03:47 2012 +0100 @@ -41,6 +41,7 @@ apply(simp add: eqvt_def height_graph_def) apply(rule TrueI) apply(rule_tac y="x" in lam.exhaust) +using [[simproc del: alpha_lst]] apply(auto) apply(erule_tac c="()" in Abs_lst1_fcb2) apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) @@ -61,6 +62,7 @@ unfolding eqvt_def subst_graph_def apply(rule, perm_simp, rule) apply(rule TrueI) + using [[simproc del: alpha_lst]] apply(auto) apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) apply(blast)+ diff -r 0440bc1a2438 -r 14c7d7e29c44 Tutorial/Tutorial2.thy --- a/Tutorial/Tutorial2.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Tutorial/Tutorial2.thy Sun Jul 15 13:03:47 2012 +0100 @@ -376,7 +376,7 @@ moreover have "Lam [x]. Var x \ Var x" using unbind_simple by auto ultimately - have "atom x \ Var x" using unbind_fake by auto + have "atom x \ Var x" using unbind_fake by blast then have "x \ x" by (simp add: lam.fresh fresh_at_base) then show "False" by simp qed diff -r 0440bc1a2438 -r 14c7d7e29c44 Tutorial/Tutorial5.thy --- a/Tutorial/Tutorial5.thy Thu Jul 12 10:11:32 2012 +0100 +++ b/Tutorial/Tutorial5.thy Sun Jul 15 13:03:47 2012 +0100 @@ -127,12 +127,13 @@ obtains T1 T2 where "T = T1 \ T2" "(x, T1) # \ \ t : T2" using ty fc apply(cases) +using [[simproc del: alpha_lst]] apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff) apply(auto simp add: Abs1_eq_iff) apply(rotate_tac 3) apply(drule_tac p="(x \ xa)" in permute_boolI) apply(perm_simp) -apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) +apply(auto simp add: flip_fresh_fresh ty_fresh) done