# HG changeset patch
# User berghofe
# Date 1184147204 -7200
# Node ID 7272a839ccd93f202bfa5aa14d6dc4fc1bfeadef
# Parent  77e796fe89eb197acb620e258c2c237cc2fb225d
Adapted to new inductive definition package.

diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -10,27 +10,27 @@
 
 theory Constrains imports UNITY begin
 
-consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
-
   (*Initial states and program => (final state, reversed trace to it)...
     Arguments MUST be curried in an inductive definition*)
 
-inductive "traces init acts"  
-  intros 
+inductive_set
+  traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
+  for init :: "'a set" and acts :: "('a * 'a)set set"
+  where
          (*Initial trace is empty*)
     Init:  "s \<in> init ==> (s,[]) \<in> traces init acts"
 
-    Acts:  "[| act: acts;  (s,evs) \<in> traces init acts;  (s,s'): act |]
+  | Acts:  "[| act: acts;  (s,evs) \<in> traces init acts;  (s,s'): act |]
 	    ==> (s', s#evs) \<in> traces init acts"
 
 
-consts reachable :: "'a program => 'a set"
-
-inductive "reachable F"
-  intros 
+inductive_set
+  reachable :: "'a program => 'a set"
+  for F :: "'a program"
+  where
     Init:  "s \<in> Init F ==> s \<in> reachable F"
 
-    Acts:  "[| act: Acts F;  s \<in> reachable F;  (s,s'): act |]
+  | Acts:  "[| act: Acts F;  s \<in> reachable F;  (s,s'): act |]
 	    ==> s' \<in> reachable F"
 
 constdefs
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/ELT.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -26,20 +26,17 @@
 
 theory ELT imports Project begin
 
-consts
-
+inductive_set
   (*LEADS-TO constant for the inductive definition*)
   elt :: "['a set set, 'a program] => ('a set * 'a set) set"
-
-
-inductive "elt CC F"
- intros 
+  for CC :: "'a set set" and F :: "'a program"
+ where
 
    Basis:  "[| F : A ensures B;  A-B : (insert {} CC) |] ==> (A,B) : elt CC F"
 
-   Trans:  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
+ | Trans:  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
 
-   Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
+ | Union:  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
 
 
 constdefs
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -17,17 +17,16 @@
 
 theory ListOrder imports Main begin
 
-consts
+inductive_set
   genPrefix :: "('a * 'a)set => ('a list * 'a list)set"
-
-inductive "genPrefix(r)"
- intros
+  for r :: "('a * 'a)set"
+ where
    Nil:     "([],[]) : genPrefix(r)"
 
-   prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
+ | prepend: "[| (xs,ys) : genPrefix(r);  (x,y) : r |] ==>
 	     (x#xs, y#ys) : genPrefix(r)"
 
-   append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
+ | append:  "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
 
 instance list :: (type)ord ..
 
@@ -45,14 +44,13 @@
   Ge :: "(nat*nat) set"
     "Ge == {(x,y). y <= x}"
 
-syntax
-  pfixLe :: "[nat list, nat list] => bool"          (infixl "pfixLe" 50)
-  pfixGe :: "[nat list, nat list] => bool"          (infixl "pfixGe" 50)
+abbreviation
+  pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
+  "xs pfixLe ys == (xs,ys) : genPrefix Le"
 
-translations
-  "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
-
-  "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
+abbreviation
+  pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
+  "xs pfixGe ys == (xs,ys) : genPrefix Ge"
 
 
 subsection{*preliminary lemmas*}
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -401,7 +401,7 @@
 
 theorem relcl_latticeof_eq:
      "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
-by (simp add: relcl_def cl_latticeof, blast)
+by (simp add: relcl_def cl_latticeof)
 
 
 subsubsection {*Decoupling Theorems*}
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -16,15 +16,14 @@
   reach :: "vertex => bool"
   nmsg  :: "edge => nat"
 
-consts REACHABLE :: "edge set"
-       root :: "vertex"
+consts root :: "vertex"
        E :: "edge set"
        V :: "vertex set"
 
-inductive "REACHABLE"
-  intros
-   base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
-   step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
+inductive_set REACHABLE :: "edge set"
+  where
+    base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
+  | step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
 
 constdefs
   reachable :: "vertex => state set"
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -159,17 +159,16 @@
 
 subsection{*Defining the Weakest Ensures Set*}
 
-consts
+inductive_set
   wens_set :: "['a program, 'a set] => 'a set set"
-
-inductive "wens_set F B"
- intros 
+  for F :: "'a program" and B :: "'a set"
+where
 
   Basis: "B \<in> wens_set F B"
 
-  Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
+| Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
 
-  Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
+| Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
 
 lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
 apply (erule wens_set.induct) 
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/UNITY/WFair.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -46,20 +46,17 @@
     "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
 
 
-consts
-
+inductive_set
   leads :: "'a program => ('a set * 'a set) set"
     --{*LEADS-TO constant for the inductive definition*}
-
-
-inductive "leads F"
-  intros 
+  for F :: "'a program"
+  where
 
     Basis:  "F \<in> A ensures B ==> (A,B) \<in> leads F"
 
-    Trans:  "[| (A,B) \<in> leads F;  (B,C) \<in> leads F |] ==> (A,C) \<in> leads F"
+  | Trans:  "[| (A,B) \<in> leads F;  (B,C) \<in> leads F |] ==> (A,C) \<in> leads F"
 
-    Union:  "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
+  | Union:  "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
 
 
 constdefs
diff -r 77e796fe89eb -r 7272a839ccd9 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Wed Jul 11 11:46:05 2007 +0200
+++ b/src/HOL/W0/W0.thy	Wed Jul 11 11:46:44 2007 +0200
@@ -381,18 +381,12 @@
 
 text {* Type inference rules. *}
 
-consts
-  has_type :: "(typ list \<times> expr \<times> typ) set"
-
-abbreviation
-  has_type_rel  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60) where
-  "a |- e :: t == (a, e, t) \<in> has_type"
-
-inductive has_type
-  intros
+inductive
+  has_type :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
+  where
     Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
-    Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
-    App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
+  | Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
+  | App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
       \<Longrightarrow> a |- App e1 e2 :: t1"
 
 
@@ -400,7 +394,7 @@
 
 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
 proof (induct set: has_type)
-  case (Var a n)
+  case (Var n a)
   then have "n < length (map ($ s) a)" by simp
   then have "map ($ s) a |- Var n :: map ($ s) a ! n"
     by (rule has_type.Var)
@@ -410,7 +404,7 @@
     by (simp only: app_subst_list)
   finally show ?case .
 next
-  case (Abs a e t1 t2)
+  case (Abs t1 a e t2)
   then have "$ s t1 # map ($ s) a |- e :: $ s t2"
     by (simp add: app_subst_list)
   then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"