modernized specifications -- some attempts to avoid wild axiomatizations;
comp: retain infix \<circ> to retain type "o" from FOL;
tuned proofs;

--- a/src/CCL/ex/Flag.thy	Tue Mar 29 22:36:56 2011 +0200
+++ b/src/CCL/ex/Flag.thy	Tue Mar 29 23:15:25 2011 +0200
@@ -10,24 +10,24 @@
 imports List
 begin
 
-consts
-  Colour             :: "i set"
-  red                :: "i"
-  white              :: "i"
-  blue               :: "i"
-  ccase              :: "[i,i,i,i]=>i"
-  flag               :: "i"
+definition Colour :: "i set"
+  where "Colour == Unit + Unit + Unit"
+
+definition red :: "i"
+  where "red == inl(one)"
+
+definition white :: "i"
+  where "white == inr(inl(one))"
 
-axioms
+definition blue :: "i"
+  where "blue == inr(inr(one))"
 
-  Colour_def:  "Colour == Unit + Unit + Unit"
-  red_def:        "red == inl(one)"
-  white_def:    "white == inr(inl(one))"
-  blue_def:     "blue == inr(inr(one))"
+definition ccase :: "[i,i,i,i]=>i"
+  where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
 
-  ccase_def:   "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
-
-  flag_def:    "flag == lam l. letrec
+definition flag :: "i"
+  where
+    "flag == lam l. letrec
       flagx l be lcase(l,<[],<[],[]>>,
                        %h t. split(flagx(t),%lr p. split(p,%lw lb.
                             ccase(h, <red$lr,<lw,lb>>,
@@ -35,13 +35,14 @@
                                      <lr,<lw,blue$lb>>))))
       in flagx(l)"
 
-  Flag_def:
-     "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
-                    x = <lr,<lw,lb>> -->
-                  (ALL c:Colour.(c mem lr = true --> c=red) &
-                                (c mem lw = true --> c=white) &
-                                (c mem lb = true --> c=blue)) &
-                  Perm(l,lr @ lw @ lb)"
+axiomatization Perm :: "i => i => o"
+definition Flag :: "i => i => o" where
+  "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
+                x = <lr,<lw,lb>> -->
+              (ALL c:Colour.(c mem lr = true --> c=red) &
+                            (c mem lw = true --> c=white) &
+                            (c mem lb = true --> c=blue)) &
+              Perm(l,lr @ lw @ lb)"
 
 
 lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
@@ -68,7 +69,7 @@
   apply assumption
   done
 
-lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
+lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
   apply (unfold flag_def)
   apply (tactic {* gen_ccs_tac @{context}
     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})

--- a/src/CCL/ex/List.thy	Tue Mar 29 22:36:56 2011 +0200
+++ b/src/CCL/ex/List.thy	Tue Mar 29 23:15:25 2011 +0200
@@ -9,46 +9,47 @@
 imports Nat
 begin
 
-consts
-  map       :: "[i=>i,i]=>i"
-  comp      :: "[i=>i,i=>i]=>i=>i"    (infixr "o" 55)
-  append    :: "[i,i]=>i"             (infixr "@" 55)
-  member    :: "[i,i]=>i"             (infixr "mem" 55)
-  filter    :: "[i,i]=>i"
-  flat      :: "i=>i"
-  partition :: "[i,i]=>i"
-  insert    :: "[i,i,i]=>i"
-  isort     :: "i=>i"
-  qsort     :: "i=>i"
+definition map :: "[i=>i,i]=>i"
+  where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+
+definition comp :: "[i=>i,i=>i]=>i=>i"  (infixr "\<circ>" 55)
+  where "f \<circ> g == (%x. f(g(x)))"
+
+definition append :: "[i,i]=>i"  (infixr "@" 55)
+  where "l @ m == lrec(l,m,%x xs g. x$g)"
 
-axioms
+axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
+  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
 
-  map_def:     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
-  comp_def:    "f o g == (%x. f(g(x)))"
-  append_def:  "l @ m == lrec(l,m,%x xs g. x$g)"
-  member_def:  "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
-  filter_def:  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
-  flat_def:    "flat(l) == lrec(l,[],%h t g. h @ g)"
+definition filter :: "[i,i]=>i"
+  where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
 
-  insert_def:  "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
-  isort_def:   "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+definition flat :: "i=>i"
+  where "flat(l) == lrec(l,[],%h t g. h @ g)"
 
-  partition_def:
+definition partition :: "[i,i]=>i" where
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
                             if f`x then part(xs,x$a,b) else part(xs,a,x$b))
                     in part(l,[],[])"
-  qsort_def:   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
+
+definition insert :: "[i,i,i]=>i"
+  where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+
+definition isort :: "i=>i"
+  where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+
+definition qsort :: "i=>i" where
+  "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
                                    let p be partition(f`h,t)
                                    in split(p,%x y. qsortx(x) @ h$qsortx(y)))
                           in qsortx(l)"
 
-
 lemmas list_defs = map_def comp_def append_def filter_def flat_def
   insert_def isort_def partition_def qsort_def
 
 lemma listBs [simp]:
-  "!!f g. (f o g) = (%a. f(g(a)))"
-  "!!a f g. (f o g)(a) = f(g(a))"
+  "!!f g. (f \<circ> g) = (%a. f(g(a)))"
+  "!!a f g. (f \<circ> g)(a) = f(g(a))"
   "!!f. map(f,[]) = []"
   "!!f x xs. map(f,x$xs) = f(x)$map(f,xs)"
   "!!m. [] @ m = m"
@@ -85,7 +86,7 @@
 
 lemma appendTS:
   "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"
-  by (blast intro!: SubtypeI appendT elim!: SubtypeE)
+  by (blast intro!: appendT)
 
 lemma filterT: "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)"
   apply (unfold filter_def)
@@ -105,7 +106,7 @@
 lemma insertTS:
   "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==>  
    insert(f,a,l)  : {x:List(A). P(x)}"
-  by (blast intro!: SubtypeI insertT elim!: SubtypeE)
+  by (blast intro!: insertT)
 
 lemma partitionT:
   "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)"

--- a/src/CCL/ex/Nat.thy	Tue Mar 29 22:36:56 2011 +0200
+++ b/src/CCL/ex/Nat.thy	Tue Mar 29 23:15:25 2011 +0200
@@ -9,37 +9,44 @@
 imports Wfd
 begin
 
-consts
+definition not :: "i=>i"
+  where "not(b) == if b then false else true"
+
+definition add :: "[i,i]=>i"  (infixr "#+" 60)
+  where "a #+ b == nrec(a,b,%x g. succ(g))"
 
-  not   :: "i=>i"
-  add   :: "[i,i]=>i"            (infixr "#+" 60)
-  mult  :: "[i,i]=>i"            (infixr "#*" 60)
-  sub   :: "[i,i]=>i"            (infixr "#-" 60)
-  div   :: "[i,i]=>i"            (infixr "##" 60)
-  lt    :: "[i,i]=>i"            (infixr "#<" 60)
-  le    :: "[i,i]=>i"            (infixr "#<=" 60)
-  ackermann :: "[i,i]=>i"
+definition mult :: "[i,i]=>i"  (infixr "#*" 60)
+  where "a #* b == nrec(a,zero,%x g. b #+ g)"
 
-defs
-
-  not_def:     "not(b) == if b then false else true"
+definition sub :: "[i,i]=>i"  (infixr "#-" 60)
+  where
+    "a #- b ==
+      letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
+      in sub(a,b)"
 
-  add_def:     "a #+ b == nrec(a,b,%x g. succ(g))"
-  mult_def:    "a #* b == nrec(a,zero,%x g. b #+ g)"
-  sub_def:     "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
-                        in sub(a,b)"
-  le_def:     "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
-                        in le(a,b)"
-  lt_def:     "a #< b == not(b #<= a)"
+definition le :: "[i,i]=>i"  (infixr "#<=" 60)
+  where
+    "a #<= b ==
+      letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
+      in le(a,b)"
+
+definition lt :: "[i,i]=>i"  (infixr "#<" 60)
+  where "a #< b == not(b #<= a)"
 
-  div_def:    "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y))
-                       in div(a,b)"
-  ack_def:
-  "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
-                          ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
-                    in ack(a,b)"
+definition div :: "[i,i]=>i"  (infixr "##" 60)
+  where
+    "a ## b ==
+      letrec div x y be if x #< y then zero else succ(div(x#-y,y))
+      in div(a,b)"
 
-lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def
+definition ackermann :: "[i,i]=>i"
+  where
+    "ackermann(a,b) ==
+      letrec ack n m be ncase(n,succ(m),%x.
+        ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
+      in ack(a,b)"
+
+lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def
 
 lemma natBs [simp]:
   "not(true) = false"
@@ -94,7 +101,7 @@
 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
 
 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
-  apply (unfold ack_def)
+  apply (unfold ackermann_def)
   apply (tactic {* gen_ccs_tac @{context} [] 1 *})
   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   done

--- a/src/CCL/ex/Stream.thy	Tue Mar 29 22:36:56 2011 +0200
+++ b/src/CCL/ex/Stream.thy	Tue Mar 29 23:15:25 2011 +0200
@@ -9,15 +9,11 @@
 imports List
 begin
 
-consts
-  iter1   ::  "[i=>i,i]=>i"
-  iter2   ::  "[i=>i,i]=>i"
+definition iter1 :: "[i=>i,i]=>i"
+  where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
 
-defs
-
-  iter1_def:   "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
-  iter2_def:   "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
-
+definition iter2 :: "[i=>i,i]=>i"
+  where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
 
 (*
 Proving properties about infinite lists using coinduction:
@@ -30,9 +26,9 @@
 
 lemma map_comp:
   assumes 1: "l:Lists(A)"
-  shows "map(f o g,l) = map(f,map(g,l))"
+  shows "map(f \<circ> g,l) = map(f,map(g,l))"
   apply (tactic {* eq_coinduct3_tac @{context}
-    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
+    "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}" 1 *})
    apply (blast intro: 1)
   apply safe
   apply (drule ListsXH [THEN iffD1])