# HG changeset patch
# User wenzelm
# Date 1301434058 -7200
# Node ID df219e736a5d05c53e7dac48c3e26a85db87849e
# Parent  ffe99b07c9c000307c773bf09da405fb9750a93f
modernized specifications -- less axioms;

diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/CCL.thy
--- 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)"
 
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Fix.thy
--- 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)))"
 
 
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Hered.thy
--- 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 *}
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Set.thy
--- 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)"
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Term.thy
--- 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>"
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Trancl.thy
--- 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)"} *}
diff -r ffe99b07c9c0 -r df219e736a5d src/CCL/Type.thy
--- 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}"