undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
authornarboux
Tue Jul 31 14:45:36 2007 +0200 (2007-07-31)
changeset 24088c2d8270e53a5
parent 24087 eb025d149a34
child 24089 070d539ba403
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
src/HOL/Nominal/Examples/Crary.thy
     1.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Tue Jul 31 14:18:24 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Jul 31 14:45:36 2007 +0200
     1.3 @@ -42,8 +42,6 @@
     1.4    shows "x\<sharp>T"
     1.5    by (simp add: fresh_def supp_def)
     1.6  
     1.7 -
     1.8 -
     1.9  lemma ty_cases:
    1.10    fixes T::ty
    1.11    shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
    1.12 @@ -318,20 +316,20 @@
    1.13    shows "valid \<Gamma>"
    1.14    using a by (induct) (auto)
    1.15  
    1.16 -(*
    1.17  declare trm.inject [simp add]
    1.18  declare ty.inject  [simp add]
    1.19  
    1.20 -inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
    1.21 -inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
    1.22 -inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
    1.23 -inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
    1.24 -inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
    1.25 -inductive_cases2 t_Unit_elim_auto'[elim]: "\<Gamma> \<turnstile> s : TUnit"
    1.26 +inductive_cases typing_inv_auto[elim]:
    1.27 +  "\<Gamma> \<turnstile> Lam [x].t : T"
    1.28 +  "\<Gamma> \<turnstile> Var x : T"
    1.29 +  "\<Gamma> \<turnstile> App x y : T"
    1.30 +  "\<Gamma> \<turnstile> Const n : T"
    1.31 +  "\<Gamma> \<turnstile> Unit : TUnit"
    1.32 +  "\<Gamma> \<turnstile> s : TUnit"
    1.33  
    1.34  declare trm.inject [simp del]
    1.35  declare ty.inject [simp del]
    1.36 -*)
    1.37 +
    1.38  
    1.39  section {* Definitional Equivalence *}
    1.40  
    1.41 @@ -490,15 +488,16 @@
    1.42  declare trm.inject  [simp add]
    1.43  declare ty.inject  [simp add]
    1.44  
    1.45 -inductive_cases whr_Gen[elim]: "t \<leadsto> t'"
    1.46 -inductive_cases whr_Lam[elim]: "Lam [x].t \<leadsto> t'"
    1.47 -inductive_cases whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t"
    1.48 -inductive_cases whr_Var[elim]: "Var x \<leadsto> t"
    1.49 -inductive_cases whr_Const[elim]: "Const n \<leadsto> t"
    1.50 -inductive_cases whr_App[elim]: "App p q \<leadsto> t"
    1.51 -inductive_cases whr_Const_Right[elim]: "t \<leadsto> Const n"
    1.52 -inductive_cases whr_Var_Right[elim]: "t \<leadsto> Var x"
    1.53 -inductive_cases whr_App_Right[elim]: "t \<leadsto> App p q"
    1.54 +inductive_cases whr_inv_auto[elim]: 
    1.55 +  "t \<leadsto> t'"
    1.56 +  "Lam [x].t \<leadsto> t'"
    1.57 +  "App (Lam [x].t12) t2 \<leadsto> t"
    1.58 +  "Var x \<leadsto> t"
    1.59 +  "Const n \<leadsto> t"
    1.60 +  "App p q \<leadsto> t"
    1.61 +  "t \<leadsto> Const n"
    1.62 +  "t \<leadsto> Var x"
    1.63 +  "t \<leadsto> App p q"
    1.64  
    1.65  declare trm.inject  [simp del]
    1.66  declare ty.inject  [simp del]
    1.67 @@ -545,12 +544,12 @@
    1.68    shows "a=b"
    1.69    using a b
    1.70  apply (induct arbitrary: b)
    1.71 -apply (erule whr_App_Lam)
    1.72 +apply (erule whr_inv_auto(3))
    1.73  apply (clarify)
    1.74  apply (rule subst_fun_eq)
    1.75  apply (simp)
    1.76  apply (force)
    1.77 -apply (erule whr_App)
    1.78 +apply (erule whr_inv_auto(6))
    1.79  apply (blast)+
    1.80  done
    1.81  
    1.82 @@ -603,27 +602,26 @@
    1.83    avoids QAT_Arrow: x
    1.84    by simp_all
    1.85  
    1.86 -
    1.87  declare trm.inject [simp add]
    1.88  declare ty.inject  [simp add]
    1.89  
    1.90 -inductive_cases alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
    1.91 -inductive_cases alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
    1.92 -
    1.93 -inductive_cases alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
    1.94 -inductive_cases alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
    1.95 -inductive_cases alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
    1.96 +inductive_cases alg_equiv_inv_auto[elim]: 
    1.97 +  "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
    1.98 +  "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
    1.99 +  "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
   1.100 +  "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
   1.101 +  "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.102  
   1.103 -inductive_cases alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
   1.104 -inductive_cases alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
   1.105 -inductive_cases alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
   1.106 -inductive_cases alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
   1.107 -inductive_cases alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
   1.108 -inductive_cases alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
   1.109 -inductive_cases alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
   1.110 -inductive_cases alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
   1.111 -inductive_cases alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
   1.112 -inductive_cases alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
   1.113 +  "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
   1.114 +  "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
   1.115 +  "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
   1.116 +  "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
   1.117 +  "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
   1.118 +  "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
   1.119 +  "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
   1.120 +  "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
   1.121 +  "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
   1.122 +  "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
   1.123  
   1.124  declare trm.inject [simp del]
   1.125  declare ty.inject [simp del]