--- 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
--- 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
--- 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);
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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