--- a/src/HOL/Nominal/Examples/Crary.thy Thu Jun 21 13:23:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Thu Jun 21 13:49:27 2007 +0200
@@ -319,12 +319,13 @@
declare trm.inject [simp add]
declare ty.inject [simp add]
-inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
-inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
-inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
-inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
-inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
-inductive_cases2 t_Unit_elim_auto'[elim]: "\<Gamma> \<turnstile> s : TUnit"
+inductive_cases2 t_inv_auto[elim]:
+ "\<Gamma> \<turnstile> Lam [x].t : T"
+ "\<Gamma> \<turnstile> Var x : T"
+ "\<Gamma> \<turnstile> App x y : T"
+ "\<Gamma> \<turnstile> Const n : T"
+ "\<Gamma> \<turnstile> Unit : TUnit"
+ "\<Gamma> \<turnstile> s : TUnit"
declare trm.inject [simp del]
declare ty.inject [simp del]
@@ -366,15 +367,16 @@
declare trm.inject [simp add]
declare ty.inject [simp add]
-inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'"
-inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'"
-inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t"
-inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t"
-inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t"
-inductive_cases2 whr_App[elim]: "App p q \<leadsto> t"
-inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n"
-inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x"
-inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q"
+inductive_cases2 whr_inv_auto[elim]:
+ "t \<leadsto> t'"
+ "Lam [x].t \<leadsto> t'"
+ "App (Lam [x].t12) t2 \<leadsto> t"
+ "Var x \<leadsto> t"
+ "Const n \<leadsto> t"
+ "App p q \<leadsto> t"
+ "t \<leadsto> Const n"
+ "t \<leadsto> Var x"
+ "t \<leadsto> App p q"
declare trm.inject [simp del]
declare ty.inject [simp del]
@@ -421,12 +423,12 @@
shows "a=b"
using a b
apply (induct arbitrary: b)
-apply (erule whr_App_Lam)
+apply (erule whr_inv_auto(3))
apply (clarify)
apply (rule subst_fun_eq)
apply (simp)
apply (force)
-apply (erule whr_App)
+apply (erule whr_inv_auto(6))
apply (blast)+
done
@@ -468,23 +470,24 @@
declare trm.inject [simp add]
declare ty.inject [simp add]
-inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
-inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
-
-inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
-inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
-inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+inductive_cases2 alg_equiv_inv_auto[elim]:
+ "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
+ "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
-inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
-inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
-inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
-inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
-inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
-inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
-inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
-inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
-inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
-inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
+inductive_cases2 alg_path_equiv_inv_auto[elim]:
+ "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
+ "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
+ "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+ "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
+ "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
+ "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
+ "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
+ "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
+ "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
+ "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
+ "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
+ "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
+ "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
declare trm.inject [simp del]
declare ty.inject [simp del]
--- a/src/HOL/Nominal/Examples/SOS.thy Thu Jun 21 13:23:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy Thu Jun 21 13:49:27 2007 +0200
@@ -286,19 +286,21 @@
declare ty.inject [simp add]
declare data.inject [simp add]
-inductive_cases2 t_Lam_inv_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
-inductive_cases2 t_Var_inv_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
-inductive_cases2 t_App_inv_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
-inductive_cases2 t_Const_inv_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
-inductive_cases2 t_Fst_inv_auto[elim]: "\<Gamma> \<turnstile> Fst x : T"
-inductive_cases2 t_Snd_inv_auto[elim]: "\<Gamma> \<turnstile> Snd x : T"
-inductive_cases2 t_InL_inv_auto[elim]: "\<Gamma> \<turnstile> InL x : T"
-inductive_cases2 t_InL_inv_auto'[elim]: "\<Gamma> \<turnstile> InL x : Data (DSum T\<^isub>1 T2)"
-inductive_cases2 t_InR_inv_auto[elim]: "\<Gamma> \<turnstile> InR x : T"
-inductive_cases2 t_InR_inv_auto'[elim]: "\<Gamma> \<turnstile> InR x : Data (DSum T\<^isub>1 T2)"
-inductive_cases2 t_Pr_inv_auto[elim]: "\<Gamma> \<turnstile> Pr x y : T"
-inductive_cases2 t_Pr_inv_auto'[elim]: "\<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd \<sigma>1 \<sigma>\<^isub>2)"
-inductive_cases2 t_Case_inv_auto[elim]: "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T"
+
+inductive_cases2 typing_inv_auto[elim]:
+ "\<Gamma> \<turnstile> Lam [x].t : T"
+ "\<Gamma> \<turnstile> Var x : T"
+ "\<Gamma> \<turnstile> App x y : T"
+ "\<Gamma> \<turnstile> Const n : T"
+ "\<Gamma> \<turnstile> Fst x : T"
+ "\<Gamma> \<turnstile> Snd x : T"
+ "\<Gamma> \<turnstile> InL x : T"
+ "\<Gamma> \<turnstile> InL x : Data (DSum T\<^isub>1 T2)"
+ "\<Gamma> \<turnstile> InR x : T"
+ "\<Gamma> \<turnstile> InR x : Data (DSum T\<^isub>1 T2)"
+ "\<Gamma> \<turnstile> Pr x y : T"
+ "\<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd \<sigma>1 \<sigma>\<^isub>2)"
+ "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T"
declare trm.inject [simp del]
declare ty.inject [simp del]
@@ -528,15 +530,16 @@
declare ty.inject [simp add]
declare data.inject [simp add]
-inductive_cases2 b_App_inv_auto[elim]: "App e\<^isub>1 e\<^isub>2 \<Down> t"
-inductive_cases2 b_Case_inv_auto[elim]: "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t"
-inductive_cases2 b_Lam_inv_auto[elim]: "Lam[x].t \<Down> t"
-inductive_cases2 b_Const_inv_auto[elim]: "Const n \<Down> t"
-inductive_cases2 b_Fst_inv_auto[elim]: "Fst e \<Down> t"
-inductive_cases2 b_Snd_inv_auto[elim]: "Snd e \<Down> t"
-inductive_cases2 b_InL_inv_auto[elim]: "InL e \<Down> t"
-inductive_cases2 b_InR_inv_auto[elim]: "InR e \<Down> t"
-inductive_cases2 b_Pr_inv_auto[elim]: "Pr e\<^isub>1 e\<^isub>2 \<Down> t"
+inductive_cases2 b_inv_auto[elim]:
+ "App e\<^isub>1 e\<^isub>2 \<Down> t"
+ "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t"
+ "Lam[x].t \<Down> t"
+ "Const n \<Down> t"
+ "Fst e \<Down> t"
+ "Snd e \<Down> t"
+ "InL e \<Down> t"
+ "InR e \<Down> t"
+ "Pr e\<^isub>1 e\<^isub>2 \<Down> t"
declare trm.inject [simp del]
declare ty.inject [simp del]
@@ -547,7 +550,7 @@
obtains f\<^isub>1 and f\<^isub>2 where "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" "e\<^isub>2 \<Down> f\<^isub>2" "f\<^isub>1[x::=f\<^isub>2] \<Down> e'"
using assms
apply -
- apply(erule b_App_inv_auto)
+ apply(erule b_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)
@@ -561,7 +564,7 @@
obtains e' where "e \<Down> InL e'" and "e\<^isub>1[x\<^isub>1::=e'] \<Down> e''"
using assms
apply -
- apply(rule b_Case_inv_auto)
+ apply(rule b_inv_auto(2))
apply(auto)
apply(simp add: alpha)
apply(auto)
@@ -590,7 +593,7 @@
obtains e' where "e \<Down> InR e'" and "e\<^isub>2[x\<^isub>2::=e'] \<Down> e''"
using assms
apply -
- apply(rule b_Case_inv_auto)
+ apply(rule b_inv_auto(2))
apply(auto)
apply(simp add: alpha)
apply(auto)
@@ -625,16 +628,17 @@
declare ty.inject [simp add]
declare data.inject [simp add]
-inductive_cases2 v_Const_inv_auto[elim]: "val (Const n)"
-inductive_cases2 v_Pr_inv_auto[elim]: "val (Pr e\<^isub>1 e\<^isub>2)"
-inductive_cases2 v_InL_inv_auto[elim]: "val (InL e)"
-inductive_cases2 v_InR_inv_auto[elim]: "val (InR e)"
-inductive_cases2 v_Fst_inv_auto[elim]: "val (Fst e)"
-inductive_cases2 v_Snd_inv_auto[elim]: "val (Snd e)"
-inductive_cases2 v_Case_inv_auto[elim]: "val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)"
-inductive_cases2 v_Var_inv_auto[elim]: "val (Var x)"
-inductive_cases2 v_Lam_inv_auto[elim]: "val (Lam [x].e)"
-inductive_cases2 v_App_inv_auto[elim]: "val (App e\<^isub>1 e\<^isub>2)"
+inductive_cases2 v_inv_auto[elim]:
+ "val (Const n)"
+ "val (Pr e\<^isub>1 e\<^isub>2)"
+ "val (InL e)"
+ "val (InR e)"
+ "val (Fst e)"
+ "val (Snd e)"
+ "val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)"
+ "val (Var x)"
+ "val (Lam [x].e)"
+ "val (App e\<^isub>1 e\<^isub>2)"
declare trm.inject [simp del]
declare ty.inject [simp del]