added constdefs section
authorclasohm
Fri Mar 08 13:11:09 1996 +0100 (1996-03-08)
changeset 15589c6ebfab4e05
parent 1557 fe30812f5b5e
child 1559 9ba0906aa60d
added constdefs section
src/HOL/Gfp.thy
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Hoare.ML
src/HOL/Hoare/Hoare.thy
src/HOL/Lfp.thy
src/HOL/Prod.thy
src/HOL/Sum.thy
src/HOL/Trancl.thy
src/HOL/WF.thy
     1.1 --- a/src/HOL/Gfp.thy	Wed Mar 06 14:19:39 1996 +0100
     1.2 +++ b/src/HOL/Gfp.thy	Fri Mar 08 13:11:09 1996 +0100
     1.3 @@ -7,8 +7,9 @@
     1.4  *)
     1.5  
     1.6  Gfp = Lfp +
     1.7 -consts gfp :: ['a set=>'a set] => 'a set
     1.8 -defs
     1.9 - (*greatest fixed point*)
    1.10 - gfp_def "gfp(f) == Union({u. u <= f(u)})"
    1.11 +
    1.12 +constdefs
    1.13 +  gfp :: ['a set=>'a set] => 'a set
    1.14 +  "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
    1.15 +
    1.16  end
     2.1 --- a/src/HOL/Hoare/Arith2.thy	Wed Mar 06 14:19:39 1996 +0100
     2.2 +++ b/src/HOL/Hoare/Arith2.thy	Fri Mar 08 13:11:09 1996 +0100
     2.3 @@ -8,20 +8,20 @@
     2.4  
     2.5  Arith2 = Arith +
     2.6  
     2.7 -consts
     2.8 -  divides :: [nat, nat] => bool                 (infixl 70)
     2.9 +constdefs
    2.10 +  divides :: [nat, nat] => bool                             (infixl 70)
    2.11 +  "x divides n == 0<n & 0<x & (n mod x) = 0"
    2.12 +
    2.13    cd      :: [nat, nat, nat] => bool
    2.14 -  gcd     :: [nat, nat] => nat
    2.15 -
    2.16 -  pow     :: [nat, nat] => nat                  (infixl 75)
    2.17 -  fac     :: nat => nat
    2.18 +  "cd x m n  == x divides m & x divides n"
    2.19  
    2.20 -defs
    2.21 -  divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
    2.22 -  cd_def        "cd x m n  == x divides m & x divides n"
    2.23 -  gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    2.24 +  gcd     :: [nat, nat] => nat
    2.25 +  "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    2.26  
    2.27 -  pow_def       "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    2.28 -  fac_def       "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    2.29 +  pow     :: [nat, nat] => nat                              (infixl 75)
    2.30 +  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    2.31 +
    2.32 +  fac     :: nat => nat
    2.33 +  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    2.34  
    2.35  end
     3.1 --- a/src/HOL/Hoare/Hoare.ML	Wed Mar 06 14:19:39 1996 +0100
     3.2 +++ b/src/HOL/Hoare/Hoare.ML	Fri Mar 08 13:11:09 1996 +0100
     3.3 @@ -10,19 +10,19 @@
     3.4  
     3.5  (*** Hoare rules ***)
     3.6  
     3.7 -val SkipRule = prove_goalw thy [SpecDef,SkipDef]
     3.8 +val SkipRule = prove_goalw thy [Spec_def,Skip_def]
     3.9    "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
    3.10    (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
    3.11  
    3.12 -val AssignRule = prove_goalw thy [SpecDef,AssignDef]
    3.13 +val AssignRule = prove_goalw thy [Spec_def,Assign_def]
    3.14    "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
    3.15    (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
    3.16  
    3.17 -val SeqRule = prove_goalw thy [SpecDef,SeqDef]
    3.18 +val SeqRule = prove_goalw thy [Spec_def,Seq_def]
    3.19    "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
    3.20    (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
    3.21  
    3.22 -val IfRule = prove_goalw thy [SpecDef,CondDef]
    3.23 +val IfRule = prove_goalw thy [Spec_def,Cond_def]
    3.24    "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
    3.25  \     Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
    3.26  \  ==> Spec p (Cond b c c') r"
    3.27 @@ -33,14 +33,14 @@
    3.28        cut_facts_tac [prem2,prem3] 1,
    3.29        fast_tac (HOL_cs addIs [prem1]) 1]);
    3.30  
    3.31 -val strenthen_pre = prove_goalw thy [SpecDef]
    3.32 +val strenthen_pre = prove_goalw thy [Spec_def]
    3.33    "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
    3.34    (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
    3.35                         fast_tac (HOL_cs addIs [prem1]) 1]);
    3.36  
    3.37 -val [iter_0,iter_Suc] = nat_recs IterDef;
    3.38 +val [iter_0,iter_Suc] = nat_recs Iter_def;
    3.39  
    3.40 -val lemma = prove_goalw thy [SpecDef,WhileDef]
    3.41 +val lemma = prove_goalw thy [Spec_def,While_def]
    3.42    "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
    3.43  \  ==> Spec inv (While b inv c) q"
    3.44    (fn [prem1,prem2] =>
    3.45 @@ -49,7 +49,7 @@
    3.46        res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
    3.47        simp_tac (!simpset addsimps [iter_0]) 1,
    3.48        fast_tac (HOL_cs addIs [prem2]) 1,
    3.49 -      simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
    3.50 +      simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
    3.51        cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
    3.52  
    3.53  val WhileRule = lemma RSN (2,strenthen_pre);
     4.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Mar 06 14:19:39 1996 +0100
     4.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Mar 08 13:11:09 1996 +0100
     4.3 @@ -27,31 +27,30 @@
     4.4  
     4.5    "@Spec"       :: [bool, 'a prog, bool] => bool        ("{_}//_//{_}")
     4.6  
     4.7 -consts
     4.8 -  (* semantics *)
     4.9 +constdefs
    4.10 +  (* denotational semantics *)
    4.11  
    4.12    Skip          :: 'a com
    4.13 +  "Skip s s' == (s=s')"
    4.14 +
    4.15    Assign        :: [pvar, 'a exp] => 'a com
    4.16 +  "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
    4.17 +
    4.18    Seq           :: ['a com, 'a com] => 'a com
    4.19 +  "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
    4.20 +
    4.21    Cond          :: ['a bexp, 'a com, 'a com] => 'a com
    4.22 +  "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
    4.23 +
    4.24    While         :: ['a bexp, 'a bexp, 'a com] => 'a com
    4.25 +  "While b inv c s s' == ? n. Iter n b c s s'"
    4.26 +
    4.27    Iter          :: [nat, 'a bexp, 'a com] => 'a com
    4.28 +  "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
    4.29 +             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
    4.30  
    4.31    Spec          :: ['a bexp, 'a com, 'a bexp] => bool
    4.32 -
    4.33 -defs
    4.34 -  (* denotational semantics *)
    4.35 -
    4.36 -  SkipDef       "Skip s s' == (s=s')"
    4.37 -  AssignDef     "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
    4.38 -  SeqDef        "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
    4.39 -  CondDef       "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
    4.40 -  WhileDef      "While b inv c s s' == ? n. Iter n b c s s'"
    4.41 -
    4.42 -  IterDef       "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
    4.43 -                           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
    4.44 -
    4.45 -  SpecDef       "Spec p c q == !s s'. c s s' --> p s --> q s'"
    4.46 +  "Spec p c q == !s s'. c s s' --> p s --> q s'"
    4.47  
    4.48  end
    4.49  
     5.1 --- a/src/HOL/Lfp.thy	Wed Mar 06 14:19:39 1996 +0100
     5.2 +++ b/src/HOL/Lfp.thy	Fri Mar 08 13:11:09 1996 +0100
     5.3 @@ -7,8 +7,9 @@
     5.4  *)
     5.5  
     5.6  Lfp = mono + Prod +
     5.7 -consts lfp :: ['a set=>'a set] => 'a set
     5.8 -defs
     5.9 - (*least fixed point*)
    5.10 - lfp_def "lfp(f) == Inter({u. f(u) <= u})"
    5.11 +
    5.12 +constdefs
    5.13 +  lfp :: ['a set=>'a set] => 'a set
    5.14 +  "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
    5.15 +
    5.16  end
     6.1 --- a/src/HOL/Prod.thy	Wed Mar 06 14:19:39 1996 +0100
     6.2 +++ b/src/HOL/Prod.thy	Fri Mar 08 13:11:09 1996 +0100
     6.3 @@ -13,11 +13,9 @@
     6.4  
     6.5  (* type definition *)
     6.6  
     6.7 -consts
     6.8 +constdefs
     6.9    Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
    6.10 -
    6.11 -defs
    6.12 -  Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    6.13 +  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    6.14  
    6.15  typedef (Prod)
    6.16    ('a, 'b) "*"          (infixr 20)
     7.1 --- a/src/HOL/Sum.thy	Wed Mar 06 14:19:39 1996 +0100
     7.2 +++ b/src/HOL/Sum.thy	Fri Mar 08 13:11:09 1996 +0100
     7.3 @@ -10,13 +10,12 @@
     7.4  
     7.5  (* type definition *)
     7.6  
     7.7 -consts
     7.8 +constdefs
     7.9    Inl_Rep       :: ['a, 'a, 'b, bool] => bool
    7.10 -  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
    7.11 +  "Inl_Rep == (%a. %x y p. x=a & p)"
    7.12  
    7.13 -defs
    7.14 -  Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
    7.15 -  Inr_Rep_def   "Inr_Rep == (%b. %x y p. y=b & ~p)"
    7.16 +  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
    7.17 +  "Inr_Rep == (%b. %x y p. y=b & ~p)"
    7.18  
    7.19  typedef (Sum)
    7.20    ('a, 'b) "+"          (infixr 10)
     8.1 --- a/src/HOL/Trancl.thy	Wed Mar 06 14:19:39 1996 +0100
     8.2 +++ b/src/HOL/Trancl.thy	Fri Mar 08 13:11:09 1996 +0100
     8.3 @@ -11,14 +11,18 @@
     8.4  *)
     8.5  
     8.6  Trancl = Lfp + Relation + 
     8.7 -consts
     8.8 -    rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
     8.9 -    trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)  
    8.10 +
    8.11 +constdefs
    8.12 +  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
    8.13 +  "r^*  ==  lfp(%s. id Un (r O s))"
    8.14 +
    8.15 +  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)
    8.16 +  "r^+  ==  r O rtrancl(r)"
    8.17 +
    8.18  syntax
    8.19 -    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
    8.20 -defs   
    8.21 -  rtrancl_def   "r^*  ==  lfp(%s. id Un (r O s))"
    8.22 -  trancl_def    "r^+  ==  r O rtrancl(r)"
    8.23 +  reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
    8.24 +
    8.25  translations
    8.26 -                "r^=" == "r Un id"
    8.27 +  "r^=" == "r Un id"
    8.28 +
    8.29  end
     9.1 --- a/src/HOL/WF.thy	Wed Mar 06 14:19:39 1996 +0100
     9.2 +++ b/src/HOL/WF.thy	Fri Mar 08 13:11:09 1996 +0100
     9.3 @@ -7,23 +7,22 @@
     9.4  *)
     9.5  
     9.6  WF = Trancl +
     9.7 -consts
     9.8 - wf         :: "('a * 'a)set => bool"
     9.9 - cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    9.10 - is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
    9.11 - the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
    9.12 - wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
    9.13 +
    9.14 +constdefs
    9.15 +  wf         :: "('a * 'a)set => bool"
    9.16 +  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    9.17 +
    9.18 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    9.19 +  "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    9.20  
    9.21 -defs
    9.22 -  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    9.23 -  
    9.24 -  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    9.25 +  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
    9.26 +  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
    9.27  
    9.28 -  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
    9.29 +  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
    9.30 +  "the_recfun r H a  == (@f. is_recfun r H a f)"
    9.31  
    9.32 -  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
    9.33 +  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
    9.34 +  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
    9.35 +                            r x)  x)"
    9.36  
    9.37 -  wfrec_def
    9.38 -    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
    9.39 -                              r x)  x)"
    9.40  end