|
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 |