# HG changeset patch
# User clasohm
# Date 826287069 -3600
# Node ID 9c6ebfab4e05330a53fc14d58f5a635151da1e32
# Parent  fe30812f5b5e3cda4191acc48d07762925f22de2
added constdefs section

diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Gfp.thy
--- a/src/HOL/Gfp.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Gfp.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -7,8 +7,9 @@
 *)
 
 Gfp = Lfp +
-consts gfp :: ['a set=>'a set] => 'a set
-defs
- (*greatest fixed point*)
- gfp_def "gfp(f) == Union({u. u <= f(u)})"
+
+constdefs
+  gfp :: ['a set=>'a set] => 'a set
+  "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
+
 end
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -8,20 +8,20 @@
 
 Arith2 = Arith +
 
-consts
-  divides :: [nat, nat] => bool                 (infixl 70)
+constdefs
+  divides :: [nat, nat] => bool                             (infixl 70)
+  "x divides n == 0<n & 0<x & (n mod x) = 0"
+
   cd      :: [nat, nat, nat] => bool
-  gcd     :: [nat, nat] => nat
-
-  pow     :: [nat, nat] => nat                  (infixl 75)
-  fac     :: nat => nat
+  "cd x m n  == x divides m & x divides n"
 
-defs
-  divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
-  cd_def        "cd x m n  == x divides m & x divides n"
-  gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+  gcd     :: [nat, nat] => nat
+  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
 
-  pow_def       "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
-  fac_def       "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+  pow     :: [nat, nat] => nat                              (infixl 75)
+  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
+
+  fac     :: nat => nat
+  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
 
 end
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Fri Mar 08 13:11:09 1996 +0100
@@ -10,19 +10,19 @@
 
 (*** Hoare rules ***)
 
-val SkipRule = prove_goalw thy [SpecDef,SkipDef]
+val SkipRule = prove_goalw thy [Spec_def,Skip_def]
   "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
   (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
 
-val AssignRule = prove_goalw thy [SpecDef,AssignDef]
+val AssignRule = prove_goalw thy [Spec_def,Assign_def]
   "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
   (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
 
-val SeqRule = prove_goalw thy [SpecDef,SeqDef]
+val SeqRule = prove_goalw thy [Spec_def,Seq_def]
   "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
   (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
 
-val IfRule = prove_goalw thy [SpecDef,CondDef]
+val IfRule = prove_goalw thy [Spec_def,Cond_def]
   "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
 \     Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
 \  ==> Spec p (Cond b c c') r"
@@ -33,14 +33,14 @@
       cut_facts_tac [prem2,prem3] 1,
       fast_tac (HOL_cs addIs [prem1]) 1]);
 
-val strenthen_pre = prove_goalw thy [SpecDef]
+val strenthen_pre = prove_goalw thy [Spec_def]
   "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
   (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
                        fast_tac (HOL_cs addIs [prem1]) 1]);
 
-val [iter_0,iter_Suc] = nat_recs IterDef;
+val [iter_0,iter_Suc] = nat_recs Iter_def;
 
-val lemma = prove_goalw thy [SpecDef,WhileDef]
+val lemma = prove_goalw thy [Spec_def,While_def]
   "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
 \  ==> Spec inv (While b inv c) q"
   (fn [prem1,prem2] =>
@@ -49,7 +49,7 @@
       res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
       simp_tac (!simpset addsimps [iter_0]) 1,
       fast_tac (HOL_cs addIs [prem2]) 1,
-      simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
+      simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
       cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
 
 val WhileRule = lemma RSN (2,strenthen_pre);
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -27,31 +27,30 @@
 
   "@Spec"       :: [bool, 'a prog, bool] => bool        ("{_}//_//{_}")
 
-consts
-  (* semantics *)
+constdefs
+  (* denotational semantics *)
 
   Skip          :: 'a com
+  "Skip s s' == (s=s')"
+
   Assign        :: [pvar, 'a exp] => 'a com
+  "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+
   Seq           :: ['a com, 'a com] => 'a com
+  "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
+
   Cond          :: ['a bexp, 'a com, 'a com] => 'a com
+  "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
+
   While         :: ['a bexp, 'a bexp, 'a com] => 'a com
+  "While b inv c s s' == ? n. Iter n b c s s'"
+
   Iter          :: [nat, 'a bexp, 'a com] => 'a com
+  "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
+             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
 
   Spec          :: ['a bexp, 'a com, 'a bexp] => bool
-
-defs
-  (* denotational semantics *)
-
-  SkipDef       "Skip s s' == (s=s')"
-  AssignDef     "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
-  SeqDef        "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
-  CondDef       "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
-  WhileDef      "While b inv c s s' == ? n. Iter n b c s s'"
-
-  IterDef       "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
-                           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
-
-  SpecDef       "Spec p c q == !s s'. c s s' --> p s --> q s'"
+  "Spec p c q == !s s'. c s s' --> p s --> q s'"
 
 end
 
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Lfp.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -7,8 +7,9 @@
 *)
 
 Lfp = mono + Prod +
-consts lfp :: ['a set=>'a set] => 'a set
-defs
- (*least fixed point*)
- lfp_def "lfp(f) == Inter({u. f(u) <= u})"
+
+constdefs
+  lfp :: ['a set=>'a set] => 'a set
+  "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
+
 end
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Prod.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -13,11 +13,9 @@
 
 (* type definition *)
 
-consts
+constdefs
   Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
-
-defs
-  Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
+  "Pair_Rep == (%a b. %x y. x=a & y=b)"
 
 typedef (Prod)
   ('a, 'b) "*"          (infixr 20)
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Sum.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -10,13 +10,12 @@
 
 (* type definition *)
 
-consts
+constdefs
   Inl_Rep       :: ['a, 'a, 'b, bool] => bool
-  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
+  "Inl_Rep == (%a. %x y p. x=a & p)"
 
-defs
-  Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
-  Inr_Rep_def   "Inr_Rep == (%b. %x y p. y=b & ~p)"
+  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
+  "Inr_Rep == (%b. %x y p. y=b & ~p)"
 
 typedef (Sum)
   ('a, 'b) "+"          (infixr 10)
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/Trancl.thy
--- a/src/HOL/Trancl.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Trancl.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -11,14 +11,18 @@
 *)
 
 Trancl = Lfp + Relation + 
-consts
-    rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
-    trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)  
+
+constdefs
+  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
+  "r^*  ==  lfp(%s. id Un (r O s))"
+
+  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)
+  "r^+  ==  r O rtrancl(r)"
+
 syntax
-    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
-defs   
-  rtrancl_def   "r^*  ==  lfp(%s. id Un (r O s))"
-  trancl_def    "r^+  ==  r O rtrancl(r)"
+  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
+
 translations
-                "r^=" == "r Un id"
+  "r^=" == "r Un id"
+
 end
diff -r fe30812f5b5e -r 9c6ebfab4e05 src/HOL/WF.thy
--- a/src/HOL/WF.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/WF.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -7,23 +7,22 @@
 *)
 
 WF = Trancl +
-consts
- wf         :: "('a * 'a)set => bool"
- cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
- is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
- the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
- wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
+
+constdefs
+  wf         :: "('a * 'a)set => bool"
+  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
+
+  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
 
-defs
-  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
-  
-  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
+  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
+  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
 
-  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
+  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
+  "the_recfun r H a  == (@f. is_recfun r H a f)"
 
-  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
+  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
+  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
+                            r x)  x)"
 
-  wfrec_def
-    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
-                              r x)  x)"
 end