src/CCL/CCL.thy
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1474 3f7d67927fe2
child 3837 d7f033c74b38
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title:      CCL/ccl.thy
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     5 
     6 Classical Computational Logic for Untyped Lambda Calculus with reduction to 
     7 weak head-normal form.
     8 
     9 Based on FOL extended with set collection, a primitive higher-order logic.
    10 HOL is too strong - descriptions prevent a type of programs being defined
    11 which contains only executable terms.
    12 *)
    13 
    14 CCL = Gfp +
    15 
    16 classes prog < term
    17 
    18 default prog
    19 
    20 types i
    21 
    22 arities 
    23       i          :: prog
    24       fun        :: (prog,prog)prog
    25 
    26 consts
    27   (*** Evaluation Judgement ***)
    28   "--->"      ::       "[i,i]=>prop"          (infixl 20)
    29 
    30   (*** Bisimulations for pre-order and equality ***)
    31   "[="        ::       "['a,'a]=>o"           (infixl 50)
    32   SIM         ::       "[i,i,i set]=>o"
    33   POgen,EQgen ::       "i set => i set"
    34   PO,EQ       ::       "i set"
    35 
    36   (*** Term Formers ***)
    37   true,false  ::       "i"
    38   pair        ::       "[i,i]=>i"             ("(1<_,/_>)")
    39   lambda      ::       "(i=>i)=>i"            (binder "lam " 55)
    40   case        ::       "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
    41   "`"         ::       "[i,i]=>i"             (infixl 56)
    42   bot         ::       "i"
    43   fix         ::       "(i=>i)=>i"
    44 
    45   (*** Defined Predicates ***)
    46   Trm,Dvg     ::       "i => o"
    47 
    48 rules
    49 
    50   (******* EVALUATION SEMANTICS *******)
    51 
    52   (**  This is the evaluation semantics from which the axioms below were derived.  **)
    53   (**  It is included here just as an evaluator for FUN and has no influence on    **)
    54   (**  inference in the theory CCL.                                                **)
    55 
    56   trueV       "true ---> true"
    57   falseV      "false ---> false"
    58   pairV       "<a,b> ---> <a,b>"
    59   lamV        "lam x.b(x) ---> lam x.b(x)"
    60   caseVtrue   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c"
    61   caseVfalse  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c"
    62   caseVpair   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    63   caseVlam    "[| t ---> lam x.b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    64 
    65   (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
    66 
    67   canonical  "[| t ---> c; c==true ==> u--->v; 
    68                           c==false ==> u--->v; 
    69                     !!a b.c==<a,b> ==> u--->v; 
    70                       !!f.c==lam x.f(x) ==> u--->v |] ==> 
    71              u--->v"
    72 
    73   (* Should be derivable - but probably a bitch! *)
    74   substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"
    75 
    76   (************** LOGIC ***************)
    77 
    78   (*** Definitions used in the following rules ***)
    79 
    80   apply_def     "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))"
    81   bot_def         "bot == (lam x.x`x)`(lam x.x`x)"
    82   fix_def      "fix(f) == (lam x.f(x`x))`(lam x.f(x`x))"
    83 
    84   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
    85   (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
    86   (*  behavioural equivalence (ie the relations PO and EQ defined below).            *)
    87 
    88   SIM_def
    89   "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) | 
    90                   (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
    91                   (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
    92 
    93   POgen_def  "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
    94   EQgen_def  "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
    95 
    96   PO_def    "PO == gfp(POgen)"
    97   EQ_def    "EQ == gfp(EQgen)"
    98 
    99   (*** Rules ***)
   100 
   101   (** Partial Order **)
   102 
   103   po_refl        "a [= a"
   104   po_trans       "[| a [= b;  b [= c |] ==> a [= c"
   105   po_cong        "a [= b ==> f(a) [= f(b)"
   106 
   107   (* Extend definition of [= to program fragments of higher type *)
   108   po_abstractn   "(!!x. f(x) [= g(x)) ==> (%x.f(x)) [= (%x.g(x))"
   109 
   110   (** Equality - equivalence axioms inherited from FOL.thy   **)
   111   (**          - congruence of "=" is axiomatised implicitly **)
   112 
   113   eq_iff         "t = t' <-> t [= t' & t' [= t"
   114 
   115   (** Properties of canonical values given by greatest fixed point definitions **)
   116  
   117   PO_iff         "t [= t' <-> <t,t'> : PO"
   118   EQ_iff         "t =  t' <-> <t,t'> : EQ"
   119 
   120   (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **)
   121 
   122   caseBtrue            "case(true,d,e,f,g) = d"
   123   caseBfalse          "case(false,d,e,f,g) = e"
   124   caseBpair           "case(<a,b>,d,e,f,g) = f(a,b)"
   125   caseBlam       "case(lam x.b(x),d,e,f,g) = g(b)"
   126   caseBbot              "case(bot,d,e,f,g) = bot"            (* strictness *)
   127 
   128   (** The theory is non-trivial **)
   129   distinctness   "~ lam x.b(x) = bot"
   130 
   131   (*** Definitions of Termination and Divergence ***)
   132 
   133   Dvg_def  "Dvg(t) == t = bot"
   134   Trm_def  "Trm(t) == ~ Dvg(t)"
   135 
   136 end
   137 
   138 
   139 (*
   140 Would be interesting to build a similar theory for a typed programming language:
   141     ie.     true :: bool,      fix :: ('a=>'a)=>'a  etc......
   142 
   143 This is starting to look like LCF.
   144 What are the advantages of this approach?   
   145         - less axiomatic                                            
   146         - wfd induction / coinduction and fixed point induction available
   147            
   148 *)