1.1 --- a/src/CCL/CCL.thy Sat Jul 05 16:07:23 2014 +0200
1.2 +++ b/src/CCL/CCL.thy Sat Jul 05 16:28:07 2014 +0200
1.3 @@ -31,11 +31,6 @@
1.4
1.5 (*** Bisimulations for pre-order and equality ***)
1.6 po :: "['a,'a]=>o" (infixl "[=" 50)
1.7 - SIM :: "[i,i,i set]=>o"
1.8 - POgen :: "i set => i set"
1.9 - EQgen :: "i set => i set"
1.10 - PO :: "i set"
1.11 - EQ :: "i set"
1.12
1.13 (*** Term Formers ***)
1.14 true :: "i"
1.15 @@ -45,11 +40,6 @@
1.16 "case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
1.17 "apply" :: "[i,i]=>i" (infixl "`" 56)
1.18 bot :: "i"
1.19 - "fix" :: "(i=>i)=>i"
1.20 -
1.21 - (*** Defined Predicates ***)
1.22 - Trm :: "i => o"
1.23 - Dvg :: "i => o"
1.24
1.25 (******* EVALUATION SEMANTICS *******)
1.26
1.27 @@ -89,23 +79,31 @@
1.28 bot_def: "bot == (lam x. x`x)`(lam x. x`x)" and
1.29 apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
1.30
1.31 -defs
1.32 - fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
1.33 +definition "fix" :: "(i=>i)=>i"
1.34 + where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
1.35
1.36 (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
1.37 (* as a bisimulation. They can both be expressed as (bi)simulations up to *)
1.38 (* behavioural equivalence (ie the relations PO and EQ defined below). *)
1.39
1.40 - SIM_def:
1.41 +definition SIM :: "[i,i,i set]=>o"
1.42 + where
1.43 "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) |
1.44 (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
1.45 (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
1.46
1.47 - POgen_def: "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
1.48 - EQgen_def: "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
1.49 +definition POgen :: "i set => i set"
1.50 + where "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
1.51
1.52 - PO_def: "PO == gfp(POgen)"
1.53 - EQ_def: "EQ == gfp(EQgen)"
1.54 +definition EQgen :: "i set => i set"
1.55 + where "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
1.56 +
1.57 +definition PO :: "i set"
1.58 + where "PO == gfp(POgen)"
1.59 +
1.60 +definition EQ :: "i set"
1.61 + where "EQ == gfp(EQgen)"
1.62 +
1.63
1.64 (*** Rules ***)
1.65
1.66 @@ -146,9 +144,11 @@
1.67
1.68 (*** Definitions of Termination and Divergence ***)
1.69
1.70 -defs
1.71 - Dvg_def: "Dvg(t) == t = bot"
1.72 - Trm_def: "Trm(t) == ~ Dvg(t)"
1.73 +definition Dvg :: "i => o"
1.74 + where "Dvg(t) == t = bot"
1.75 +
1.76 +definition Trm :: "i => o"
1.77 + where "Trm(t) == ~ Dvg(t)"
1.78
1.79 text {*
1.80 Would be interesting to build a similar theory for a typed programming language:
2.1 --- a/src/CCL/Wfd.thy Sat Jul 05 16:07:23 2014 +0200
2.2 +++ b/src/CCL/Wfd.thy Sat Jul 05 16:28:07 2014 +0200
2.3 @@ -9,29 +9,23 @@
2.4 imports Trancl Type Hered
2.5 begin
2.6
2.7 -consts
2.8 - (*** Predicates ***)
2.9 - Wfd :: "[i set] => o"
2.10 - (*** Relations ***)
2.11 - wf :: "[i set] => i set"
2.12 - wmap :: "[i=>i,i set] => i set"
2.13 - lex :: "[i set,i set] => i set" (infixl "**" 70)
2.14 - NatPR :: "i set"
2.15 - ListPR :: "i set => i set"
2.16 +definition Wfd :: "[i set] => o"
2.17 + where "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
2.18
2.19 -defs
2.20 +definition wf :: "[i set] => i set"
2.21 + where "wf(R) == {x. x:R & Wfd(R)}"
2.22
2.23 - Wfd_def:
2.24 - "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
2.25 +definition wmap :: "[i=>i,i set] => i set"
2.26 + where "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"
2.27
2.28 - wf_def: "wf(R) == {x. x:R & Wfd(R)}"
2.29 +definition lex :: "[i set,i set] => i set" (infixl "**" 70)
2.30 + where "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
2.31
2.32 - wmap_def: "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"
2.33 - lex_def:
2.34 - "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
2.35 +definition NatPR :: "i set"
2.36 + where "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
2.37
2.38 - NatPR_def: "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
2.39 - ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
2.40 +definition ListPR :: "i set => i set"
2.41 + where "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
2.42
2.43
2.44 lemma wfd_induct:
3.1 --- a/src/Pure/defs.ML Sat Jul 05 16:07:23 2014 +0200
3.2 +++ b/src/Pure/defs.ML Sat Jul 05 16:28:07 2014 +0200
3.3 @@ -142,7 +142,7 @@
3.4 err ctxt (c, args) (d, Us) "Circular" "";
3.5
3.6 fun wellformed ctxt defs (c, args) (d, Us) =
3.7 - forall is_TVar Us orelse
3.8 + plain_args Us orelse
3.9 (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
3.10 SOME (Ts, description) =>
3.11 err ctxt (c, args) (d, Us) "Malformed"