author urbanc Wed, 28 Mar 2007 18:25:23 +0200 changeset 22541 c33b542394f3 parent 22540 e4817fa0f6a1 child 22542 8279a25ad0ae
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
 src/HOL/Nominal/Examples/Compile.thy file | annotate | diff | comparison | revisions src/HOL/Nominal/Examples/Fsub.thy file | annotate | diff | comparison | revisions src/HOL/Nominal/Examples/SN.thy file | annotate | diff | comparison | revisions src/HOL/Nominal/Examples/SOS.thy file | annotate | diff | comparison | revisions src/HOL/Nominal/nominal_permeq.ML file | annotate | diff | comparison | revisions src/HOL/Nominal/nominal_thmdecls.ML file | annotate | diff | comparison | revisions
```--- 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\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>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:```
```--- 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\<bullet>(domain \<Gamma>) = domain (pi\<bullet>\<Gamma>)"
and   "pi'\<bullet>(domain \<Gamma>) = domain (pi'\<bullet>\<Gamma>)"
-  by (induct \<Gamma>) (simp_all add: eqvt)
+  by (induct \<Gamma>) (simp_all add: eqvts)

lemma finite_domain:
shows "finite (domain \<Gamma>)"```
```--- 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: ```
```--- 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)
done

lemma  b_CaseL_elim[elim]:
@@ -564,7 +564,7 @@
apply(drule meta_mp)
apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt')
apply(assumption)
apply(drule_tac x="[(x\<^isub>1,x\<^isub>1')]\<bullet>e'" in meta_spec)
apply(drule meta_mp)
@@ -572,7 +572,7 @@
apply(drule meta_mp)
apply(rule_tac pi="[(x\<^isub>1,x\<^isub>1')]" in big_eqvt')
apply(assumption)
done

@@ -593,7 +593,7 @@
apply(drule meta_mp)
apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt')
apply(assumption)
apply(drule_tac x="[(x\<^isub>2,x\<^isub>2')]\<bullet>e'" in meta_spec)
apply(drule meta_mp)
@@ -601,7 +601,7 @@
apply(drule meta_mp)
apply(rule_tac pi="[(x\<^isub>2,x\<^isub>2')]" in big_eqvt')
apply(assumption)
done

@@ -854,7 +854,7 @@
apply(rule_tac x="pi\<bullet>v'" in exI)
apply(auto)
apply(drule_tac pi="pi" in big_eqvt)
done

lemma V_arrow_elim_weak[elim] :
@@ -887,7 +887,7 @@
apply(rule_tac x="[(a,a')]\<bullet>v'" in exI)
apply(auto)
apply(drule_tac pi="[(a,a')]" in big_eqvt)
(*A*)
apply(rule exists_fresh')```
```--- 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 *)```
```--- 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 @@