# HG changeset patch # User urbanc # Date 1175099123 -7200 # Node ID c33b542394f3fdfd6e36c41632b300fca410b572 # Parent e4817fa0f6a18abb4b28fd0d8af7f69d67b6aed8 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/Examples/Compile.thy --- a/src/HOL/Nominal/Examples/Compile.thy Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/Examples/Compile.thy Wed Mar 28 18:25:23 2007 +0200 @@ -130,7 +130,7 @@ and x::"name" shows "pi\(t1[x::=t2]) = ((pi\t1)[(pi\x)::=(pi\t2)])" apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct) - apply (simp_all add: Isubst.simps eqvt fresh_bij) + apply (simp_all add: Isubst.simps eqvts fresh_bij) done lemma Isubst_supp: diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Mar 28 18:25:23 2007 +0200 @@ -92,7 +92,7 @@ and pi'::"vrs prm" shows "pi\(domain \) = domain (pi\\)" and "pi'\(domain \) = domain (pi'\\)" - by (induct \) (simp_all add: eqvt) + by (induct \) (simp_all add: eqvts) lemma finite_domain: shows "finite (domain \)" diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/Examples/SN.thy --- a/src/HOL/Nominal/Examples/SN.thy Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/Examples/SN.thy Wed Mar 28 18:25:23 2007 +0200 @@ -93,7 +93,7 @@ apply(rule conjI) apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm) apply(force dest!: supp_beta simp add: fresh_def) -apply(force intro!: eqvt) +apply(force intro!: eqvts) done lemma beta_subst: diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/Examples/SOS.thy --- a/src/HOL/Nominal/Examples/SOS.thy Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/Examples/SOS.thy Wed Mar 28 18:25:23 2007 +0200 @@ -544,7 +544,7 @@ apply(drule_tac pi="[(xa,x)]" in big_eqvt) apply(drule_tac pi="[(xa,x)]" in big_eqvt) apply(drule_tac pi="[(xa,x)]" in big_eqvt) - apply(perm_simp add: calc_atm eqvt) + apply(perm_simp add: calc_atm eqvts) done lemma b_CaseL_elim[elim]: @@ -564,7 +564,7 @@ apply(perm_simp add: fresh_prod) apply(drule meta_mp) apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') - apply(perm_simp add: eqvt calc_atm) + apply(perm_simp add: eqvts calc_atm) apply(assumption) apply(drule_tac x="[(x\<^isub>1,x\<^isub>1')]\e'" in meta_spec) apply(drule meta_mp) @@ -572,7 +572,7 @@ apply(perm_simp add: fresh_prod) apply(drule meta_mp) apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt') - apply(perm_simp add: eqvt calc_atm) + apply(perm_simp add: eqvts calc_atm) apply(assumption) done @@ -593,7 +593,7 @@ apply(perm_simp add: fresh_prod) apply(drule meta_mp) apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') - apply(perm_simp add: eqvt calc_atm) + apply(perm_simp add: eqvts calc_atm) apply(assumption) apply(drule_tac x="[(x\<^isub>2,x\<^isub>2')]\e'" in meta_spec) apply(drule meta_mp) @@ -601,7 +601,7 @@ apply(perm_simp add: fresh_prod) apply(drule meta_mp) apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt') - apply(perm_simp add: eqvt calc_atm) + apply(perm_simp add: eqvts calc_atm) apply(assumption) done @@ -854,7 +854,7 @@ apply(rule_tac x="pi\v'" in exI) apply(auto) apply(drule_tac pi="pi" in big_eqvt) -apply(perm_simp add: eqvt) +apply(perm_simp add: eqvts) done lemma V_arrow_elim_weak[elim] : @@ -887,7 +887,7 @@ apply(rule_tac x="[(a,a')]\v'" in exI) apply(auto) apply(drule_tac pi="[(a,a')]" in big_eqvt) -apply(perm_simp add: eqvt calc_atm) +apply(perm_simp add: eqvts calc_atm) apply(simp add: V_eqvt) (*A*) apply(rule exists_fresh') diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Mar 28 18:25:23 2007 +0200 @@ -151,7 +151,7 @@ (* general simplification of permutations and permutation that arose from eqvt-problems *) val perm_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp"]; -val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvt"]; +val eqvt_simp = perm_simp_gen ["perm_swap","perm_fresh_fresh","perm_pi_simp","eqvts"]; (* main simplification tactics for permutations *) (* FIXME: perm_simp_tac should simplify more permutations *) diff -r e4817fa0f6a1 -r c33b542394f3 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 28 17:27:44 2007 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Mar 28 18:25:23 2007 +0200 @@ -30,10 +30,10 @@ structure Data = GenericDataFun ( val name = "HOL/Nominal/eqvt"; - type T = {eqvt:thm list, fresh:thm list, bij:thm list}; - val empty = ({eqvt=[], fresh=[], bij=[]}:T); + type T = {eqvts:thm list, fresh:thm list, bij:thm list}; + val empty = ({eqvts=[], fresh=[], bij=[]}:T); val extend = I; - fun merge _ (r1:T,r2:T) = {eqvt = Drule.merge_rules (#eqvt r1, #eqvt r2), + fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2), fresh = Drule.merge_rules (#fresh r1, #fresh r2), bij = Drule.merge_rules (#bij r1, #bij r2)} fun print context (data:T) = @@ -42,7 +42,7 @@ Pretty.writeln (Pretty.big_list msg (map (ProofContext.pretty_thm (Context.proof_of context)) thms)) in - (print_aux "Equivariance lemmas: " (#eqvt data); + (print_aux "Equivariance lemmas: " (#eqvts data); print_aux "Freshness lemmas: " (#fresh data); print_aux "Bijection lemmas: " (#bij data)) end; @@ -61,7 +61,7 @@ exception EQVT_FORM of string; val print_data = Data.print o Context.Proof; -val get_eqvt_thms = Context.Theory #> Data.get #> #eqvt; +val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts; val get_fresh_thms = Context.Theory #> Data.get #> #fresh; val get_bij_thms = Context.Theory #> Data.get #> #bij; @@ -111,7 +111,7 @@ let val context' = fold (fn thm => Data.map (flag thm)) thms context in - Context.mapping (snd o PureThy.add_thmss [(("eqvt",(#eqvt (Data.get context'))),[])]) I context' + Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context' end; (* replaces every variable x in t with pi o x *) @@ -197,11 +197,11 @@ fun bij_add_del_aux f = simple_add_del_aux #bij "bij" f fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f -fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvt "eqvt" f +fun eqvt_force_add_del_aux f = simple_add_del_aux #eqvts "eqvts" f -fun eqvt_map f th (r:Data.T) = {eqvt = (f th (#eqvt r)), fresh = #fresh r, bij = #bij r}; -fun fresh_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = (f th (#fresh r)), bij = #bij r}; -fun bij_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = #fresh r, bij = (f th (#bij r))}; +fun eqvt_map f th (r:Data.T) = {eqvts = (f th (#eqvts r)), fresh = #fresh r, bij = #bij r}; +fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = (f th (#fresh r)), bij = #bij r}; +fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, fresh = #fresh r, bij = (f th (#bij r))}; val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));