# Theory CCL

Up to index of Isabelle/CCL

theory CCL
imports Gfp
uses [CCL.ML]
begin

    (*  Title:      CCL/CCL.thy
        ID:         $Id: CCL.thy,v 1.6 2005/09/17 15:35:27 wenzelm Exp $
        Author:     Martin Coen
        Copyright   1993  University of Cambridge
    *)

    header {* Classical Computational Logic for Untyped Lambda Calculus
      with reduction to weak head-normal form *}

    theory CCL
    imports Gfp
    begin

    text {*
      Based on FOL extended with set collection, a primitive higher-order
      logic.  HOL is too strong - descriptions prevent a type of programs
      being defined which contains only executable terms.
    *}

    classes prog < "term"
    defaultsort prog

    arities fun :: (prog, prog) prog

    typedecl i
    arities i :: prog

    consts
      (*** Evaluation Judgement ***)
      "--->"      ::       "[i,i]=>prop"          (infixl 20)

      (*** Bisimulations for pre-order and equality ***)
      "[="        ::       "['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"
      false       ::       "i"
      pair        ::       "[i,i]=>i"             ("(1<_,/_>)")
      lambda      ::       "(i=>i)=>i"            (binder "lam " 55)
      "case"      ::       "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i"
      "`"         ::       "[i,i]=>i"             (infixl 56)
      bot         ::       "i"
      "fix"       ::       "(i=>i)=>i"

      (*** Defined Predicates ***)
      Trm         ::       "i => o"
      Dvg         ::       "i => o"

    axioms

      (******* EVALUATION SEMANTICS *******)

      (**  This is the evaluation semantics from which the axioms below were derived.  **)
      (**  It is included here just as an evaluator for FUN and has no influence on    **)
      (**  inference in the theory CCL.                                                **)

      trueV:       "true ---> true"
      falseV:      "false ---> false"
      pairV:       "<a,b> ---> <a,b>"
      lamV:        "lam x. b(x) ---> lam x. b(x)"
      caseVtrue:   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c"
      caseVfalse:  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c"
      caseVpair:   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
      caseVlam:    "[| t ---> lam x. b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"

      (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)

      canonical:  "[| t ---> c; c==true ==> u--->v;
                              c==false ==> u--->v;
                        !!a b. c==<a,b> ==> u--->v;
                          !!f. c==lam x. f(x) ==> u--->v |] ==>
                 u--->v"

      (* Should be derivable - but probably a bitch! *)
      substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')"

      (************** LOGIC ***************)

      (*** Definitions used in the following rules ***)

      apply_def:     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
      bot_def:         "bot == (lam x. x`x)`(lam x. x`x)"
      fix_def:      "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:
      "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))}"

      PO_def:    "PO == gfp(POgen)"
      EQ_def:    "EQ == gfp(EQgen)"

      (*** Rules ***)

      (** Partial Order **)

      po_refl:        "a [= a"
      po_trans:       "[| a [= b;  b [= c |] ==> a [= c"
      po_cong:        "a [= b ==> f(a) [= f(b)"

      (* Extend definition of [= to program fragments of higher type *)
      po_abstractn:   "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))"

      (** Equality - equivalence axioms inherited from FOL.thy   **)
      (**          - congruence of "=" is axiomatised implicitly **)

      eq_iff:         "t = t' <-> t [= t' & t' [= t"

      (** Properties of canonical values given by greatest fixed point definitions **)

      PO_iff:         "t [= t' <-> <t,t'> : PO"
      EQ_iff:         "t =  t' <-> <t,t'> : EQ"

      (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **)

      caseBtrue:            "case(true,d,e,f,g) = d"
      caseBfalse:          "case(false,d,e,f,g) = e"
      caseBpair:           "case(<a,b>,d,e,f,g) = f(a,b)"
      caseBlam:       "case(lam x. b(x),d,e,f,g) = g(b)"
      caseBbot:              "case(bot,d,e,f,g) = bot"            (* strictness *)

      (** The theory is non-trivial **)
      distinctness:   "~ lam x. b(x) = bot"

      (*** Definitions of Termination and Divergence ***)

      Dvg_def:  "Dvg(t) == t = bot"
      Trm_def:  "Trm(t) == ~ Dvg(t)"

    text {*
    Would be interesting to build a similar theory for a typed programming language:
        ie.     true :: bool,      fix :: ('a=>'a)=>'a  etc......

    This is starting to look like LCF.
    What are the advantages of this approach?
            - less axiomatic
            - wfd induction / coinduction and fixed point induction available
    *}

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem fun_cong:

      f = g ==> f(x) = g(x)

theorem arg_cong:

      x = y ==> f(x) = f(y)

theorem abstractn:

      (!!x. f(x) = g(x)) ==> f = g

theorem Trm_iff:

      Trm(t) <-> t ≠ bot

theorem Dvg_iff:

      Dvg(t) <-> t = bot

theorem eq_lemma:

      [| x = a; y = b; x = y |] ==> a = b

theorem XHlemma1:

      [| A = B; a : B <-> P |] ==> a : A <-> P

theorem XHlemma2:

      P(t, t') <-> Q ==> <t,t'> : {p. ∃t t'. p = <t,t'> ∧ P(t, t')} <-> Q

theorem POgen_mono:

      mono(POgen)

theorem POgenXH:

      <t,t'> : POgen(R) <->
      t = bot ∨
      t = true ∧ t' = true ∨
      t = false ∧ t' = false ∨
      (∃a a' b b'. t = <a,b> ∧ t' = <a',b'> ∧ <a,a'> : R ∧ <b,b'> : R) ∨
      (∃f f'. t = lam x. f(x) ∧ t' = lam x. f'(x) ∧ (∀x. <f(x),f'(x)> : R))

theorem poXH:

      t [= t' <->
      t = bot ∨
      t = true ∧ t' = true ∨
      t = false ∧ t' = false ∨
      (∃a a' b b'. t = <a,b> ∧ t' = <a',b'> ∧ a [= a' ∧ b [= b') ∨
      (∃f f'. t = lam x. f(x) ∧ t' = lam x. f'(x) ∧ (∀x. f(x) [= f'(x)))

theorem po_bot:

      bot [= b

theorem bot_poleast:

      a [= bot ==> a = bot

theorem po_pair:

      <a,b> [= <a',b'> <-> a [= a' ∧ b [= b'

theorem po_lam:

      lam x. f(x) [= lam x. f'(x) <-> (∀x. f(x) [= f'(x))

theorem case_pocong:

      [| t [= t'; a [= a'; b [= b'; !!x y. c(x, y) [= c'(x, y); !!u. d(u) [= d'(u) |]
      ==> case(t, a, b, c, d) [= case(t', a', b', c', d')

theorem apply_pocong:

      [| f [= f'; a [= a' |] ==> f ` a [= f' ` a'

theorem npo_lam_bot:

      ¬ lam x. b(x) [= bot

theorem po_lemma:

      [| x = a; y = b; x [= y |] ==> a [= b

theorem npo_pair_lam:

      ¬ <a,b> [= lam x. f(x)

theorem npo_lam_pair:

      ¬ lam x. f(x) [= <a,b>

theorem po_coinduct:

      [| <t,u> : R; R <= POgen(R) |] ==> t [= u

theorem EQgen_mono:

      mono(EQgen)

theorem EQgenXH:

      <t,t'> : EQgen(R) <->
      t = bot ∧ t' = bot ∨
      t = true ∧ t' = true ∨
      t = false ∧ t' = false ∨
      (∃a a' b b'. t = <a,b> ∧ t' = <a',b'> ∧ <a,a'> : R ∧ <b,b'> : R) ∨
      (∃f f'. t = lam x. f(x) ∧ t' = lam x. f'(x) ∧ (∀x. <f(x),f'(x)> : R))

theorem eqXH:

      t = t' <->
      t = bot ∧ t' = bot ∨
      t = true ∧ t' = true ∨
      t = false ∧ t' = false ∨
      (∃a a' b b'. t = <a,b> ∧ t' = <a',b'> ∧ a = a' ∧ b = b') ∨
      (∃f f'. t = lam x. f(x) ∧ t' = lam x. f'(x) ∧ (∀x. f(x) = f'(x)))

theorem eq_coinduct:

      [| <t,u> : R; R <= EQgen(R) |] ==> t = u

theorem eq_coinduct3:

      [| <t,u> : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u

theorem cond_eta:

      ∃f. t = lam x. f(x) ==> t = lam x. t ` x

theorem exhaustion:

      t = bot ∨ t = true ∨ t = false ∨ (∃a b. t = <a,b>) ∨ (∃f. t = lam x. f(x))

theorem term_case:

      [| P(bot); P(true); P(false); !!x y. P(<x,y>); !!b. P(lam x. b(x)) |] ==> P(t)