# HG changeset patch
# User berghofe
# Date 1184147661 -7200
# Node ID 18f426a137a95da28dbf0e279707f06b0ae5a854
# Parent  60b7800338d5415d5f7eb979c86e5808ad9e77ab
Adapted to new inductive definition package.

diff -r 60b7800338d5 -r 18f426a137a9 src/HOL/ex/NBE.thy
--- a/src/HOL/ex/NBE.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOL/ex/NBE.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -44,19 +44,16 @@
  and x :: lam_var_name
  and X :: ml_var_name
 
-consts Pure_tms :: "tm set"
-inductive Pure_tms
-intros
-"Ct s : Pure_tms"
-"Vt x : Pure_tms"
-"t : Pure_tms ==> Lam t : Pure_tms"
-"s : Pure_tms ==> t : Pure_tms ==> At s t : Pure_tms"
+inductive_set Pure_tms :: "tm set"
+where
+  "Ct s : Pure_tms"
+| "Vt x : Pure_tms"
+| "t : Pure_tms ==> Lam t : Pure_tms"
+| "s : Pure_tms ==> t : Pure_tms ==> At s t : Pure_tms"
 
 consts
   R :: "(const_name * tm list * tm)set" (* reduction rules *)
   compR :: "(const_name * ml list * ml)set" (* compiled reduction rules *)
-  tRed :: "(tm * tm)set" (* beta + R reduction on pure terms *)
-  tRed_list :: "(tm list * tm list) set"
 
 fun
   lift_tm :: "nat \<Rightarrow> tm \<Rightarrow> tm" ("lift") and
@@ -226,55 +223,34 @@
 apply (simp cong:if_cong)
 done
 
-abbreviation
-  tred :: "[tm, tm] => bool"  (infixl "\<rightarrow>" 50) where
+inductive_set
+  tRed :: "(tm * tm)set" (* beta + R reduction on pure terms *)
+  and tred :: "[tm, tm] => bool"  (infixl "\<rightarrow>" 50)
+where
   "s \<rightarrow> t == (s, t) \<in> tRed"
+| "At (Lam t) s \<rightarrow> t[s/0]"
+| "(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t"
+| "t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'"
+| "s \<rightarrow> s' ==> At s t \<rightarrow> At s' t"
+| "t \<rightarrow> t' ==> At s t \<rightarrow> At s t'"
+
 abbreviation
   treds :: "[tm, tm] => bool"  (infixl "\<rightarrow>*" 50) where
   "s \<rightarrow>* t == (s, t) \<in> tRed^*"
-abbreviation
-  treds_list :: "[tm list, tm list] \<Rightarrow> bool" (infixl "\<rightarrow>*" 50) where
+
+inductive_set
+  tRed_list :: "(tm list * tm list) set"
+  and treds_list :: "[tm list, tm list] \<Rightarrow> bool" (infixl "\<rightarrow>*" 50)
+where
   "ss \<rightarrow>* ts == (ss, ts) \<in> tRed_list"
-
-inductive tRed
-intros
-"At (Lam t) s \<rightarrow> t[s/0]"
-"(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t"
-"t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'"
-"s \<rightarrow> s' ==> At s t \<rightarrow> At s' t"
-"t \<rightarrow> t' ==> At s t \<rightarrow> At s t'"
-
-inductive tRed_list
-intros
-"[] \<rightarrow>* []"
-"ts \<rightarrow>* ts' ==> t \<rightarrow>* t' ==> t#ts \<rightarrow>* t'#ts'"
+| "[] \<rightarrow>* []"
+| "ts \<rightarrow>* ts' ==> t \<rightarrow>* t' ==> t#ts \<rightarrow>* t'#ts'"
 
 declare tRed_list.intros[simp]
 
 lemma tRed_list_refl[simp]: includes Vars shows "ts \<rightarrow>* ts"
 by(induct ts) auto
 
-consts
-  Red :: "(ml * ml)set"
-  Redl :: "(ml list * ml list)set"
-  Redt :: "(tm * tm)set"
-
-abbreviation
-  red :: "[ml, ml] => bool"  (infixl "\<Rightarrow>" 50) where
-  "s \<Rightarrow> t == (s, t) \<in> Red"
-abbreviation
-  redl :: "[ml list, ml list] => bool"  (infixl "\<Rightarrow>" 50) where
-  "s \<Rightarrow> t == (s, t) \<in> Redl"
-abbreviation
-  redt :: "[tm, tm] => bool"  (infixl "\<Rightarrow>" 50) where
-  "s \<Rightarrow> t == (s, t) \<in> Redt"
-abbreviation
-  reds :: "[ml, ml] => bool"  (infixl "\<Rightarrow>*" 50) where
-  "s \<Rightarrow>* t == (s, t) \<in> Red^*"
-abbreviation
-  redts :: "[tm, tm] => bool"  (infixl "\<Rightarrow>*" 50) where
-  "s \<Rightarrow>* t == (s, t) \<in> Redt^*"
-
 
 fun ML_closed :: "nat \<Rightarrow> ml \<Rightarrow> bool"
 and ML_closed_t :: "nat \<Rightarrow> tm \<Rightarrow> bool" where
@@ -292,38 +268,51 @@
 "ML_closed_t i v = True"
 thm ML_closed.simps ML_closed_t.simps
 
-inductive Red Redt Redl
-intros
+inductive_set
+  Red :: "(ml * ml)set"
+  and Redt :: "(tm * tm)set"
+  and Redl :: "(ml list * ml list)set"
+  and red :: "[ml, ml] => bool"  (infixl "\<Rightarrow>" 50)
+  and redl :: "[ml list, ml list] => bool"  (infixl "\<Rightarrow>" 50)
+  and redt :: "[tm, tm] => bool"  (infixl "\<Rightarrow>" 50)
+  and reds :: "[ml, ml] => bool"  (infixl "\<Rightarrow>*" 50)
+  and redts :: "[tm, tm] => bool"  (infixl "\<Rightarrow>*" 50)
+where
+  "s \<Rightarrow> t == (s, t) \<in> Red"
+| "s \<Rightarrow> t == (s, t) \<in> Redl"
+| "s \<Rightarrow> t == (s, t) \<in> Redt"
+| "s \<Rightarrow>* t == (s, t) \<in> Red^*"
+| "s \<Rightarrow>* t == (s, t) \<in> Redt^*"
 (* ML *)
-"A_ML (Lam_ML u) [v] \<Rightarrow> u[v/0]"
+| "A_ML (Lam_ML u) [v] \<Rightarrow> u[v/0]"
 (* compiled rules *)
-"(nm,vs,v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs) \<Rightarrow> subst\<^bsub>ML\<^esub> f v"
+| "(nm,vs,v) : compR ==> ALL i. ML_closed 0 (f i) \<Longrightarrow> A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs) \<Rightarrow> subst\<^bsub>ML\<^esub> f v"
 (* apply *)
-apply_Fun1: "apply (Fun f vs (Suc 0)) v \<Rightarrow> A_ML f (vs @ [v])"
-apply_Fun2: "n > 0 ==>
+| apply_Fun1: "apply (Fun f vs (Suc 0)) v \<Rightarrow> A_ML f (vs @ [v])"
+| apply_Fun2: "n > 0 ==>
  apply (Fun f vs (Suc n)) v \<Rightarrow> Fun f (vs @ [v]) n"
-apply_C: "apply (C nm vs) v \<Rightarrow> C nm (vs @ [v])"
-apply_V: "apply (V x vs) v \<Rightarrow> V x (vs @ [v])"
+| apply_C: "apply (C nm vs) v \<Rightarrow> C nm (vs @ [v])"
+| apply_V: "apply (V x vs) v \<Rightarrow> V x (vs @ [v])"
 (* term_of *)
-term_of_C: "term_of (C nm vs) \<Rightarrow> foldl At (Ct nm) (map term_of vs)"
-term_of_V: "term_of (V x vs) \<Rightarrow> foldl At (Vt x) (map term_of vs)"
-term_of_Fun: "term_of(Fun vf vs n) \<Rightarrow>
+| term_of_C: "term_of (C nm vs) \<Rightarrow> foldl At (Ct nm) (map term_of vs)"
+| term_of_V: "term_of (V x vs) \<Rightarrow> foldl At (Vt x) (map term_of vs)"
+| term_of_Fun: "term_of(Fun vf vs n) \<Rightarrow>
  Lam (term_of ((apply (lift 0 (Fun vf vs n)) (V_ML 0))[V 0 []/0]))"
 (* Context *)
-ctxt_Lam: "t \<Rightarrow> t' ==> Lam t \<Rightarrow> Lam t'"
-ctxt_At1: "s \<Rightarrow> s' ==> At s t \<Rightarrow> At s' t"
-ctxt_At2: "t \<Rightarrow> t' ==> At s t \<Rightarrow> At s t'"
-ctxt_term_of: "v \<Rightarrow> v' ==> term_of v \<Rightarrow> term_of v'"
-ctxt_C: "vs \<Rightarrow> vs' ==> C nm vs \<Rightarrow> C nm vs'"
-ctxt_V: "vs \<Rightarrow> vs' ==> V x vs \<Rightarrow> V x vs'"
-ctxt_Fun1: "f \<Rightarrow> f'   ==> Fun f vs n \<Rightarrow> Fun f' vs n"
-ctxt_Fun3: "vs \<Rightarrow> vs' ==> Fun f vs n \<Rightarrow> Fun f vs' n"
-ctxt_apply1: "s \<Rightarrow> s'   ==> apply s t \<Rightarrow> apply s' t"
-ctxt_apply2: "t \<Rightarrow> t'   ==> apply s t \<Rightarrow> apply s t'"
-ctxt_A_ML1: "f \<Rightarrow> f'   ==> A_ML f vs \<Rightarrow> A_ML f' vs"
-ctxt_A_ML2: "vs \<Rightarrow> vs' ==> A_ML f vs \<Rightarrow> A_ML f vs'"
-ctxt_list1: "v \<Rightarrow> v'   ==> v#vs \<Rightarrow> v'#vs"
-ctxt_list2: "vs \<Rightarrow> vs' ==> v#vs \<Rightarrow> v#vs'"
+| ctxt_Lam: "t \<Rightarrow> t' ==> Lam t \<Rightarrow> Lam t'"
+| ctxt_At1: "s \<Rightarrow> s' ==> At s t \<Rightarrow> At s' t"
+| ctxt_At2: "t \<Rightarrow> t' ==> At s t \<Rightarrow> At s t'"
+| ctxt_term_of: "v \<Rightarrow> v' ==> term_of v \<Rightarrow> term_of v'"
+| ctxt_C: "vs \<Rightarrow> vs' ==> C nm vs \<Rightarrow> C nm vs'"
+| ctxt_V: "vs \<Rightarrow> vs' ==> V x vs \<Rightarrow> V x vs'"
+| ctxt_Fun1: "f \<Rightarrow> f'   ==> Fun f vs n \<Rightarrow> Fun f' vs n"
+| ctxt_Fun3: "vs \<Rightarrow> vs' ==> Fun f vs n \<Rightarrow> Fun f vs' n"
+| ctxt_apply1: "s \<Rightarrow> s'   ==> apply s t \<Rightarrow> apply s' t"
+| ctxt_apply2: "t \<Rightarrow> t'   ==> apply s t \<Rightarrow> apply s t'"
+| ctxt_A_ML1: "f \<Rightarrow> f'   ==> A_ML f vs \<Rightarrow> A_ML f' vs"
+| ctxt_A_ML2: "vs \<Rightarrow> vs' ==> A_ML f vs \<Rightarrow> A_ML f vs'"
+| ctxt_list1: "v \<Rightarrow> v'   ==> v#vs \<Rightarrow> v'#vs"
+| ctxt_list2: "vs \<Rightarrow> vs' ==> v#vs \<Rightarrow> v#vs'"
 
 
 consts
@@ -791,7 +780,7 @@
 next
   case term_of_V thus ?case apply (auto simp:map_compose[symmetric]) sorry
 next
-  case (term_of_Fun n vf vs)
+  case (term_of_Fun vf vs n)
   hence "term_of (Fun vf vs n)! \<rightarrow>*
        Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!" sorry
   moreover
diff -r 60b7800338d5 -r 18f426a137a9 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -937,35 +937,30 @@
 
 subsubsection {* Inductively defined sets *}
 
-consts
-  arbitrarySet :: "'a set"
-inductive arbitrarySet
-intros
+inductive_set arbitrarySet :: "'a set"
+where
   "arbitrary : arbitrarySet"
 
 lemma "x : arbitrarySet"
   refute
 oops
 
-consts
-  evenCard :: "'a set set"
-inductive evenCard
-intros
+inductive_set evenCard :: "'a set set"
+where
   "{} : evenCard"
-  "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
+| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
 
 lemma "S : evenCard"
   refute
 oops
 
-consts
+inductive_set
   even :: "nat set"
-  odd  :: "nat set"
-inductive even odd
-intros
+  and odd  :: "nat set"
+where
   "0 : even"
-  "n : even \<Longrightarrow> Suc n : odd"
-  "n : odd \<Longrightarrow> Suc n : even"
+| "n : even \<Longrightarrow> Suc n : odd"
+| "n : odd \<Longrightarrow> Suc n : even"
 
 lemma "n : odd"
   (*refute*)  -- {* unfortunately, this little example already takes too long *}
diff -r 60b7800338d5 -r 18f426a137a9 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -50,8 +50,7 @@
   was_enabled        ::"('a,'s)ioa => 'a => 's => bool"
   set_was_enabled    ::"('a,'s)ioa => 'a set => 's => bool"
 
-  (* reachability and invariants *)
-  reachable     :: "('a,'s)ioa => 's set"
+  (* invariants *)
   invariant     :: "[('a,'s)ioa, 's=>bool] => bool"
 
   (* binary composition of action signatures and automata *)
@@ -73,7 +72,6 @@
 syntax
 
   "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  ("_ -_--_-> _" [81,81,81,81] 100)
-  "reachable"  :: "[('a,'s)ioa, 's] => bool"
   "act"        :: "('a,'s)ioa => 'a set"
   "ext"        :: "('a,'s)ioa => 'a set"
   "int"        :: "('a,'s)ioa => 'a set"
@@ -91,15 +89,16 @@
   par  (infixr "\<parallel>" 10)
 
 
-inductive "reachable C"
-   intros
-    reachable_0:  "s:(starts_of C) ==> s : reachable C"
-    reachable_n:  "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C"
+inductive
+  reachable :: "('a, 's) ioa => 's => bool"
+  for C :: "('a, 's) ioa"
+  where
+    reachable_0:  "s : starts_of C ==> reachable C s"
+  | reachable_n:  "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
 
 
 translations
   "s -a--A-> t"   == "(s,a,t):trans_of A"
-  "reachable A s" == "s:reachable A"
   "act A"         == "actions (asig_of A)"
   "ext A"         == "externals (asig_of A)"
   "int A"         == "internals (asig_of A)"
@@ -481,7 +480,7 @@
 apply (unfold invariant_def)
 apply (rule allI)
 apply (rule impI)
-apply (rule_tac xa = "s" in reachable.induct)
+apply (rule_tac x = "s" in reachable.induct)
 apply assumption
 apply blast
 apply blast
diff -r 60b7800338d5 -r 18f426a137a9 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -34,9 +34,11 @@
   sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
   "xs @@ ys == sconc $ xs $ ys"
 
-abbreviation
-  Finite :: "'a seq => bool" where
-  "Finite x == x:sfinite"
+inductive
+  Finite :: "'a seq => bool"
+  where
+    sfinite_0:  "Finite nil"
+  | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
 
 defs
 
@@ -108,12 +110,7 @@
   "Infinite x == ~(seq_finite x)"
 
 
-inductive "sfinite"
-   intros
-    sfinite_0:  "nil:sfinite"
-    sfinite_n:  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
-
-declare sfinite.intros [simp]
+declare Finite.intros [simp]
 declare seq.rews [simp]
 
 
@@ -437,7 +434,7 @@
 
 lemma Finite_UU_a: "Finite x --> x~=UU"
 apply (rule impI)
-apply (erule sfinite.induct)
+apply (erule Finite.induct)
  apply simp
 apply simp
 done
@@ -449,7 +446,7 @@
 
 lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
 apply (intro strip)
-apply (erule sfinite.elims)
+apply (erule Finite.cases)
 apply fastsimp
 apply (simp add: seq.injects)
 done
diff -r 60b7800338d5 -r 18f426a137a9 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Jul 11 11:54:03 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Jul 11 11:54:21 2007 +0200
@@ -355,7 +355,7 @@
 
 lemma Seq_Finite_ind:
 "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
-apply (erule (1) sfinite.induct)
+apply (erule (1) Finite.induct)
 apply (tactic {* def_tac 1 *})
 apply (simp add: Consq_def)
 done