src/HOL/Datatype_Examples/Milner_Tofte.thy
author traytel
Tue Nov 24 10:54:21 2015 +0100 (2015-11-24)
changeset 61745 e23e0ff98657
child 62136 c92d82c3f41b
permissions -rw-r--r--
Ported old example to use (co)datatypes
traytel@61745
     1
(*  Title:      HOL/Datatype_Examples/Milner_Tofte.thy
traytel@61745
     2
    Author:     Dmitriy Traytel, ETH Z├╝rich
traytel@61745
     3
    Copyright   2015
traytel@61745
     4
traytel@61745
     5
Modernized version of HOL/ex/MT.thy by Jacob Frost
traytel@61745
     6
traytel@61745
     7
Based upon the article
traytel@61745
     8
    Robin Milner and Mads Tofte,
traytel@61745
     9
    Co-induction in Relational Semantics,
traytel@61745
    10
    Theoretical Computer Science 87 (1991), pages 209-220.
traytel@61745
    11
traytel@61745
    12
Written up as
traytel@61745
    13
    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
traytel@61745
    14
    Report 308, Computer Lab, University of Cambridge (1993).
traytel@61745
    15
*)
traytel@61745
    16
traytel@61745
    17
section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close>
traytel@61745
    18
traytel@61745
    19
theory Milner_Tofte
traytel@61745
    20
imports Main
traytel@61745
    21
begin
traytel@61745
    22
traytel@61745
    23
typedecl Const
traytel@61745
    24
typedecl ExVar
traytel@61745
    25
typedecl TyConst
traytel@61745
    26
traytel@61745
    27
datatype Ex =
traytel@61745
    28
  e_const (e_const_fst: Const)
traytel@61745
    29
| e_var ExVar
traytel@61745
    30
| e_fn ExVar Ex ("fn _ => _" [0,51] 1000)
traytel@61745
    31
| e_fix ExVar ExVar Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
traytel@61745
    32
| e_app Ex Ex ("_ @@ _" [51,51] 1000)
traytel@61745
    33
traytel@61745
    34
datatype Ty =
traytel@61745
    35
  t_const TyConst
traytel@61745
    36
| t_fun Ty Ty ("_ -> _" [51,51] 1000)
traytel@61745
    37
traytel@61745
    38
datatype 'a genClos =
traytel@61745
    39
  clos_mk ExVar Ex "ExVar \<rightharpoonup> 'a" ("\<langle>_ , _ , _\<rangle>" [0,0,0] 1000)
traytel@61745
    40
traytel@61745
    41
codatatype Val =
traytel@61745
    42
  v_const Const
traytel@61745
    43
| v_clos "Val genClos"
traytel@61745
    44
traytel@61745
    45
type_synonym Clos = "Val genClos"
traytel@61745
    46
type_synonym ValEnv = "ExVar \<rightharpoonup> Val"
traytel@61745
    47
type_synonym TyEnv = "ExVar \<rightharpoonup> Ty"
traytel@61745
    48
traytel@61745
    49
axiomatization 
traytel@61745
    50
  c_app :: "[Const, Const] => Const" and
traytel@61745
    51
  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) where
traytel@61745
    52
  isof_app: "\<lbrakk>c1 isof t1 -> t2; c2 isof t1\<rbrakk> \<Longrightarrow> c_app c1 c2 isof t2"
traytel@61745
    53
traytel@61745
    54
text \<open>The dynamic semantics is defined inductively by a set of inference
traytel@61745
    55
rules.  These inference rules allows one to draw conclusions of the form ve
traytel@61745
    56
|- e ---> v, read the expression e evaluates to the value v in the value
traytel@61745
    57
environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
traytel@61745
    58
as the least fixpoint of the functor eval_fun below.  From this definition
traytel@61745
    59
introduction rules and a strong elimination (induction) rule can be derived.\<close>
traytel@61745
    60
traytel@61745
    61
inductive eval :: "[ValEnv, Ex, Val] => bool" ("_ \<turnstile> _ ---> _" [36,0,36] 50) where
traytel@61745
    62
  eval_const: "ve \<turnstile> e_const c ---> v_const c"
traytel@61745
    63
| eval_var2:  "ev \<in> dom ve  \<Longrightarrow> ve \<turnstile> e_var ev ---> the (ve ev)"
traytel@61745
    64
| eval_fn:    "ve \<turnstile> fn ev => e ---> v_clos \<langle>ev, e, ve\<rangle>"
traytel@61745
    65
| eval_fix:   "cl = \<langle>ev1, e, ve(ev2 \<mapsto> v_clos cl)\<rangle> \<Longrightarrow> ve \<turnstile> fix ev2(ev1) = e ---> v_clos(cl)"
traytel@61745
    66
| eval_app1:  "\<lbrakk>ve \<turnstile> e1 ---> v_const c1; ve \<turnstile> e2 ---> v_const c2\<rbrakk> \<Longrightarrow>
traytel@61745
    67
                ve \<turnstile> e1 @@ e2 ---> v_const (c_app c1 c2)"
traytel@61745
    68
| 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>
traytel@61745
    69
                ve \<turnstile> e1 @@ e2 ---> v"
traytel@61745
    70
traytel@61745
    71
declare eval.intros[intro]
traytel@61745
    72
traytel@61745
    73
text \<open>The static semantics is defined in the same way as the dynamic
traytel@61745
    74
semantics.  The relation te |- e ===> t express the expression e has the
traytel@61745
    75
type t in the type environment te.\<close>
traytel@61745
    76
traytel@61745
    77
inductive elab :: "[TyEnv, Ex, Ty] => bool" ("_ \<turnstile> _ ===> _" [36,0,36] 50) where
traytel@61745
    78
  elab_const: "c isof ty \<Longrightarrow> te \<turnstile> e_const c ===> ty"
traytel@61745
    79
| elab_var:   "x \<in> dom te \<Longrightarrow> te \<turnstile> e_var x ===> the (te x)"
traytel@61745
    80
| elab_fn:    "te(x \<mapsto> ty1) \<turnstile> e ===> ty2 \<Longrightarrow> te \<turnstile> fn x => e ===> ty1 -> ty2"
traytel@61745
    81
| elab_fix:   "te(f \<mapsto> ty1 -> ty2, x \<mapsto> ty1) \<turnstile> e ===> ty2 \<Longrightarrow> te \<turnstile> fix f x = e ===> ty1 -> ty2"
traytel@61745
    82
| elab_app:   "\<lbrakk>te \<turnstile> e1 ===> ty1 -> ty2; te \<turnstile> e2 ===> ty1\<rbrakk> \<Longrightarrow> te \<turnstile> e1 @@ e2 ===> ty2"
traytel@61745
    83
traytel@61745
    84
declare elab.intros[intro]
traytel@61745
    85
inductive_cases elabE[elim!]:
traytel@61745
    86
  "te \<turnstile> e_const(c) ===> ty"
traytel@61745
    87
  "te \<turnstile> e_var(x) ===> ty"
traytel@61745
    88
  "te \<turnstile> fn x => e ===> ty"
traytel@61745
    89
  "te \<turnstile> fix f(x) = e ===> ty"
traytel@61745
    90
  "te \<turnstile> e1 @@ e2 ===> ty"
traytel@61745
    91
traytel@61745
    92
(* The original correspondence relation *)
traytel@61745
    93
traytel@61745
    94
abbreviation isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") where
traytel@61745
    95
  "ve isofenv te \<equiv> (dom(ve) = dom(te) \<and>
traytel@61745
    96
     (\<forall>x. x \<in> dom ve \<longrightarrow> (\<exists>c. the (ve x) = v_const(c) \<and> c isof the (te x))))"
traytel@61745
    97
traytel@61745
    98
coinductive hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) where
traytel@61745
    99
  hasty_const: "c isof t \<Longrightarrow> v_const c hasty t"
traytel@61745
   100
| hasty_clos:  "\<lbrakk>te \<turnstile> fn ev => e ===> t; dom(ve) = dom(te) \<and>
traytel@61745
   101
   (\<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"
traytel@61745
   102
traytel@61745
   103
declare hasty.intros[intro]
traytel@61745
   104
inductive_cases hastyE[elim!]:
traytel@61745
   105
  "v_const c hasty t"
traytel@61745
   106
  "v_clos \<langle>xm , em , evm\<rangle> hasty u -> t"
traytel@61745
   107
traytel@61745
   108
definition hasty_env :: "[ValEnv, TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) where
traytel@61745
   109
  [simp]: "ve hastyenv te \<equiv> (dom(ve) = dom(te) \<and>
traytel@61745
   110
     (\<forall>x. x \<in> dom ve --> the (ve x) hasty the (te x)))"
traytel@61745
   111
traytel@61745
   112
theorem consistency: "\<lbrakk>ve \<turnstile> e ---> v; ve hastyenv te; te \<turnstile> e ===> t\<rbrakk> \<Longrightarrow> v hasty t"
traytel@61745
   113
proof (induct ve e v arbitrary: t te rule: eval.induct)
traytel@61745
   114
  case (eval_fix cl x e ve f)
traytel@61745
   115
  then show ?case
traytel@61745
   116
    by coinduction
traytel@61745
   117
      (auto 0 11 intro: exI[of _ "te(f \<mapsto> _)"] exI[of _ x] exI[of _ e] exI[of _ "ve(f \<mapsto> v_clos cl)"])
traytel@61745
   118
next
traytel@61745
   119
  case (eval_app2 ve e1 xm em evm e2 v2 v)
traytel@61745
   120
  then obtain u where "te \<turnstile> e1 ===> u -> t" "te \<turnstile> e2 ===> u" by auto
traytel@61745
   121
  with eval_app2(2)[of te "u -> t"] eval_app2(4)[of te u] eval_app2(1,3,5,7) show ?case
traytel@61745
   122
    by (auto 0 4 elim!: eval_app2(6)[rotated])
traytel@61745
   123
qed (auto 8 0 intro!: isof_app)
traytel@61745
   124
traytel@61745
   125
lemma basic_consistency_aux:
traytel@61745
   126
  "ve isofenv te \<Longrightarrow> ve hastyenv te"
traytel@61745
   127
  using hasty_const hasty_env_def by force
traytel@61745
   128
traytel@61745
   129
theorem basic_consistency:
traytel@61745
   130
  "\<lbrakk>ve isofenv te; ve \<turnstile> e ---> v_const c; te \<turnstile> e ===> t\<rbrakk> \<Longrightarrow> c isof t"
traytel@61745
   131
  by (auto dest: consistency intro!: basic_consistency_aux)
traytel@61745
   132
traytel@61745
   133
end