# HG changeset patch # User berghofe # Date 1175102171 -7200 # Node ID 8279a25ad0ae49ae11616de229f170a54ef7a79d # Parent c33b542394f3fdfd6e36c41632b300fca410b572 - Renamed _eqvt to .eqvt - Renamed induct_weak to weak_induct diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/CR.thy --- 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*} diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/Class.thy --- 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)" diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/Crary.thy --- 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\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 "(\ T\<^isub>1 T\<^isub>2. T=T\<^isub>1\T\<^isub>2) \ T=TUnit \ 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\(\,t,u)" and "(y,T\<^isub>1)#\ \ App t (Var y) \ App u (Var y) : T\<^isub>2" using h by auto then have "([(x,y)]\((y,T\<^isub>1)#\)) \ [(x,y)]\ App t (Var y) \ [(x,y)]\ 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 diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/Fsub.thy --- 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\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 diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/SN.thy --- 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: "\\ \ Lam [a].t : \;a\\\\ \\ \'. \=\\\' \ ((a,\)#\) \ t : \'" apply(ind_cases2 "\ \ Lam [a].t : \") 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)\\ = \")(*A*) apply(force simp add: calc_atm) diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/SOS.thy --- 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\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\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 "\ \ t : T" @@ -311,7 +311,7 @@ then have fs: "c\\" "c\x" "c\x'" "c\t" "c\t'" by (simp_all add: fresh_atm[symmetric]) then have b5: "[(x',c)]\t'=[(x,c)]\t" using b3 fs by (simp add: alpha') have "([(x,c)]\[(x',c)]\((x',T\<^isub>1)#\)) \ ([(x,c)]\[(x',c)]\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)#\ \ 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 \ 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\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')]\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*)