Renamed inductive2 to inductive.
--- a/src/HOL/Bali/AxSem.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy Wed Jul 11 11:16:34 2007 +0200
@@ -476,7 +476,7 @@
change_claset (fn cs => cs delSWrapper "split_all_tac");
*}
-inductive2
+inductive
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
for G :: prog
--- a/src/HOL/Bali/DeclConcepts.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Jul 11 11:16:34 2007 +0200
@@ -541,7 +541,7 @@
below
*)
-inductive2
+inductive
members :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile> _ member'_of _" [61,61,61] 60)
for G :: prog
@@ -634,7 +634,7 @@
text {* Static overriding (used during the typecheck of the compiler) *}
-inductive2
+inductive
stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60)
for G :: prog
@@ -653,7 +653,7 @@
text {* Dynamic overriding (used during the typecheck of the compiler) *}
-inductive2
+inductive
overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
("_ \<turnstile> _ overrides _" [61,61,61] 60)
for G :: prog
@@ -784,7 +784,7 @@
\end{itemize}
*}
-inductive2
+inductive
accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
and accessible_from :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60)
@@ -828,7 +828,7 @@
"G\<turnstile>Field fn f of C accessible_from accclass"
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass"
-inductive2
+inductive
dyn_accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
and dyn_accessible_from' :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60)
--- a/src/HOL/Bali/DefiniteAssignment.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Wed Jul 11 11:16:34 2007 +0200
@@ -533,7 +533,7 @@
distinguish boolean and other expressions.
*}
-inductive2
+inductive
da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
where
Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
@@ -823,7 +823,7 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases2 da_elim_cases [cases set]:
+inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A"
"Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A"
--- a/src/HOL/Bali/Eval.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Eval.thy Wed Jul 11 11:16:34 2007 +0200
@@ -474,7 +474,7 @@
section "evaluation judgments"
-inductive2
+inductive
halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
where --{* allocating objects on the heap, cf. 12.5 *}
@@ -487,7 +487,7 @@
\<Longrightarrow>
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
-inductive2 sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
+inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
where --{* allocating exception objects for
standard exceptions (other than OutOfMemory) *}
@@ -503,7 +503,7 @@
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
-inductive2
+inductive
eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')" [61,61,80,0,0]60)
and exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60)
and evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
@@ -765,17 +765,17 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
-inductive_cases2 halloc_elim_cases:
+inductive_cases halloc_elim_cases:
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
-inductive_cases2 sxalloc_elim_cases:
+inductive_cases sxalloc_elim_cases:
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
-inductive_cases2 sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
+inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;
@@ -793,9 +793,9 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases2 eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
+inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
-inductive_cases2 eval_elim_cases [cases set]:
+inductive_cases eval_elim_cases [cases set]:
"G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> (v, s')"
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> (x, s')"
"G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<rightarrow> (x, s')"
--- a/src/HOL/Bali/Evaln.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy Wed Jul 11 11:16:34 2007 +0200
@@ -28,7 +28,7 @@
for welltyped, and definitely assigned terms.
*}
-inductive2
+inductive
evaln :: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
@@ -201,9 +201,9 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
+inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
-inductive_cases2 evaln_elim_cases:
+inductive_cases evaln_elim_cases:
"G\<turnstile>(Some xc, s) \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (v, s')"
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<midarrow>n\<rightarrow> (x, s')"
"G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<midarrow>n\<rightarrow> (x, s')"
--- a/src/HOL/Bali/Trans.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/Trans.thy Wed Jul 11 11:16:34 2007 +0200
@@ -68,7 +68,7 @@
"Ref a" == "Lit (Addr a)"
"SKIP" == "Lit Unit"
-inductive2
+inductive
step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
for G :: prog
where
--- a/src/HOL/Bali/TypeRel.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy Wed Jul 11 11:16:34 2007 +0200
@@ -351,7 +351,7 @@
done
-inductive2 --{* implementation, cf. 8.1.4 *}
+inductive --{* implementation, cf. 8.1.4 *}
implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
for G :: prog
where
@@ -385,7 +385,7 @@
section "widening relation"
-inductive2
+inductive
--{*widening, viz. method invocation conversion, cf. 5.3
i.e. kind of syntactic subtyping *}
widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
@@ -407,14 +407,14 @@
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
*)
lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
-apply (ind_cases2 "G\<turnstile>PrimT x\<preceq>T")
+apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
by auto
(* too strong in general:
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
*)
lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
-apply (ind_cases2 "G\<turnstile>S\<preceq>PrimT x")
+apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
by auto
text {*
@@ -424,37 +424,37 @@
*}
lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
-by (ind_cases2 "G\<turnstile>PrimT x\<preceq>T") simp_all
+by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all
lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
-by (ind_cases2 "G\<turnstile>S\<preceq>PrimT x") simp_all
+by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all
text {* Specialized versions for booleans also would work for real Java *}
lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
-by (ind_cases2 "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
+by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
-by (ind_cases2 "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
+by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
+apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
by auto
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
+apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
by auto
lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
-apply (ind_cases2 "G\<turnstile>Iface I\<preceq>T")
+apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
by auto
lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
-apply (ind_cases2 "G\<turnstile>S\<preceq> Iface J")
+apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
by auto
lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
-apply (ind_cases2 "G\<turnstile>Iface I\<preceq> Iface J")
+apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
by auto
lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
@@ -464,15 +464,15 @@
done
lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow> (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
+apply (ind_cases "G\<turnstile>Class C\<preceq>T")
by auto
lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
-apply (ind_cases2 "G\<turnstile>S\<preceq> Class C")
+apply (ind_cases "G\<turnstile>S\<preceq> Class C")
by auto
lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq> Class cm")
+apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
by auto
lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
@@ -482,7 +482,7 @@
done
lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
-apply (ind_cases2 "G\<turnstile>Class C\<preceq> Iface I")
+apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
by auto
lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
@@ -492,21 +492,21 @@
done
lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
-apply (ind_cases2 "G\<turnstile>S.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
by auto
lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
-apply (ind_cases2 "G\<turnstile>S\<preceq>T.[]")
+apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
by auto
lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
-apply (ind_cases2 "G\<turnstile>PrimT t.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
by auto
lemma widen_ArrayRefT:
"G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
-apply (ind_cases2 "G\<turnstile>RefT t.[]\<preceq>T")
+apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
by auto
lemma widen_ArrayRefT_ArrayRefT_eq [simp]:
@@ -527,7 +527,7 @@
lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
-apply (ind_cases2 "G\<turnstile>S\<preceq>NT")
+apply (ind_cases "G\<turnstile>S\<preceq>NT")
by auto
lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
@@ -610,7 +610,7 @@
*)
(* more detailed than necessary for type-safety, see above rules. *)
-inductive2 --{* narrowing reference conversion, cf. 5.1.5 *}
+inductive --{* narrowing reference conversion, cf. 5.1.5 *}
narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
for G :: prog
where
@@ -625,20 +625,20 @@
(*unused*)
lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<succ>T")
+apply (ind_cases "G\<turnstile>RefT R\<succ>T")
by auto
lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<succ>RefT R")
+apply (ind_cases "G\<turnstile>S\<succ>RefT R")
by auto
(*unused*)
lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
-by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
+by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>
\<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
+by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
text {*
These narrowing lemmata hold in Bali but are to strong for ordinary
@@ -646,22 +646,22 @@
long, int. These lemmata are just for documentation and are not used.
*}
lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
-by (ind_cases2 "G\<turnstile>PrimT pt\<succ>T")
+by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT pt")
+by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
text {* Specialized versions for booleans also would work for real Java *}
lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
-by (ind_cases2 "G\<turnstile>PrimT Boolean\<succ>T")
+by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
-by (ind_cases2 "G\<turnstile>S\<succ>PrimT Boolean")
+by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
section "casting relation"
-inductive2 --{* casting conversion, cf. 5.5 *}
+inductive --{* casting conversion, cf. 5.5 *}
cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
for G :: prog
where
@@ -670,20 +670,20 @@
(*unused*)
lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
-apply (ind_cases2 "G\<turnstile>RefT R\<preceq>? T")
+apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
by (auto dest: widen_RefT narrow_RefT)
lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
-apply (ind_cases2 "G\<turnstile>S\<preceq>? RefT R")
+apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
by (auto dest: widen_RefT2 narrow_RefT2)
(*unused*)
lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
-apply (ind_cases2 "G\<turnstile>PrimT pt\<preceq>? T")
+apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
by (auto dest: widen_PrimT narrow_PrimT)
lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
-apply (ind_cases2 "G\<turnstile>S\<preceq>? PrimT pt")
+apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
by (auto dest: widen_PrimT2 narrow_PrimT2)
lemma cast_Boolean:
--- a/src/HOL/Bali/WellType.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Bali/WellType.thy Wed Jul 11 11:16:34 2007 +0200
@@ -246,7 +246,7 @@
"tys" <= (type) "ty + ty list"
-inductive2
+inductive
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
@@ -456,7 +456,7 @@
change_simpset (fn ss => ss delloop "split_all_tac")
*}
-inductive_cases2 wt_elim_cases [cases set]:
+inductive_cases wt_elim_cases [cases set]:
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T"
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T"
--- a/src/HOL/Extraction/Higman.thy Wed Jul 11 11:14:51 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy Wed Jul 11 11:16:34 2007 +0200
@@ -15,37 +15,37 @@
datatype letter = A | B
-inductive2 emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
+inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
where
emb0 [Pure.intro]: "emb [] bs"
| emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
| emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
-inductive2 L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
for v :: "letter list"
where
L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
| L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
-inductive2 good :: "letter list list \<Rightarrow> bool"
+inductive good :: "letter list list \<Rightarrow> bool"
where
good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
| good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
-inductive2 R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
for a :: letter
where
R0 [Pure.intro]: "R a [] []"
| R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
-inductive2 T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
+inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
for a :: letter
where
T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
| T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
| T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
-inductive2 bar :: "letter list list \<Rightarrow> bool"
+inductive bar :: "letter list list \<Rightarrow> bool"
where
bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
| bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"