Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: CCL.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      CCL/CCL.thy
    Author:     Martin Coen
    Copyright   1993  University of Cambridge
*)

section \<open>Classical Computational Logic for Untyped Lambda Calculus
  with reduction to weak head-normal form\<close>

theory CCL
imports Gfp
begin

text \<open>
  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.
\<close>

class prog = "term"
default_sort prog

instance "fun" :: (prog, prog) prog ..

typedecl i
instance i :: prog ..

consts
  (*** Evaluation Judgement ***)
  Eval      ::       "[i,i]\prop" (infixl "\" 20)

  (*** Bisimulations for pre-order and equality ***)
  po          ::       "['a,'a]\o" (infixl "[=" 50)

  (*** 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"
  "apply"     ::       "[i,i]\i" (infixl "`" 56)
  bot         ::       "i"

  (******* 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.                                                **)

axiomatization where
  trueV:       "true \ true" and
  falseV:      "false \ false" and
  pairV:       " \ " and
  lamV:        "\b. lam x. b(x) \ lam x. b(x)" and

  caseVtrue:   "\t \ true; d \ c\ \ case(t,d,e,f,g) \ c" and
  caseVfalse:  "\t \ false; e \ c\ \ case(t,d,e,f,g) \ c" and
  caseVpair:   "\t \ ; f(a,b) \ c\ \ case(t,d,e,f,g) \ c" and
  caseVlam:    "\b. \t \ lam x. b(x); g(b) \ c\ \ case(t,d,e,f,g) \ c"

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

axiomatization where
  canonical:  "\t \ c; c==true \ u\v;
                          c==false \<Longrightarrow> u\<longlongrightarrow>v;
                    \<And>a b. c==<a,b> \<Longrightarrow> u\<longlongrightarrow>v;
                      \<And>f. c==lam x. f(x) \<Longrightarrow> u\<longlongrightarrow>v\<rbrakk> \<Longrightarrow>
             u\<longlongrightarrow>v"

  (* Should be derivable - but probably a bitch! *)
axiomatization where
  substitute: "\a==a'; t(a)\c(a)\ \ t(a')\c(a')"

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

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

axiomatization where
  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))"

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).            *)

definition SIM :: "[i,i,i set]\o"
  where
  "SIM(t,t',R) == (t=true \ t'=true) | (t=false \ t'=false) |
                  (\<exists>a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (\<exists>f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"

definition POgen :: "i set \ i set"
  where "POgen(R) == {p. \t t'. p= \ (t = bot | SIM(t,t',R))}"

definition EQgen :: "i set \ i set"
  where "EQgen(R) == {p. \t t'. p= \ (t = bot \ t' = bot | SIM(t,t',R))}"

definition PO :: "i set"
  where "PO == gfp(POgen)"

definition EQ :: "i set"
  where "EQ == gfp(EQgen)"

  (*** Rules ***)

  (** Partial Order **)

axiomatization where
  po_refl:        "a [= a" and
  po_trans:       "\a [= b; b [= c\ \ a [= c" and
  po_cong:        "a [= b \ f(a) [= f(b)" and

  (* 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 **)

axiomatization where
  eq_iff:         "t = t' \ t [= t' \ t' [= t"

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

axiomatization where
  PO_iff:         "t [= t' \ : PO" and
  EQ_iff:         "t = t' \ : EQ"

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

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

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

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

definition Dvg :: "i \ o"
  where "Dvg(t) == t = bot"

definition Trm :: "i \ o"
  where "Trm(t) == \ Dvg(t)"

text \<open>
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
\<close>

lemmas ccl_data_defs = apply_def fix_def

declare po_refl [simp]

subsection \<open>Congruence Rules\<close>

(*similar to AP_THM in Gordon's HOL*)
lemma fun_cong: "(f::'a\'b) = g \ f(x)=g(x)"
  by simp

(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
lemma arg_cong: "x=y \ f(x)=f(y)"
  by simp

lemma abstractn: "(\x. f(x) = g(x)) \ f = g"
  apply (simp add: eq_iff)
  apply (blast intro: po_abstractn)
  done

lemmas caseBs = caseBtrue caseBfalse caseBpair caseBlam caseBbot

subsection \<open>Termination and Divergence\<close>

lemma Trm_iff: "Trm(t) \ \ t = bot"
  by (simp add: Trm_def Dvg_def)

lemma Dvg_iff: "Dvg(t) \ t = bot"
  by (simp add: Trm_def Dvg_def)

subsection \<open>Constructors are injective\<close>

lemma eq_lemma: "\x=a; y=b; x=y\ \ a=b"
  by simp

ML \<open>
  fun inj_rl_tac ctxt rews i =
    let
      fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
      val inj_lemmas = maps mk_inj_lemmas rews
    in
      CHANGED (REPEAT (assume_tac ctxt i ORELSE
        resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
        eresolve_tac ctxt inj_lemmas i ORELSE
        asm_simp_tac (ctxt addsimps rews) i))
    end;
\<close>

method_setup inj_rl = \<open>
  Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
\<close>

lemma ccl_injs:
  " = \ (a=a' \ b=b')"
  "\b b'. (lam x. b(x) = lam x. b'(x)) \ ((ALL z. b(z)=b'(z)))"
  by (inj_rl caseBs)

lemma pair_inject: " = \ (a = a' \ b = b' \ R) \ R"
  by (simp add: ccl_injs)

subsection \<open>Constructors are distinct\<close>

lemma lem: "t=t' \ case(t,b,c,d,e) = case(t',b,c,d,e)"
  by simp

ML \<open>
local
  fun pairs_of f x [] = []
    | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)

  fun mk_combs ff [] = []
    | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs

  (* Doesn't handle binder types correctly *)
  fun saturate thy sy name =
       let fun arg_str 0 a s = s
         | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
         | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
           val T = Sign.the_const_type thy (Sign.intern_const thy sy);
           val arity = length (binder_types T)
       in sy ^ (arg_str arity name "") end

  fun mk_thm_str thy a b = "\ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")

  val lemma = @{thm lem};
  val eq_lemma = @{thm eq_lemma};
  val distinctness = @{thm distinctness};
  fun mk_lemma (ra,rb) =
    [lemma] RL [ra RS (rb RS eq_lemma)] RL
    [distinctness RS @{thm notE}, @{thm sym} RS (distinctness RS @{thm notE})]
in
  fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
  fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
end
\<close>

ML \<open>
val caseB_lemmas = mk_lemmas @{thms caseBs}

val ccl_dstncts =
  let
    fun mk_raw_dstnct_thm rls s =
      Goal.prove_global \<^theory> [] [] (Syntax.read_prop_global \<^theory> s)
        (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1)
  in map (mk_raw_dstnct_thm caseB_lemmas)
    (mk_dstnct_rls \<^theory> ["bot","true","false","pair","lambda"]) end

fun mk_dstnct_thms ctxt defs inj_rls xs =
  let
    val thy = Proof_Context.theory_of ctxt;
    fun mk_dstnct_thm rls s =
      Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
        (fn _ =>
          rewrite_goals_tac ctxt defs THEN
          simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
  in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end

fun mkall_dstnct_thms ctxt defs i_rls xss = maps (mk_dstnct_thms ctxt defs i_rls) xss

(*** Rewriting and Proving ***)

fun XH_to_I rl = rl RS @{thm iffD2}
fun XH_to_D rl = rl RS @{thm iffD1}
val XH_to_E = make_elim o XH_to_D
val XH_to_Is = map XH_to_I
val XH_to_Ds = map XH_to_D
val XH_to_Es = map XH_to_E;

ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
\<close>

lemmas [simp] = ccl_rews
  and [elim!] = pair_inject ccl_dstnctsEs
  and [dest!] = ccl_injDs

subsection \<open>Facts from gfp Definition of \<open>[=\<close> and \<open>=\<close>\<close>

lemma XHlemma1: "\A=B; a:B \ P\ \ a:A \ P"
  by simp

lemma XHlemma2: "(P(t,t') \ Q) \ ( : {p. \t t'. p= \ P(t,t')} \ Q)"
  by blast

subsection \<open>Pre-Order\<close>

lemma POgen_mono: "mono(\X. POgen(X))"
  apply (unfold POgen_def SIM_def)
  apply (rule monoI)
  apply blast
  done

lemma POgenXH:
  " : POgen(R) \ t= bot | (t=true \ t'=true) | (t=false \ t'=false) |
           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
           (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. : R))"
  apply (unfold POgen_def SIM_def)
  apply (rule iff_refl [THEN XHlemma2])
  done

lemma poXH:
  "t [= t' \ t=bot | (t=true \ t'=true) | (t=false \ t'=false) |
                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                 (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. f(x) [= f'(x)))"
  apply (simp add: PO_iff del: ex_simps)
  apply (rule POgen_mono
    [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def])
  apply (rule iff_refl [THEN XHlemma2])
  done

lemma po_bot: "bot [= b"
  apply (rule poXH [THEN iffD2])
  apply simp
  done

lemma bot_poleast: "a [= bot \ a=bot"
  apply (drule poXH [THEN iffD1])
  apply simp
  done

lemma po_pair: " [= \ a [= a' \ b [= b'"
  apply (rule poXH [THEN iff_trans])
  apply simp
  done

lemma po_lam: "lam x. f(x) [= lam x. f'(x) \ (ALL x. f(x) [= f'(x))"
  apply (rule poXH [THEN iff_trans])
  apply fastforce
  done

lemmas ccl_porews = po_bot po_pair po_lam

lemma case_pocong:
  assumes 1: "t [= t'"
    and 2: "a [= a'"
    and 3: "b [= b'"
    and 4: "\x y. c(x,y) [= c'(x,y)"
    and 5: "\u. d(u) [= d'(u)"
  shows "case(t,a,b,c,d) [= case(t',a',b',c',d')"
  apply (rule 1 [THEN po_cong, THEN po_trans])
  apply (rule 2 [THEN po_cong, THEN po_trans])
  apply (rule 3 [THEN po_cong, THEN po_trans])
  apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans])
  apply (rule_tac f1 = "\d. case (t',a',b',c',d)" in
    5 [THEN po_abstractn, THEN po_cong, THEN po_trans])
  apply (rule po_refl)
  done

lemma apply_pocong: "\f [= f'; a [= a'\ \ f ` a [= f' ` a'"
  unfolding ccl_data_defs
  apply (rule case_pocong, (rule po_refl | assumption)+)
  apply (erule po_cong)
  done

lemma npo_lam_bot: "\ lam x. b(x) [= bot"
  apply (rule notI)
  apply (drule bot_poleast)
  apply (erule distinctness [THEN notE])
  done

lemma po_lemma: "\x=a; y=b; x[=y\ \ a[=b"
  by simp

lemma npo_pair_lam: "\ [= lam x. f(x)"
  apply (rule notI)
  apply (rule npo_lam_bot [THEN notE])
  apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]])
  apply (rule po_refl npo_lam_bot)+
  done

lemma npo_lam_pair: "\ lam x. f(x) [= "
  apply (rule notI)
  apply (rule npo_lam_bot [THEN notE])
  apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]])
  apply (rule po_refl npo_lam_bot)+
  done

lemma npo_rls1:
  "\ true [= false"
  "\ false [= true"
  "\ true [= "
  "\ [= true"
  "\ true [= lam x. f(x)"
  "\ lam x. f(x) [= true"
  "\ false [= "
  "\ [= false"
  "\ false [= lam x. f(x)"
  "\ lam x. f(x) [= false"
  by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all,
    (rule po_refl npo_lam_bot)+)+

lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1

subsection \<open>Coinduction for \<open>[=\<close>\<close>

lemma po_coinduct: "\ : R; R <= POgen(R)\ \ t [= u"
  apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]])
   apply assumption+
  done

subsection \<open>Equality\<close>

lemma EQgen_mono: "mono(\X. EQgen(X))"
  apply (unfold EQgen_def SIM_def)
  apply (rule monoI)
  apply blast
  done

lemma EQgenXH:
  " : EQgen(R) \ (t=bot \ t'=bot) | (t=true \ t'=true) |
                                             (t=false \<and> t'=false) |
                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                 (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. : R))"
  apply (unfold EQgen_def SIM_def)
  apply (rule iff_refl [THEN XHlemma2])
  done

lemma eqXH:
  "t=t' \ (t=bot \ t'=bot) | (t=true \ t'=true) | (t=false \ t'=false) |
                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                     (EX f f'. t=lam x. f(x) \ t'=lam x. f'(x) \ (ALL x. f(x)=f'(x)))"
  apply (subgoal_tac " : EQ \
    (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
    (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : EQ \<and> <b,b'> : EQ) |
    (EX f f'. t=lam x. f (x) \ t'=lam x. f' (x) \ (ALL x. : EQ))")
  apply (erule rev_mp)
  apply (simp add: EQ_iff [THEN iff_sym])
  apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1,
    unfolded EQgen_def SIM_def])
  apply (rule iff_refl [THEN XHlemma2])
  done

lemma eq_coinduct: "\ : R; R <= EQgen(R)\ \ t = u"
  apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]])
   apply assumption+
  done

lemma eq_coinduct3:
  "\ : R; R <= EQgen(lfp(\x. EQgen(x) Un R Un EQ))\ \ t = u"
  apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]])
  apply (rule EQgen_mono | assumption)+
  done

method_setup eq_coinduct3 = \<open>
  Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
    SIMPLE_METHOD'
      (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
\<close>

subsection \<open>Untyped Case Analysis and Other Facts\<close>

lemma cond_eta: "(EX f. t=lam x. f(x)) \ t = lam x.(t ` x)"
  by (auto simp: apply_def)

lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=) | (EX f. t=lam x. f(x))"
  apply (cut_tac refl [THEN eqXH [THEN iffD1]])
  apply blast
  done

lemma term_case:
  "\P(bot); P(true); P(false); \x y. P(); \b. P(lam x. b(x))\ \ P(t)"
  using exhaustion [of t] by blast

end

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.