--- a/src/CCL/CCL.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/CCL.thy Tue Mar 29 23:27:38 2011 +0200
@@ -85,6 +85,8 @@
apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
bot_def: "bot == (lam x. x`x)`(lam x. x`x)"
+
+defs
fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
(* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
@@ -106,6 +108,7 @@
(** Partial Order **)
+axioms
po_refl: "a [= a"
po_trans: "[| a [= b; b [= c |] ==> a [= c"
po_cong: "a [= b ==> f(a) [= f(b)"
@@ -136,6 +139,7 @@
(*** Definitions of Termination and Divergence ***)
+defs
Dvg_def: "Dvg(t) == t = bot"
Trm_def: "Trm(t) == ~ Dvg(t)"
--- a/src/CCL/Fix.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Fix.thy Tue Mar 29 23:27:38 2011 +0200
@@ -9,17 +9,12 @@
imports Type
begin
-consts
- idgen :: "[i]=>i"
- INCL :: "[i=>o]=>o"
+definition idgen :: "i => i"
+ where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
-defs
- idgen_def:
- "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
-
-axioms
- INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
- po_INCL: "INCL(%x. a(x) [= b(x))"
+axiomatization INCL :: "[i=>o]=>o" where
+ INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and
+ po_INCL: "INCL(%x. a(x) [= b(x))" and
INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
--- a/src/CCL/Hered.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Hered.thy Tue Mar 29 23:27:38 2011 +0200
@@ -15,18 +15,13 @@
is. Not so useful for functions!
*}
-consts
- (*** Predicates ***)
- HTTgen :: "i set => i set"
- HTT :: "i set"
+definition HTTgen :: "i set => i set" where
+ "HTTgen(R) ==
+ {t. t=true | t=false | (EX a b. t= <a, b> & a : R & b : R) |
+ (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}"
-axioms
- (*** Definitions of Hereditary Termination ***)
-
- HTTgen_def:
- "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) |
- (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"
- HTT_def: "HTT == gfp(HTTgen)"
+definition HTT :: "i set"
+ where "HTT == gfp(HTTgen)"
subsection {* Hereditary Termination *}
--- a/src/CCL/Set.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Set.thy Tue Mar 29 23:27:38 2011 +0200
@@ -46,9 +46,9 @@
"ALL x:A. P" == "CONST Ball(A, %x. P)"
"EX x:A. P" == "CONST Bex(A, %x. P)"
-axioms
- mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)"
- set_extension: "A=B <-> (ALL x. x:A <-> x:B)"
+axiomatization where
+ mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and
+ set_extension: "A = B <-> (ALL x. x:A <-> x:B)"
defs
Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)"
--- a/src/CCL/Term.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Term.thy Tue Mar 29 23:27:38 2011 +0200
@@ -111,8 +111,7 @@
consts
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
-axioms
-
+defs
one_def: "one == true"
if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)"
inl_def: "inl(a) == <true,a>"
--- a/src/CCL/Trancl.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Trancl.thy Tue Mar 29 23:27:38 2011 +0200
@@ -9,21 +9,20 @@
imports CCL
begin
-consts
- trans :: "i set => o" (*transitivity predicate*)
- id :: "i set"
- rtrancl :: "i set => i set" ("(_^*)" [100] 100)
- trancl :: "i set => i set" ("(_^+)" [100] 100)
- relcomp :: "[i set,i set] => i set" (infixr "O" 60)
+definition trans :: "i set => o" (*transitivity predicate*)
+ where "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+
+definition id :: "i set" (*the identity relation*)
+ where "id == {p. EX x. p = <x,x>}"
-axioms
- trans_def: "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
- relcomp_def: (*composition of relations*)
- "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
- id_def: (*the identity relation*)
- "id == {p. EX x. p = <x,x>}"
- rtrancl_def: "r^* == lfp(%s. id Un (r O s))"
- trancl_def: "r^+ == r O rtrancl(r)"
+definition relcomp :: "[i set,i set] => i set" (infixr "O" 60) (*composition of relations*)
+ where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+
+definition rtrancl :: "i set => i set" ("(_^*)" [100] 100)
+ where "r^* == lfp(%s. id Un (r O s))"
+
+definition trancl :: "i set => i set" ("(_^+)" [100] 100)
+ where "r^+ == r O rtrancl(r)"
subsection {* Natural deduction for @{text "trans(r)"} *}
--- a/src/CCL/Type.thy Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Type.thy Tue Mar 29 23:27:38 2011 +0200
@@ -50,7 +50,7 @@
(@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
*}
-axioms
+defs
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
Unit_def: "Unit == {x. x=one}"
Bool_def: "Bool == {x. x=true | x=false}"