Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
- Renamed <predicate>_eqvt to <predicate>.eqvt
authorberghofe
Wed, 28 Mar 2007 19:16:11 +0200
changeset 22542 8279a25ad0ae
parent 22541 c33b542394f3
child 22543 9460a4cf0acc
- Renamed <predicate>_eqvt to <predicate>.eqvt - Renamed induct_weak to weak_induct
src/HOL/Nominal/Examples/CR.thy file | annotate | diff | comparison | revisions
src/HOL/Nominal/Examples/Class.thy file | annotate | diff | comparison | revisions
src/HOL/Nominal/Examples/Crary.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 
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -271,7 +271,7 @@
   apply(rule conjI)
   apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
   apply(simp add: calc_atm)
-  apply(force intro!: One_eqvt)
+  apply(force intro!: One.eqvt)
   done
 
 lemma one_app: 
@@ -314,7 +314,7 @@
   apply(simp add: subst_rename)
   (*A*)
   apply(force intro: one_fresh_preserv)
-  apply(force intro: One_eqvt)
+  apply(force intro: One.eqvt)
   done
 
 text {* first case in Lemma 3.2.4*}
--- a/src/HOL/Nominal/Examples/Class.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -35,7 +35,7 @@
 
 text {* Induction principles *}
 
-thm trm.induct_weak --"weak"
+thm trm.weak_induct --"weak"
 thm trm.induct      --"strong"
 thm trm.induct'     --"strong with explicit context (rarely needed)"
 
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -32,7 +32,7 @@
   fixes T::"ty"
   and   pi::"name prm"
   shows "pi\<bullet>T = T"
-  by (induct T rule: ty.induct_weak) (simp_all)
+  by (induct T rule: ty.weak_induct) (simp_all)
 
 lemma fresh_ty[simp]:
   fixes x::"name" 
@@ -43,7 +43,7 @@
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
-by (induct T rule:ty.induct_weak) (auto)
+by (induct T rule:ty.weak_induct) (auto)
 
 instance ty :: size ..
 
@@ -399,11 +399,11 @@
 using a
 apply(induct)
 apply(rule QAN_Reduce)
-apply(rule whr_def_eqvt)
+apply(rule whr_def.eqvt)
 apply(assumption)+
 apply(rule QAN_Normal)
 apply(auto)
-apply(drule_tac pi="rev pi" in whr_def_eqvt)
+apply(drule_tac pi="rev pi" in whr_def.eqvt)
 apply(perm_simp)
 done
 
@@ -494,7 +494,7 @@
   obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
     using h by auto
   then have "([(x,y)]\<bullet>((y,T\<^isub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^isub>2" 
-    using  alg_equiv_eqvt[simplified] by blast
+    using  alg_equiv.eqvt[simplified] by blast
   then show ?thesis using fs fs2 by (perm_simp)
 qed
 
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -159,7 +159,7 @@
   fixes pi::"vrs prm"
   and   S::"ty"
   shows "pi\<bullet>S = S"
-by (induct S rule: ty.induct_weak) (auto simp add: calc_atm)
+by (induct S rule: ty.weak_induct) (auto simp add: calc_atm)
 
 lemma ty_context_vrs_prm_simp:
   fixes pi::"vrs prm"
@@ -530,7 +530,7 @@
   apply(drule_tac X="Xa" in subtype_implies_fresh)
   apply(assumption)
   apply(simp add: fresh_prod)
-  apply(drule_tac pi="[(X,Xa)]" in subtype_of_eqvt(2))
+  apply(drule_tac pi="[(X,Xa)]" in subtype_of.eqvt(2))
   apply(simp add: calc_atm)
   apply(simp add: pt_fresh_fresh[OF pt_tyvrs_inst, OF at_tyvrs_inst])
   done
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -211,7 +211,7 @@
 lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
 apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
 apply(auto simp add: lam.distinct lam.inject alpha) 
-apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt)
+apply(drule_tac pi="[(a,aa)]::name prm" in typing.eqvt)
 apply(simp)
 apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
 apply(force simp add: calc_atm)
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -46,13 +46,13 @@
   fixes D::"data"
   and   pi::"name prm"
   shows "pi\<bullet>D = D"
-  by (induct D rule: data.induct_weak) (simp_all)
+  by (induct D rule: data.weak_induct) (simp_all)
 
 lemma perm_ty[simp]: 
   fixes T::"ty"
   and   pi::"name prm"
   shows "pi\<bullet>T = T"
-  by (induct T rule: ty.induct_weak) (simp_all)
+  by (induct T rule: ty.weak_induct) (simp_all)
 
 lemma fresh_ty[simp]:
   fixes x::"name" 
@@ -269,7 +269,7 @@
 nominal_inductive typing
   by (simp_all add: abs_fresh fresh_prod fresh_atm)
 
-lemmas typing_eqvt' = typing_eqvt[simplified]
+lemmas typing_eqvt' = typing.eqvt[simplified]
 
 lemma typing_implies_valid:
   assumes "\<Gamma> \<turnstile> t : T"
@@ -311,7 +311,7 @@
   then have fs: "c\<sharp>\<Gamma>" "c\<noteq>x" "c\<noteq>x'" "c\<sharp>t" "c\<sharp>t'" by (simp_all add: fresh_atm[symmetric]) 
   then have b5: "[(x',c)]\<bullet>t'=[(x,c)]\<bullet>t" using b3 fs by (simp add: alpha')
   have "([(x,c)]\<bullet>[(x',c)]\<bullet>((x',T\<^isub>1)#\<Gamma>)) \<turnstile> ([(x,c)]\<bullet>[(x',c)]\<bullet>t') : T\<^isub>2" using b2
-    by (simp only: typing_eqvt[simplified perm_ty])
+    by (simp only: typing_eqvt')
   then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2" using fs b1 a2 b5 by (perm_simp add: calc_atm)
   then show ?thesis using prems b4 by simp
 qed
@@ -505,7 +505,7 @@
   shows "t \<Down> t'"
 using a
 apply -
-apply(drule_tac pi="rev pi" in big_eqvt)
+apply(drule_tac pi="rev pi" in big.eqvt)
 apply(perm_simp)
 done
 
@@ -541,9 +541,9 @@
   using assms
   apply -
   apply(erule b_App_inv_auto)
-  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(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 eqvts)
   done
 
@@ -853,7 +853,7 @@
 apply(auto)
 apply(rule_tac x="pi\<bullet>v'" in exI)
 apply(auto)
-apply(drule_tac pi="pi" in big_eqvt)
+apply(drule_tac pi="pi" in big.eqvt)
 apply(perm_simp add: eqvts)
 done
 
@@ -886,7 +886,7 @@
 apply(auto)
 apply(rule_tac x="[(a,a')]\<bullet>v'" in exI)
 apply(auto)
-apply(drule_tac pi="[(a,a')]" in big_eqvt)
+apply(drule_tac pi="[(a,a')]" in big.eqvt)
 apply(perm_simp add: eqvts calc_atm)
 apply(simp add: V_eqvt)
 (*A*)
isabelle