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