--- 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:
--- 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: