1.1 --- a/src/CCL/CCL.thy	Thu Feb 28 13:46:45 2013 +0100
     1.2 +++ b/src/CCL/CCL.thy	Thu Feb 28 13:54:45 2013 +0100
     1.3 @@ -51,25 +51,26 @@
     1.4    Trm         ::       "i => o"
     1.5    Dvg         ::       "i => o"
     1.6  
     1.7 -axioms
     1.8 -
     1.9    (******* EVALUATION SEMANTICS *******)
    1.10  
    1.11    (**  This is the evaluation semantics from which the axioms below were derived.  **)
    1.12    (**  It is included here just as an evaluator for FUN and has no influence on    **)
    1.13    (**  inference in the theory CCL.                                                **)
    1.14  
    1.15 -  trueV:       "true ---> true"
    1.16 -  falseV:      "false ---> false"
    1.17 -  pairV:       "<a,b> ---> <a,b>"
    1.18 -  lamV:        "lam x. b(x) ---> lam x. b(x)"
    1.19 -  caseVtrue:   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c"
    1.20 -  caseVfalse:  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c"
    1.21 -  caseVpair:   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    1.22 -  caseVlam:    "[| t ---> lam x. b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    1.23 +axiomatization where
    1.24 +  trueV:       "true ---> true" and
    1.25 +  falseV:      "false ---> false" and
    1.26 +  pairV:       "<a,b> ---> <a,b>" and
    1.27 +  lamV:        "\<And>b. lam x. b(x) ---> lam x. b(x)" and
    1.28 +
    1.29 +  caseVtrue:   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c" and
    1.30 +  caseVfalse:  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c" and
    1.31 +  caseVpair:   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" and
    1.32 +  caseVlam:    "\<And>b. [| t ---> lam x. b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    1.33  
    1.34    (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
    1.35  
    1.36 +axiomatization where
    1.37    canonical:  "[| t ---> c; c==true ==> u--->v;
    1.38                            c==false ==> u--->v;
    1.39                      !!a b. c==<a,b> ==> u--->v;
    1.40 @@ -77,14 +78,16 @@
    1.41               u--->v"
    1.42  
    1.43    (* Should be derivable - but probably a bitch! *)
    1.44 +axiomatization where
    1.45    substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"
    1.46  
    1.47    (************** LOGIC ***************)
    1.48  
    1.49    (*** Definitions used in the following rules ***)
    1.50  
    1.51 +axiomatization where
    1.52 +  bot_def:         "bot == (lam x. x`x)`(lam x. x`x)" and
    1.53    apply_def:     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
    1.54 -  bot_def:         "bot == (lam x. x`x)`(lam x. x`x)"
    1.55  
    1.56  defs
    1.57    fix_def:      "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
    1.58 @@ -108,10 +111,10 @@
    1.59  
    1.60    (** Partial Order **)
    1.61  
    1.62 -axioms
    1.63 -  po_refl:        "a [= a"
    1.64 -  po_trans:       "[| a [= b;  b [= c |] ==> a [= c"
    1.65 -  po_cong:        "a [= b ==> f(a) [= f(b)"
    1.66 +axiomatization where
    1.67 +  po_refl:        "a [= a" and
    1.68 +  po_trans:       "[| a [= b;  b [= c |] ==> a [= c" and
    1.69 +  po_cong:        "a [= b ==> f(a) [= f(b)" and
    1.70  
    1.71    (* Extend definition of [= to program fragments of higher type *)
    1.72    po_abstractn:   "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))"
    1.73 @@ -119,22 +122,26 @@
    1.74    (** Equality - equivalence axioms inherited from FOL.thy   **)
    1.75    (**          - congruence of "=" is axiomatised implicitly **)
    1.76  
    1.77 +axiomatization where
    1.78    eq_iff:         "t = t' <-> t [= t' & t' [= t"
    1.79  
    1.80    (** Properties of canonical values given by greatest fixed point definitions **)
    1.81  
    1.82 -  PO_iff:         "t [= t' <-> <t,t'> : PO"
    1.83 +axiomatization where
    1.84 +  PO_iff:         "t [= t' <-> <t,t'> : PO" and
    1.85    EQ_iff:         "t =  t' <-> <t,t'> : EQ"
    1.86  
    1.87    (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **)
    1.88  
    1.89 -  caseBtrue:            "case(true,d,e,f,g) = d"
    1.90 -  caseBfalse:          "case(false,d,e,f,g) = e"
    1.91 -  caseBpair:           "case(<a,b>,d,e,f,g) = f(a,b)"
    1.92 -  caseBlam:       "case(lam x. b(x),d,e,f,g) = g(b)"
    1.93 -  caseBbot:              "case(bot,d,e,f,g) = bot"            (* strictness *)
    1.94 +axiomatization where
    1.95 +  caseBtrue:            "case(true,d,e,f,g) = d" and
    1.96 +  caseBfalse:          "case(false,d,e,f,g) = e" and
    1.97 +  caseBpair:           "case(<a,b>,d,e,f,g) = f(a,b)" and
    1.98 +  caseBlam:       "\<And>b. case(lam x. b(x),d,e,f,g) = g(b)" and
    1.99 +  caseBbot:              "case(bot,d,e,f,g) = bot"           (* strictness *)
   1.100  
   1.101    (** The theory is non-trivial **)
   1.102 +axiomatization where
   1.103    distinctness:   "~ lam x. b(x) = bot"
   1.104  
   1.105    (*** Definitions of Termination and Divergence ***)