src/HOL/Datatype_Examples/Milner_Tofte.thy
changeset 61745 e23e0ff98657
child 62136 c92d82c3f41b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Datatype_Examples/Milner_Tofte.thy	Tue Nov 24 10:54:21 2015 +0100
     1.3 @@ -0,0 +1,133 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/Milner_Tofte.thy
     1.5 +    Author:     Dmitriy Traytel, ETH Z├╝rich
     1.6 +    Copyright   2015
     1.7 +
     1.8 +Modernized version of HOL/ex/MT.thy by Jacob Frost
     1.9 +
    1.10 +Based upon the article
    1.11 +    Robin Milner and Mads Tofte,
    1.12 +    Co-induction in Relational Semantics,
    1.13 +    Theoretical Computer Science 87 (1991), pages 209-220.
    1.14 +
    1.15 +Written up as
    1.16 +    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
    1.17 +    Report 308, Computer Lab, University of Cambridge (1993).
    1.18 +*)
    1.19 +
    1.20 +section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close>
    1.21 +
    1.22 +theory Milner_Tofte
    1.23 +imports Main
    1.24 +begin
    1.25 +
    1.26 +typedecl Const
    1.27 +typedecl ExVar
    1.28 +typedecl TyConst
    1.29 +
    1.30 +datatype Ex =
    1.31 +  e_const (e_const_fst: Const)
    1.32 +| e_var ExVar
    1.33 +| e_fn ExVar Ex ("fn _ => _" [0,51] 1000)
    1.34 +| e_fix ExVar ExVar Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
    1.35 +| e_app Ex Ex ("_ @@ _" [51,51] 1000)
    1.36 +
    1.37 +datatype Ty =
    1.38 +  t_const TyConst
    1.39 +| t_fun Ty Ty ("_ -> _" [51,51] 1000)
    1.40 +
    1.41 +datatype 'a genClos =
    1.42 +  clos_mk ExVar Ex "ExVar \<rightharpoonup> 'a" ("\<langle>_ , _ , _\<rangle>" [0,0,0] 1000)
    1.43 +
    1.44 +codatatype Val =
    1.45 +  v_const Const
    1.46 +| v_clos "Val genClos"
    1.47 +
    1.48 +type_synonym Clos = "Val genClos"
    1.49 +type_synonym ValEnv = "ExVar \<rightharpoonup> Val"
    1.50 +type_synonym TyEnv = "ExVar \<rightharpoonup> Ty"
    1.51 +
    1.52 +axiomatization 
    1.53 +  c_app :: "[Const, Const] => Const" and
    1.54 +  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) where
    1.55 +  isof_app: "\<lbrakk>c1 isof t1 -> t2; c2 isof t1\<rbrakk> \<Longrightarrow> c_app c1 c2 isof t2"
    1.56 +
    1.57 +text \<open>The dynamic semantics is defined inductively by a set of inference
    1.58 +rules.  These inference rules allows one to draw conclusions of the form ve
    1.59 +|- e ---> v, read the expression e evaluates to the value v in the value
    1.60 +environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
    1.61 +as the least fixpoint of the functor eval_fun below.  From this definition
    1.62 +introduction rules and a strong elimination (induction) rule can be derived.\<close>
    1.63 +
    1.64 +inductive eval :: "[ValEnv, Ex, Val] => bool" ("_ \<turnstile> _ ---> _" [36,0,36] 50) where
    1.65 +  eval_const: "ve \<turnstile> e_const c ---> v_const c"
    1.66 +| eval_var2:  "ev \<in> dom ve  \<Longrightarrow> ve \<turnstile> e_var ev ---> the (ve ev)"
    1.67 +| eval_fn:    "ve \<turnstile> fn ev => e ---> v_clos \<langle>ev, e, ve\<rangle>"
    1.68 +| eval_fix:   "cl = \<langle>ev1, e, ve(ev2 \<mapsto> v_clos cl)\<rangle> \<Longrightarrow> ve \<turnstile> fix ev2(ev1) = e ---> v_clos(cl)"
    1.69 +| eval_app1:  "\<lbrakk>ve \<turnstile> e1 ---> v_const c1; ve \<turnstile> e2 ---> v_const c2\<rbrakk> \<Longrightarrow>
    1.70 +                ve \<turnstile> e1 @@ e2 ---> v_const (c_app c1 c2)"
    1.71 +| eval_app2:  "\<lbrakk>ve \<turnstile> e1 ---> v_clos \<langle>xm, em, vem\<rangle>; ve \<turnstile> e2 ---> v2; vem(xm \<mapsto> v2) \<turnstile> em ---> v\<rbrakk> \<Longrightarrow>
    1.72 +                ve \<turnstile> e1 @@ e2 ---> v"
    1.73 +
    1.74 +declare eval.intros[intro]
    1.75 +
    1.76 +text \<open>The static semantics is defined in the same way as the dynamic
    1.77 +semantics.  The relation te |- e ===> t express the expression e has the
    1.78 +type t in the type environment te.\<close>
    1.79 +
    1.80 +inductive elab :: "[TyEnv, Ex, Ty] => bool" ("_ \<turnstile> _ ===> _" [36,0,36] 50) where
    1.81 +  elab_const: "c isof ty \<Longrightarrow> te \<turnstile> e_const c ===> ty"
    1.82 +| elab_var:   "x \<in> dom te \<Longrightarrow> te \<turnstile> e_var x ===> the (te x)"
    1.83 +| elab_fn:    "te(x \<mapsto> ty1) \<turnstile> e ===> ty2 \<Longrightarrow> te \<turnstile> fn x => e ===> ty1 -> ty2"
    1.84 +| elab_fix:   "te(f \<mapsto> ty1 -> ty2, x \<mapsto> ty1) \<turnstile> e ===> ty2 \<Longrightarrow> te \<turnstile> fix f x = e ===> ty1 -> ty2"
    1.85 +| elab_app:   "\<lbrakk>te \<turnstile> e1 ===> ty1 -> ty2; te \<turnstile> e2 ===> ty1\<rbrakk> \<Longrightarrow> te \<turnstile> e1 @@ e2 ===> ty2"
    1.86 +
    1.87 +declare elab.intros[intro]
    1.88 +inductive_cases elabE[elim!]:
    1.89 +  "te \<turnstile> e_const(c) ===> ty"
    1.90 +  "te \<turnstile> e_var(x) ===> ty"
    1.91 +  "te \<turnstile> fn x => e ===> ty"
    1.92 +  "te \<turnstile> fix f(x) = e ===> ty"
    1.93 +  "te \<turnstile> e1 @@ e2 ===> ty"
    1.94 +
    1.95 +(* The original correspondence relation *)
    1.96 +
    1.97 +abbreviation isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") where
    1.98 +  "ve isofenv te \<equiv> (dom(ve) = dom(te) \<and>
    1.99 +     (\<forall>x. x \<in> dom ve \<longrightarrow> (\<exists>c. the (ve x) = v_const(c) \<and> c isof the (te x))))"
   1.100 +
   1.101 +coinductive hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) where
   1.102 +  hasty_const: "c isof t \<Longrightarrow> v_const c hasty t"
   1.103 +| hasty_clos:  "\<lbrakk>te \<turnstile> fn ev => e ===> t; dom(ve) = dom(te) \<and>
   1.104 +   (\<forall>x. x \<in> dom ve --> the (ve x) hasty the (te x)); cl = \<langle>ev,e,ve\<rangle>\<rbrakk> \<Longrightarrow> v_clos cl hasty t"
   1.105 +
   1.106 +declare hasty.intros[intro]
   1.107 +inductive_cases hastyE[elim!]:
   1.108 +  "v_const c hasty t"
   1.109 +  "v_clos \<langle>xm , em , evm\<rangle> hasty u -> t"
   1.110 +
   1.111 +definition hasty_env :: "[ValEnv, TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) where
   1.112 +  [simp]: "ve hastyenv te \<equiv> (dom(ve) = dom(te) \<and>
   1.113 +     (\<forall>x. x \<in> dom ve --> the (ve x) hasty the (te x)))"
   1.114 +
   1.115 +theorem consistency: "\<lbrakk>ve \<turnstile> e ---> v; ve hastyenv te; te \<turnstile> e ===> t\<rbrakk> \<Longrightarrow> v hasty t"
   1.116 +proof (induct ve e v arbitrary: t te rule: eval.induct)
   1.117 +  case (eval_fix cl x e ve f)
   1.118 +  then show ?case
   1.119 +    by coinduction
   1.120 +      (auto 0 11 intro: exI[of _ "te(f \<mapsto> _)"] exI[of _ x] exI[of _ e] exI[of _ "ve(f \<mapsto> v_clos cl)"])
   1.121 +next
   1.122 +  case (eval_app2 ve e1 xm em evm e2 v2 v)
   1.123 +  then obtain u where "te \<turnstile> e1 ===> u -> t" "te \<turnstile> e2 ===> u" by auto
   1.124 +  with eval_app2(2)[of te "u -> t"] eval_app2(4)[of te u] eval_app2(1,3,5,7) show ?case
   1.125 +    by (auto 0 4 elim!: eval_app2(6)[rotated])
   1.126 +qed (auto 8 0 intro!: isof_app)
   1.127 +
   1.128 +lemma basic_consistency_aux:
   1.129 +  "ve isofenv te \<Longrightarrow> ve hastyenv te"
   1.130 +  using hasty_const hasty_env_def by force
   1.131 +
   1.132 +theorem basic_consistency:
   1.133 +  "\<lbrakk>ve isofenv te; ve \<turnstile> e ---> v_const c; te \<turnstile> e ===> t\<rbrakk> \<Longrightarrow> c isof t"
   1.134 +  by (auto dest: consistency intro!: basic_consistency_aux)
   1.135 +
   1.136 +end