# HG changeset patch
# User wenzelm
# Date 1404560393 -7200
# Node ID b14c0794f97fbb8cf86fa0589e9ff046e5600f64
# Parent  3ad1b289f21b2afd3c4746ace3889279bf3cbf40
modernized definitions;

diff -r 3ad1b289f21b -r b14c0794f97f src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Sat Jul 05 13:21:53 2014 +0200
+++ b/src/CCL/CCL.thy	Sat Jul 05 13:39:53 2014 +0200
@@ -31,11 +31,6 @@
 
   (*** Bisimulations for pre-order and equality ***)
   po          ::       "['a,'a]=>o"           (infixl "[=" 50)
-  SIM         ::       "[i,i,i set]=>o"
-  POgen       ::       "i set => i set"
-  EQgen       ::       "i set => i set"
-  PO          ::       "i set"
-  EQ          ::       "i set"
 
   (*** Term Formers ***)
   true        ::       "i"
@@ -45,11 +40,6 @@
   "case"      ::       "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
   "apply"     ::       "[i,i]=>i"             (infixl "`" 56)
   bot         ::       "i"
-  "fix"       ::       "(i=>i)=>i"
-
-  (*** Defined Predicates ***)
-  Trm         ::       "i => o"
-  Dvg         ::       "i => o"
 
   (******* EVALUATION SEMANTICS *******)
 
@@ -89,23 +79,31 @@
   bot_def:         "bot == (lam x. x`x)`(lam x. x`x)" and
   apply_def:     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
 
-defs
-  fix_def:      "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
+definition "fix" :: "(i=>i)=>i"
+  where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
 
   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
   (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
   (*  behavioural equivalence (ie the relations PO and EQ defined below).            *)
 
-  SIM_def:
+definition SIM :: "[i,i,i set]=>o"
+  where
   "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) |
                   (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
                   (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
 
-  POgen_def:  "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
-  EQgen_def:  "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
+definition POgen :: "i set => i set"
+  where "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
+
+definition EQgen :: "i set => i set"
+  where "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
 
-  PO_def:    "PO == gfp(POgen)"
-  EQ_def:    "EQ == gfp(EQgen)"
+definition PO :: "i set"
+  where "PO == gfp(POgen)"
+
+definition EQ :: "i set"
+  where "EQ == gfp(EQgen)"
+
 
   (*** Rules ***)
 
@@ -146,9 +144,11 @@
 
   (*** Definitions of Termination and Divergence ***)
 
-defs
-  Dvg_def:  "Dvg(t) == t = bot"
-  Trm_def:  "Trm(t) == ~ Dvg(t)"
+definition Dvg :: "i => o"
+  where "Dvg(t) == t = bot"
+
+definition Trm :: "i => o"
+  where "Trm(t) == ~ Dvg(t)"
 
 text {*
 Would be interesting to build a similar theory for a typed programming language:
diff -r 3ad1b289f21b -r b14c0794f97f src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sat Jul 05 13:21:53 2014 +0200
+++ b/src/CCL/Wfd.thy	Sat Jul 05 13:39:53 2014 +0200
@@ -9,29 +9,23 @@
 imports Trancl Type Hered
 begin
 
-consts
-      (*** Predicates ***)
-  Wfd        ::       "[i set] => o"
-      (*** Relations ***)
-  wf         ::       "[i set] => i set"
-  wmap       ::       "[i=>i,i set] => i set"
-  lex        ::       "[i set,i set] => i set"      (infixl "**" 70)
-  NatPR      ::       "i set"
-  ListPR     ::       "i set => i set"
+definition Wfd :: "[i set] => o"
+  where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
 
-defs
+definition wf :: "[i set] => i set"
+  where "wf(R) == {x. x:R & Wfd(R)}"
+
+definition wmap :: "[i=>i,i set] => i set"
+  where "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
 
-  Wfd_def:
-  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
-
-  wf_def:         "wf(R) == {x. x:R & Wfd(R)}"
+definition lex :: "[i set,i set] => i set"      (infixl "**" 70)
+  where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
 
-  wmap_def:       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
-  lex_def:
-  "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
+definition NatPR :: "i set"
+  where "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
 
-  NatPR_def:      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
-  ListPR_def:     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
+definition ListPR :: "i set => i set"
+  where "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
 
 
 lemma wfd_induct: