diff -r 61b65ffb4186 -r 9b0142dad559 ex/MT.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/MT.thy Tue Nov 09 11:08:13 1993 +0100 @@ -0,0 +1,286 @@ +(* Title: HOL/ex/mt.thy + ID: $Id$ + Author: Jacob Frost, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +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). +*) + +MT = Gfp + + +types + Const 0 + + ExVar 0 + Ex 0 + + TyConst 0 + Ty 0 + + Clos 0 + Val 0 + + ValEnv 0 + TyEnv 0 + +arities + Const :: term + + ExVar :: term + Ex :: term + + TyConst :: term + Ty :: term + + Clos :: term + Val :: term + + ValEnv :: term + TyEnv :: term + +consts + c_app :: "[Const, Const] => Const" + + e_const :: "Const => Ex" + e_var :: "ExVar => Ex" + e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _") + e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _") + e_app :: "[Ex, Ex] => Ex" ("_ @ _") + e_const_fst :: "Ex => Const" + + t_const :: "TyConst => Ty" + t_fun :: "[Ty, Ty] => Ty" ("_ -> _") + + v_const :: "Const => Val" + v_clos :: "Clos => Val" + + ve_emp :: "ValEnv" + ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [0,0,0] 1000) + ve_dom :: "ValEnv => ExVar set" + ve_app :: "[ValEnv, ExVar] => Val" + + clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000) + + te_emp :: "TyEnv" + te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [0,0,0] 1000) + te_app :: "[TyEnv, ExVar] => Ty" + te_dom :: "TyEnv => ExVar set" + + eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set" + eval_rel :: "((ValEnv * Ex) * Val) set" + eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [0,0,0] 1000) + + elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" + elab_rel :: "((TyEnv * Ex) * Ty) set" + elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [0,0,0] 1000) + + isof :: "[Const, Ty] => bool" ("_ isof _") + isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") + + hasty_fun :: "(Val * Ty) set => (Val * Ty) set" + hasty_rel :: "(Val * Ty) set" + hasty :: "[Val, Ty] => bool" ("_ hasty _") + hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ ") + +rules + +(* + Expression constructors must be injective, distinct and it must be possible + to do induction over expressions. +*) + +(* All the constructors are injective *) + + e_const_inj "e_const(c1) = e_const(c2) ==> c1 = c2" + e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" + e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" + e_fix_inj + " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \ +\ ev11 = ev21 & ev12 = ev22 & e1 = e2 \ +\ " + e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22" + +(* All constructors are distinct *) + + e_disj_const_var "~e_const(c) = e_var(ev)" + e_disj_const_fn "~e_const(c) = fn ev => e" + e_disj_const_fix "~e_const(c) = fix ev1(ev2) = e" + e_disj_const_app "~e_const(c) = e1 @ e2" + e_disj_var_fn "~e_var(ev1) = fn ev2 => e" + e_disj_var_fix "~e_var(ev) = fix ev1(ev2) = e" + e_disj_var_app "~e_var(ev) = e1 @ e2" + e_disj_fn_fix "~fn ev1 => e1 = fix ev21(ev22) = e2" + e_disj_fn_app "~fn ev1 => e1 = e21 @ e22" + e_disj_fix_app "~fix ev11(ev12) = e1 = e21 @ e22" + +(* Strong elimination, induction on expressions *) + + e_ind + " [| !!ev. P(e_var(ev)); \ +\ !!c. P(e_const(c)); \ +\ !!ev e. P(e) ==> P(fn ev => e); \ +\ !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \ +\ !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \ +\ |] ==> \ +\ P(e) \ +\ " + +(* Types - same scheme as for expressions *) + +(* All constructors are injective *) + + t_const_inj "t_const(c1) = t_const(c2) ==> c1 = c2" + t_fun_inj "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22" + +(* All constructors are distinct, not needed so far ... *) + +(* Strong elimination, induction on types *) + + t_ind + "[| !!p. P(t_const(p)); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun(t1,t2)) |] \ +\ ==> P(t)" + + +(* Values - same scheme again *) + +(* All constructors are injective *) + + v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2" + v_clos_inj + " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \ +\ ev1 = ev2 & e1 = e2 & ve1 = ve2" + +(* All constructors are distinct *) + + v_disj_const_clos "~v_const(c) = v_clos(cl)" + +(* Strong elimination, induction on values, not needed yet ... *) + + +(* + Value environments bind variables to values. Only the following trivial + properties are needed. +*) + + ve_dom_owr "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" + + ve_app_owr1 "ve_app(ve + {ev |-> v},ev)=v" + ve_app_owr2 "~ev1=ev2 ==> ve_app(ve+{ev1 |-> v},ev2)=ve_app(ve,ev2)" + + +(* Type Environments bind variables to types. The following trivial +properties are needed. *) + + te_dom_owr "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" + + te_app_owr1 "te_app(te + {ev |=> t},ev)=t" + te_app_owr2 "~ev1=ev2 ==> te_app(te+{ev1 |=> t},ev2)=te_app(te,ev2)" + + +(* 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. +*) + + eval_fun_def + " eval_fun(s) == \ +\ { pp. \ +\ (? ve c. pp=<,v_const(c)>) | \ +\ (? ve x. pp=<,ve_app(ve,x)> & x:ve_dom(ve)) |\ +\ (? ve e x. pp=< e>,v_clos(<|x,e,ve|>)>)| \ +\ ( ? ve e x f cl. \ +\ pp=<,v_clos(cl)> & \ +\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \ +\ ) | \ +\ ( ? ve e1 e2 c1 c2. \ +\ pp=<,v_const(c_app(c1,c2))> & \ +\ <,v_const(c1)>:s & <,v_const(c2)>:s \ +\ ) | \ +\ ( ? ve vem e1 e2 em xm v v2. \ +\ pp=<,v> & \ +\ <,v_clos(<|xm,em,vem|>)>:s & \ +\ <,v2>:s & \ +\ < v2},em>,v>:s \ +\ ) \ +\ }" + + eval_rel_def "eval_rel == lfp(eval_fun)" + eval_def "ve |- e ---> v == <,v>:eval_rel" + +(* 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. +*) + + elab_fun_def + "elab_fun(s) == \ +\ { pp. \ +\ (? te c t. pp=<,t> & c isof t) | \ +\ (? te x. pp=<,te_app(te,x)> & x:te_dom(te)) | \ +\ (? te x e t1 t2. pp=< e>,t1->t2> & < t1},e>,t2>:s) | \ +\ (? te f x e t1 t2. \ +\ pp=<,t1->t2> & < t1->t2}+{x |=> t1},e>,t2>:s \ +\ ) | \ +\ (? te e1 e2 t1 t2. \ +\ pp=<,t2> & <,t1->t2>:s & <,t1>:s \ +\ ) \ +\ }" + + elab_rel_def "elab_rel == lfp(elab_fun)" + elab_def "te |- e ===> t == <,t>:elab_rel" + +(* The original correspondence relation *) + + isof_env_def + " ve isofenv te == \ +\ ve_dom(ve) = te_dom(te) & \ +\ ( ! x. \ +\ x:ve_dom(ve) --> \ +\ (? c.ve_app(ve,x) = v_const(c) & c isof te_app(te,x)) \ +\ ) \ +\ " + + isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app(c1,c2) isof t2" + +(* The extented correspondence relation *) + + hasty_fun_def + " hasty_fun(r) == \ +\ { p. \ +\ ( ? c t. p = & c isof t) | \ +\ ( ? ev e ve t te. \ +\ p = ),t> & \ +\ te |- fn ev => e ===> t & \ +\ ve_dom(ve) = te_dom(te) & \ +\ (! ev1.ev1:ve_dom(ve) --> : r) \ +\ ) \ +\ } \ +\ " + + hasty_rel_def "hasty_rel == gfp(hasty_fun)" + hasty_def "v hasty t == : hasty_rel" + hasty_env_def + " ve hastyenv te == \ +\ ve_dom(ve) = te_dom(te) & \ +\ (! x. x: ve_dom(ve) --> ve_app(ve,x) hasty te_app(te,x))" + +end + + + + + + + +