Theory Milner_Tofte

(*  Title:      HOL/Datatype_Examples/Milner_Tofte.thy
    Author:     Dmitriy Traytel, ETH Zürich
    Copyright   2015

Modernized version of an old development by Jacob Frost

Based upon the article
    Robin Milner and Mads Tofte,
    Co-induction in Relational Semantics,
    Theoretical Computer Science 87 (1991), pages 209-220.

Written up as
    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
    Report 308, Computer Lab, University of Cambridge (1993).
*)

section ‹Milner-Tofte: Co-induction in Relational Semantics›

theory Milner_Tofte
imports Main
begin

typedecl Const
typedecl ExVar
typedecl TyConst

datatype Ex =
  e_const (e_const_fst: Const)
| e_var ExVar
| e_fn ExVar Ex ("fn _ => _" [0,51] 1000)
| e_fix ExVar ExVar Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
| e_app Ex Ex ("_ @@ _" [51,51] 1000)

datatype Ty =
  t_const TyConst
| t_fun Ty Ty ("_ -> _" [51,51] 1000)

datatype 'a genClos =
  clos_mk ExVar Ex "ExVar ⇀ 'a" ("⟨_ , _ , _⟩" [0,0,0] 1000)

codatatype Val =
  v_const Const
| v_clos "Val genClos"

type_synonym Clos = "Val genClos"
type_synonym ValEnv = "ExVar ⇀ Val"
type_synonym TyEnv = "ExVar ⇀ Ty"

axiomatization 
  c_app :: "[Const, Const] => Const" and
  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) where
  isof_app: "⟦c1 isof t1 -> t2; c2 isof t1⟧ ⟹ c_app c1 c2 isof t2"

text ‹The dynamic semantics is defined inductively by a set of inference
rules.  These inference rules allows one to draw conclusions of the form ve
|- e ---> v, read the expression e evaluates to the value v in the value
environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
as the least fixpoint of the functor eval_fun below.  From this definition
introduction rules and a strong elimination (induction) rule can be derived.›

inductive eval :: "[ValEnv, Ex, Val] => bool" ("_ ⊢ _ ---> _" [36,0,36] 50) where
  eval_const: "ve ⊢ e_const c ---> v_const c"
| eval_var2:  "ev ∈ dom ve  ⟹ ve ⊢ e_var ev ---> the (ve ev)"
| eval_fn:    "ve ⊢ fn ev => e ---> v_clos ⟨ev, e, ve⟩"
| eval_fix:   "cl = ⟨ev1, e, ve(ev2 ↦ v_clos cl)⟩ ⟹ ve ⊢ fix ev2(ev1) = e ---> v_clos(cl)"
| eval_app1:  "⟦ve ⊢ e1 ---> v_const c1; ve ⊢ e2 ---> v_const c2⟧ ⟹
                ve ⊢ e1 @@ e2 ---> v_const (c_app c1 c2)"
| eval_app2:  "⟦ve ⊢ e1 ---> v_clos ⟨xm, em, vem⟩; ve ⊢ e2 ---> v2; vem(xm ↦ v2) ⊢ em ---> v⟧ ⟹
                ve ⊢ e1 @@ e2 ---> v"

declare eval.intros[intro]

text ‹The static semantics is defined in the same way as the dynamic
semantics.  The relation te |- e ===> t express the expression e has the
type t in the type environment te.›

inductive elab :: "[TyEnv, Ex, Ty] => bool" ("_ ⊢ _ ===> _" [36,0,36] 50) where
  elab_const: "c isof ty ⟹ te ⊢ e_const c ===> ty"
| elab_var:   "x ∈ dom te ⟹ te ⊢ e_var x ===> the (te x)"
| elab_fn:    "te(x ↦ ty1) ⊢ e ===> ty2 ⟹ te ⊢ fn x => e ===> ty1 -> ty2"
| elab_fix:   "te(f ↦ ty1 -> ty2, x ↦ ty1) ⊢ e ===> ty2 ⟹ te ⊢ fix f x = e ===> ty1 -> ty2"
| elab_app:   "⟦te ⊢ e1 ===> ty1 -> ty2; te ⊢ e2 ===> ty1⟧ ⟹ te ⊢ e1 @@ e2 ===> ty2"

declare elab.intros[intro]
inductive_cases elabE[elim!]:
  "te ⊢ e_const(c) ===> ty"
  "te ⊢ e_var(x) ===> ty"
  "te ⊢ fn x => e ===> ty"
  "te ⊢ fix f(x) = e ===> ty"
  "te ⊢ e1 @@ e2 ===> ty"

(* The original correspondence relation *)

abbreviation isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") where
  "ve isofenv te ≡ (dom(ve) = dom(te) ∧
     (∀x. x ∈ dom ve ⟶ (∃c. the (ve x) = v_const(c) ∧ c isof the (te x))))"

coinductive hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) where
  hasty_const: "c isof t ⟹ v_const c hasty t"
| hasty_clos:  "⟦te ⊢ fn ev => e ===> t; dom(ve) = dom(te) ∧
   (∀x. x ∈ dom ve --> the (ve x) hasty the (te x)); cl = ⟨ev,e,ve⟩⟧ ⟹ v_clos cl hasty t"

declare hasty.intros[intro]
inductive_cases hastyE[elim!]:
  "v_const c hasty t"
  "v_clos ⟨xm , em , evm⟩ hasty u -> t"

definition hasty_env :: "[ValEnv, TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) where
  [simp]: "ve hastyenv te ≡ (dom(ve) = dom(te) ∧
     (∀x. x ∈ dom ve --> the (ve x) hasty the (te x)))"

theorem consistency: "⟦ve ⊢ e ---> v; ve hastyenv te; te ⊢ e ===> t⟧ ⟹ v hasty t"
proof (induct ve e v arbitrary: t te rule: eval.induct)
  case (eval_fix cl x e ve f)
  then show ?case
    by coinduction
      (auto 0 11 intro: exI[of _ "te(f ↦ _)"] exI[of _ x] exI[of _ e] exI[of _ "ve(f ↦ v_clos cl)"])
next
  case (eval_app2 ve e1 xm em evm e2 v2 v)
  then obtain u where "te ⊢ e1 ===> u -> t" "te ⊢ e2 ===> u" by auto
  with eval_app2(2)[of te "u -> t"] eval_app2(4)[of te u] eval_app2(1,3,5,7) show ?case
    by (auto 0 4 elim!: eval_app2(6)[rotated])
qed (auto 8 0 intro!: isof_app)

lemma basic_consistency_aux:
  "ve isofenv te ⟹ ve hastyenv te"
  using hasty_const hasty_env_def by force

theorem basic_consistency:
  "⟦ve isofenv te; ve ⊢ e ---> v_const c; te ⊢ e ===> t⟧ ⟹ c isof t"
  by (auto dest: consistency intro!: basic_consistency_aux)

end