--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/MT.ML Tue Nov 09 11:08:13 1993 +0100
@@ -0,0 +1,826 @@
+(* Title: HOL/ex/mt.ML
+ 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).
+*)
+
+open MT;
+
+val prems = goal MT.thy "~a:{b} ==> ~a=b";
+by (cut_facts_tac prems 1);
+by (rtac notI 1);
+by (dtac notE 1);
+by (hyp_subst_tac 1);
+by (rtac singletonI 1);
+by (assume_tac 1);
+val notsingletonI = result();
+
+val prems = goalw MT.thy [Un_def]
+ "[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P";
+by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1;
+by (cut_facts_tac [excluded_middle] 1);be disjE 1;
+by (resolve_tac prems 1);br conjI 1;ba 1;ba 1;
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+val UnSE = result();
+
+(* ############################################################ *)
+(* Inference systems *)
+(* ############################################################ *)
+
+val infsys_mono_tac =
+ (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
+ (rtac CollectI 1) THEN (dtac CollectD 1) THEN
+ REPEAT
+ ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
+ (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
+ );
+
+val prems = goal MT.thy "P(a,b) ==> P(fst(<a,b>),snd(<a,b>))";
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (resolve_tac prems 1);
+val infsys_p1 = result();
+
+val prems = goal MT.thy "P(fst(<a,b>),snd(<a,b>)) ==> P(a,b)";
+by (cut_facts_tac prems 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (assume_tac 1);
+val infsys_p2 = result();
+
+val prems = goal MT.thy
+ "P(a,b,c) ==> P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>))";
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (resolve_tac prems 1);
+val infsys_pp1 = result();
+
+val prems = goal MT.thy
+ "P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>)) ==> P(a,b,c)";
+by (cut_facts_tac prems 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (assume_tac 1);
+val infsys_pp2 = result();
+
+(* ############################################################ *)
+(* Fixpoints *)
+(* ############################################################ *)
+
+(* Least fixpoints *)
+
+val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
+by (rtac subsetD 1);
+by (rtac lfp_lemma2 1);
+by (resolve_tac prems 1);brs prems 1;
+val lfp_intro2 = result();
+
+val prems = goal MT.thy
+ " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
+\ P(x)";
+by (cut_facts_tac prems 1);
+by (resolve_tac prems 1);br subsetD 1;
+by (rtac lfp_lemma3 1);ba 1;ba 1;
+val lfp_elim2 = result();
+
+val prems = goal MT.thy
+ " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
+\ P(x)";
+by (cut_facts_tac prems 1);
+by (etac induct 1);ba 1;
+by (eresolve_tac prems 1);
+val lfp_ind2 = result();
+
+(* Greatest fixpoints *)
+
+(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
+
+val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
+by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
+by (rtac (monoh RS monoD) 1);
+by (rtac (UnE RS subsetI) 1);ba 1;
+by (fast_tac (set_cs addSIs [cih]) 1);
+by (rtac (monoh RS monoD RS subsetD) 1);
+by (rtac Un_upper2 1);
+by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
+val gfp_coind2 = result();
+
+val [gfph,monoh,caseh] = goal MT.thy
+ "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
+by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1;
+val gfp_elim2 =result();
+
+(* ############################################################ *)
+(* Expressions *)
+(* ############################################################ *)
+
+val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
+
+val e_disjs =
+ [ e_disj_const_var,
+ e_disj_const_fn,
+ e_disj_const_fix,
+ e_disj_const_app,
+ e_disj_var_fn,
+ e_disj_var_fix,
+ e_disj_var_app,
+ e_disj_fn_fix,
+ e_disj_fn_app,
+ e_disj_fix_app
+ ];
+
+val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
+val e_disj_se = (e_disj_si RL [notE]);
+
+fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
+
+(* ############################################################ *)
+(* Values *)
+(* ############################################################ *)
+
+val v_disjs = [v_disj_const_clos];
+val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
+val v_disj_se = (v_disj_si RL [notE]);
+
+val v_injs = [v_const_inj, v_clos_inj];
+
+fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
+
+(* ############################################################ *)
+(* Evaluations *)
+(* ############################################################ *)
+
+(* Monotonicity of eval_fun *)
+
+goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
+by infsys_mono_tac;
+val eval_fun_mono = result();
+
+(* Introduction rules *)
+
+goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_const = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app(ve,ev)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_var = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_fn = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ ve |- fix ev2(ev1) = e ---> v_clos(cl)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_fix = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
+\ ve |- e1 @ e2 ---> v_const(c_app(c1,c2))";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_app1 = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \
+\ ve |- e2 ---> v2; \
+\ vem + {xm |-> v2} |- em ---> v \
+\ |] ==> \
+\ ve |- e1 @ e2 ---> v";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
+by (fast_tac HOL_cs 1);
+val eval_app2 = result();
+
+(* Strong elimination, induction on evaluations *)
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e ---> v; \
+\ !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
+\ !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app(ve,ev)>); \
+\ !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
+\ !!ev1 ev2 ve cl e. \
+\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
+\ !!ve c1 c2 e1 e2. \
+\ [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
+\ P(<<ve,e1 @ e2>,v_const(c_app(c1,c2))>); \
+\ !!ve vem xm e1 e2 em v v2. \
+\ [| P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
+\ P(<<ve,e2>,v2>); \
+\ P(<<vem + {xm |-> v2},em>,v>) \
+\ |] ==> \
+\ P(<<ve,e1 @ e2>,v>) \
+\ |] ==> \
+\ P(<<ve,e>,v>)";
+by (resolve_tac (prems RL [lfp_ind2]) 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val eval_ind0 = result();
+
+val prems = goal MT.thy
+ " [| ve |- e ---> v; \
+\ !!ve c. P(ve,e_const(c),v_const(c)); \
+\ !!ev ve. ev:ve_dom(ve) ==> P(ve,e_var(ev),ve_app(ve,ev)); \
+\ !!ev ve e. P(ve,fn ev => e,v_clos(<|ev,e,ve|>)); \
+\ !!ev1 ev2 ve cl e. \
+\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ P(ve,fix ev2(ev1) = e,v_clos(cl)); \
+\ !!ve c1 c2 e1 e2. \
+\ [| P(ve,e1,v_const(c1)); P(ve,e2,v_const(c2)) |] ==> \
+\ P(ve,e1 @ e2,v_const(c_app(c1,c2))); \
+\ !!ve vem evm e1 e2 em v v2. \
+\ [| P(ve,e1,v_clos(<|evm,em,vem|>)); \
+\ P(ve,e2,v2); \
+\ P(vem + {evm |-> v2},em,v) \
+\ |] ==> P(ve,e1 @ e2,v) \
+\ |] ==> P(ve,e,v)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac eval_ind0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val eval_ind = result();
+
+(* ############################################################ *)
+(* Elaborations *)
+(* ############################################################ *)
+
+goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
+by infsys_mono_tac;
+val elab_fun_mono = result();
+
+(* Introduction rules *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "c isof ty ==> te |- e_const(c) ===> ty";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_const = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "x:te_dom(te) ==> te |- e_var(x) ===> te_app(te,x)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_var = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_fn = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
+\ te |- fix f(x) = e ===> ty1->ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_fix = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
+\ te |- e1 @ e2 ===> ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
+by (fast_tac HOL_cs 1);
+val elab_app = result();
+
+(* Strong elimination, induction on elaborations *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
+\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \
+\ !!te x e t1 t2. \
+\ [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
+\ P(<<te,fn x => e>,t1->t2>); \
+\ !!te f x e t1 t2. \
+\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
+\ P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
+\ |] ==> \
+\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
+\ te |- e2 ===> t1; P(<<te,e2>,t1>) \
+\ |] ==> \
+\ P(<<te,e1 @ e2>,t2>) \
+\ |] ==> \
+\ P(<<te,e>,t>)";
+by (resolve_tac (prems RL [lfp_ind2]) 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val elab_ind0 = result();
+
+val prems = goal MT.thy
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(te,e_const(c),t); \
+\ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \
+\ !!te x e t1 t2. \
+\ [| te + {x |=> t1} |- e ===> t2; P(te + {x |=> t1},e,t2) |] ==> \
+\ P(te,fn x => e,t1->t2); \
+\ !!te f x e t1 t2. \
+\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
+\ P(te + {f |=> t1->t2} + {x |=> t1},e,t2) \
+\ |] ==> \
+\ P(te,fix f(x) = e,t1->t2); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; P(te,e1,t1->t2); \
+\ te |- e2 ===> t1; P(te,e2,t1) \
+\ |] ==> \
+\ P(te,e1 @ e2,t2) \
+\ |] ==> \
+\ P(te,e,t)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac elab_ind0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val elab_ind = result();
+
+(* Weak elimination, case analysis on elaborations *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
+\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \
+\ !!te x e t1 t2. \
+\ te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
+\ !!te f x e t1 t2. \
+\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
+\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
+\ P(<<te,e1 @ e2>,t2>) \
+\ |] ==> \
+\ P(<<te,e>,t>)";
+by (resolve_tac (prems RL [lfp_elim2]) 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val elab_elim0 = result();
+
+val prems = goal MT.thy
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(te,e_const(c),t); \
+\ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \
+\ !!te x e t1 t2. \
+\ te + {x |=> t1} |- e ===> t2 ==> P(te,fn x => e,t1->t2); \
+\ !!te f x e t1 t2. \
+\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
+\ P(te,fix f(x) = e,t1->t2); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
+\ P(te,e1 @ e2,t2) \
+\ |] ==> \
+\ P(te,e,t)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac elab_elim0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val elab_elim = result();
+
+(* Elimination rules for each expression *)
+
+fun elab_e_elim_tac p =
+ ( (rtac elab_elim 1) THEN
+ (resolve_tac p 1) THEN
+ (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
+ );
+
+val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
+by (elab_e_elim_tac prems);
+val elab_const_elim_lem = result();
+
+val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
+by (cut_facts_tac prems 1);
+by (dtac elab_const_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_const_elim = result();
+
+val prems = goal MT.thy
+ "te |- e ===> t ==> (e = e_var(x) --> t=te_app(te,x) & x:te_dom(te))";
+by (elab_e_elim_tac prems);
+val elab_var_elim_lem = result();
+
+val prems = goal MT.thy
+ "te |- e_var(ev) ===> t ==> t=te_app(te,ev) & ev : te_dom(te)";
+by (cut_facts_tac prems 1);
+by (dtac elab_var_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_var_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t ==> \
+\ ( e = fn x1 => e1 --> \
+\ (? t1 t2.t=t_fun(t1,t2) & te + {x1 |=> t1} |- e1 ===> t2) \
+\ )";
+by (elab_e_elim_tac prems);
+val elab_fn_elim_lem = result();
+
+val prems = goal MT.thy
+ " te |- fn x1 => e1 ===> t ==> \
+\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
+by (cut_facts_tac prems 1);
+by (dtac elab_fn_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_fn_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t ==> \
+\ (e = fix f(x) = e1 --> \
+\ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))";
+by (elab_e_elim_tac prems);
+val elab_fix_elim_lem = result();
+
+val prems = goal MT.thy
+ " te |- fix ev1(ev2) = e1 ===> t ==> \
+\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
+by (cut_facts_tac prems 1);
+by (dtac elab_fix_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_fix_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t2 ==> \
+\ (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))";
+by (elab_e_elim_tac prems);
+val elab_app_elim_lem = result();
+
+val prems = goal MT.thy
+ "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_app_elim = result();
+
+(* ############################################################ *)
+(* The extended correspondence relation *)
+(* ############################################################ *)
+
+(* Monotonicity of hasty_fun *)
+
+goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
+by infsys_mono_tac;
+val mono_hasty_fun = result();
+
+(*
+ Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
+ enjoys two strong indtroduction (co-induction) rules and an elimination rule.
+*)
+
+(* First strong indtroduction (co-induction) rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
+by (cut_facts_tac prems 1);
+by (rtac gfp_coind2 1);
+by (rewtac MT.hasty_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+by (rtac mono_hasty_fun 1);
+val hasty_rel_const_coind = result();
+
+(* Second strong introduction (co-induction) rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def]
+ " [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ ! ev1. \
+\ ev1:ve_dom(ve) --> \
+\ <ve_app(ve,ev1),te_app(te,ev1)> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
+\ |] ==> \
+\ <v_clos(<|ev,e,ve|>),t> : hasty_rel";
+by (cut_facts_tac prems 1);
+by (rtac gfp_coind2 1);
+by (rewtac hasty_fun_def);
+by (rtac CollectI 1);br disjI2 1;
+by (fast_tac HOL_cs 1);
+by (rtac mono_hasty_fun 1);
+val hasty_rel_clos_coind = result();
+
+(* Elimination rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def]
+ " [| !! c t.c isof t ==> P(<v_const(c),t>); \
+\ !! te ev e t ve. \
+\ [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \
+\ |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
+\ <v,t> : hasty_rel \
+\ |] ==> P(<v,t>)";
+by (cut_facts_tac prems 1);
+by (etac gfp_elim2 1);
+by (rtac mono_hasty_fun 1);
+by (rewtac hasty_fun_def);
+by (dtac CollectD 1);
+by (fold_goals_tac [hasty_fun_def]);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val hasty_rel_elim0 = result();
+
+val prems = goal MT.thy
+ " [| <v,t> : hasty_rel; \
+\ !! c t.c isof t ==> P(v_const(c),t); \
+\ !! te ev e t ve. \
+\ [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \
+\ |] ==> P(v_clos(<|ev,e,ve|>),t) \
+\ |] ==> P(v,t)";
+by (res_inst_tac [("P","P")] infsys_p2 1);
+by (rtac hasty_rel_elim0 1);
+by (ALLGOALS (rtac infsys_p1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
+val hasty_rel_elim = result();
+
+(* Introduction rules for hasty *)
+
+val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
+by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
+val hasty_const = result();
+
+val prems = goalw MT.thy [hasty_def,hasty_env_def]
+ "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_clos_coind 1);
+by (ALLGOALS (fast_tac set_cs));
+val hasty_clos = result();
+
+(* Elimination on constants for hasty *)
+
+val prems = goalw MT.thy [hasty_def]
+ "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_elim 1);
+by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+val hasty_elim_const_lem = result();
+
+val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
+by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
+by (fast_tac HOL_cs 1);
+val hasty_elim_const = result();
+
+(* Elimination on closures for hasty *)
+
+val prems = goalw MT.thy [hasty_env_def,hasty_def]
+ " v hasty t ==> \
+\ ! x e ve. \
+\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_elim 1);
+by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+val hasty_elim_clos_lem = result();
+
+val prems = goal MT.thy
+ "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
+by (fast_tac HOL_cs 1);
+val hasty_elim_clos = result();
+
+(* ############################################################ *)
+(* The pointwise extension of hasty to environments *)
+(* ############################################################ *)
+
+val prems = goal MT.thy
+ "[| ve hastyenv te; v hasty t |] ==> \
+\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
+by (cut_facts_tac prems 1);
+by (SELECT_GOAL (rewtac hasty_env_def) 1);
+by (safe_tac HOL_cs);
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (rtac (te_dom_owr RS ssubst) 1);
+by (etac subst 1);br refl 1;
+
+by (dtac (ve_dom_owr RS subst) 1);back();back();back();
+by (etac UnSE 1);be conjE 1;
+by (dtac notsingletonI 1);bd not_sym 1;
+by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
+by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
+by (fast_tac HOL_cs 1);
+by (dtac singletonD 1);by (hyp_subst_tac 1);
+
+by (rtac (ve_app_owr1 RS ssubst) 1);
+by (rtac (te_app_owr1 RS ssubst) 1);
+by (assume_tac 1);
+val hasty_env1 = result();
+
+(* ############################################################ *)
+(* The Consistency theorem *)
+(* ############################################################ *)
+
+val prems = goal MT.thy
+ "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_const_elim 1);
+by (etac hasty_const 1);
+val consistency_const = result();
+
+val prems = goalw MT.thy [hasty_env_def]
+ " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
+\ ve_app(ve,ev) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_var_elim 1);
+by (fast_tac HOL_cs 1);
+val consistency_var = result();
+
+val prems = goal MT.thy
+ " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+\ v_clos(<| ev, e, ve |>) hasty t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_clos 1);
+by (fast_tac prop_cs 1);
+val consistency_fn = result();
+
+val prems = goalw MT.thy [hasty_env_def,hasty_def]
+ " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
+\ ve hastyenv te ; \
+\ te |- fix ev2 ev1 = e ===> t \
+\ |] ==> \
+\ v_clos(cl) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_fix_elim 1);
+by (safe_tac HOL_cs);
+by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN
+ (rtac hasty_rel_clos_coind 1));
+by (etac elab_fn 1);
+
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (rtac (te_dom_owr RS ssubst) 1);
+by ((etac subst 1) THEN (rtac refl 1));
+
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (safe_tac HOL_cs);
+by (dtac (Un_commute RS subst) 1);
+by (etac UnSE 1);
+
+by (safe_tac HOL_cs);
+by (dtac notsingletonI 1);bd not_sym 1;
+by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
+by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
+by (fast_tac set_cs 1);
+
+by (etac singletonE 1);
+by (hyp_subst_tac 1);
+by (rtac (ve_app_owr1 RS ssubst) 1);
+by (rtac (te_app_owr1 RS ssubst) 1);
+by (etac subst 1);
+by (fast_tac set_cs 1);
+val consistency_fix = result();
+
+val prems = goal MT.thy
+ " [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \
+\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
+\ ve hastyenv te ; te |- e1 @ e2 ===> t \
+\ |] ==> \
+\ v_const(c_app(c1,c2)) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim 1);
+by (safe_tac HOL_cs);
+by (rtac hasty_const 1);
+by (rtac isof_app 1);
+by (rtac hasty_elim_const 1);
+by (fast_tac HOL_cs 1);
+by (rtac hasty_elim_const 1);
+by (fast_tac HOL_cs 1);
+val consistency_app1 = result();
+
+val prems = goal MT.thy
+ " [| ! t te. \
+\ ve hastyenv te --> \
+\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
+\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
+\ ! t te. \
+\ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \
+\ ve hastyenv te ; \
+\ te |- e1 @ e2 ===> t \
+\ |] ==> \
+\ v hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim 1);
+by (safe_tac HOL_cs);
+by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
+by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
+by (dtac hasty_elim_clos 1);
+by (safe_tac HOL_cs);
+by (dtac elab_fn_elim 1);
+by (safe_tac HOL_cs);
+by (dtac t_fun_inj 1);
+by (safe_tac prop_cs);
+by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
+val consistency_app2 = result();
+
+val prems = goal MT.thy
+ "ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
+
+(* Proof by induction on the structure of evaluations *)
+
+by (resolve_tac (prems RL [eval_ind]) 1);
+by (safe_tac HOL_cs);
+
+by (rtac consistency_const 1);ba 1;ba 1;
+by (rtac consistency_var 1);ba 1;ba 1;ba 1;
+by (rtac consistency_fn 1);ba 1;ba 1;
+by (rtac consistency_fix 1);ba 1;ba 1;ba 1;
+by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1;
+by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1;
+val consistency = result();
+
+(* ############################################################ *)
+(* The Basic Consistency theorem *)
+(* ############################################################ *)
+
+val prems = goalw MT.thy [isof_env_def,hasty_env_def]
+ "ve isofenv te ==> ve hastyenv te";
+by (cut_facts_tac prems 1);
+by (safe_tac HOL_cs);
+by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1;
+by (dtac hasty_const 1);
+by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1));
+val basic_consistency_lem = result();
+
+val prems = goal MT.thy
+ "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_elim_const 1);
+by (dtac consistency 1);
+by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
+val basic_consistency = result();
+
+
--- /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=<<ve,e_const(c)>,v_const(c)>) | \
+\ (? ve x. pp=<<ve,e_var(x)>,ve_app(ve,x)> & x:ve_dom(ve)) |\
+\ (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
+\ ( ? ve e x f cl. \
+\ pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
+\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \
+\ ) | \
+\ ( ? ve e1 e2 c1 c2. \
+\ pp=<<ve,e1 @ e2>,v_const(c_app(c1,c2))> & \
+\ <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
+\ ) | \
+\ ( ? ve vem e1 e2 em xm v v2. \
+\ pp=<<ve,e1 @ e2>,v> & \
+\ <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
+\ <<ve,e2>,v2>:s & \
+\ <<vem+{xm |-> v2},em>,v>:s \
+\ ) \
+\ }"
+
+ eval_rel_def "eval_rel == lfp(eval_fun)"
+ eval_def "ve |- e ---> v == <<ve,e>,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=<<te,e_const(c)>,t> & c isof t) | \
+\ (? te x. pp=<<te,e_var(x)>,te_app(te,x)> & x:te_dom(te)) | \
+\ (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
+\ (? te f x e t1 t2. \
+\ pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
+\ ) | \
+\ (? te e1 e2 t1 t2. \
+\ pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
+\ ) \
+\ }"
+
+ elab_rel_def "elab_rel == lfp(elab_fun)"
+ elab_def "te |- e ===> t == <<te,e>,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 = <v_const(c),t> & c isof t) | \
+\ ( ? ev e ve t te. \
+\ p = <v_clos(<|ev,e,ve|>),t> & \
+\ te |- fn ev => e ===> t & \
+\ ve_dom(ve) = te_dom(te) & \
+\ (! ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : r) \
+\ ) \
+\ } \
+\ "
+
+ hasty_rel_def "hasty_rel == gfp(hasty_fun)"
+ hasty_def "v hasty t == <v,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
+
+
+
+
+
+
+
+
--- a/ex/ROOT.ML Wed Nov 03 19:02:17 1993 +0100
+++ b/ex/ROOT.ML Tue Nov 09 11:08:13 1993 +0100
@@ -20,4 +20,5 @@
time_use_thy "ex/pl";
time_use_thy "ex/term";
time_use_thy "ex/simult";
+time_use_thy "ex/mt";
maketest "END: Root file for HOL examples";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/mt.ML Tue Nov 09 11:08:13 1993 +0100
@@ -0,0 +1,826 @@
+(* Title: HOL/ex/mt.ML
+ 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).
+*)
+
+open MT;
+
+val prems = goal MT.thy "~a:{b} ==> ~a=b";
+by (cut_facts_tac prems 1);
+by (rtac notI 1);
+by (dtac notE 1);
+by (hyp_subst_tac 1);
+by (rtac singletonI 1);
+by (assume_tac 1);
+val notsingletonI = result();
+
+val prems = goalw MT.thy [Un_def]
+ "[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P";
+by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1;
+by (cut_facts_tac [excluded_middle] 1);be disjE 1;
+by (resolve_tac prems 1);br conjI 1;ba 1;ba 1;
+by (eresolve_tac prems 1);
+by (eresolve_tac prems 1);
+val UnSE = result();
+
+(* ############################################################ *)
+(* Inference systems *)
+(* ############################################################ *)
+
+val infsys_mono_tac =
+ (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
+ (rtac CollectI 1) THEN (dtac CollectD 1) THEN
+ REPEAT
+ ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
+ (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
+ );
+
+val prems = goal MT.thy "P(a,b) ==> P(fst(<a,b>),snd(<a,b>))";
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (resolve_tac prems 1);
+val infsys_p1 = result();
+
+val prems = goal MT.thy "P(fst(<a,b>),snd(<a,b>)) ==> P(a,b)";
+by (cut_facts_tac prems 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (assume_tac 1);
+val infsys_p2 = result();
+
+val prems = goal MT.thy
+ "P(a,b,c) ==> P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>))";
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (fst_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (rtac (snd_conv RS ssubst) 1);
+by (resolve_tac prems 1);
+val infsys_pp1 = result();
+
+val prems = goal MT.thy
+ "P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>)) ==> P(a,b,c)";
+by (cut_facts_tac prems 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (fst_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (dtac (snd_conv RS subst) 1);
+by (assume_tac 1);
+val infsys_pp2 = result();
+
+(* ############################################################ *)
+(* Fixpoints *)
+(* ############################################################ *)
+
+(* Least fixpoints *)
+
+val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
+by (rtac subsetD 1);
+by (rtac lfp_lemma2 1);
+by (resolve_tac prems 1);brs prems 1;
+val lfp_intro2 = result();
+
+val prems = goal MT.thy
+ " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
+\ P(x)";
+by (cut_facts_tac prems 1);
+by (resolve_tac prems 1);br subsetD 1;
+by (rtac lfp_lemma3 1);ba 1;ba 1;
+val lfp_elim2 = result();
+
+val prems = goal MT.thy
+ " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
+\ P(x)";
+by (cut_facts_tac prems 1);
+by (etac induct 1);ba 1;
+by (eresolve_tac prems 1);
+val lfp_ind2 = result();
+
+(* Greatest fixpoints *)
+
+(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
+
+val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
+by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
+by (rtac (monoh RS monoD) 1);
+by (rtac (UnE RS subsetI) 1);ba 1;
+by (fast_tac (set_cs addSIs [cih]) 1);
+by (rtac (monoh RS monoD RS subsetD) 1);
+by (rtac Un_upper2 1);
+by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
+val gfp_coind2 = result();
+
+val [gfph,monoh,caseh] = goal MT.thy
+ "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
+by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1;
+val gfp_elim2 =result();
+
+(* ############################################################ *)
+(* Expressions *)
+(* ############################################################ *)
+
+val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
+
+val e_disjs =
+ [ e_disj_const_var,
+ e_disj_const_fn,
+ e_disj_const_fix,
+ e_disj_const_app,
+ e_disj_var_fn,
+ e_disj_var_fix,
+ e_disj_var_app,
+ e_disj_fn_fix,
+ e_disj_fn_app,
+ e_disj_fix_app
+ ];
+
+val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
+val e_disj_se = (e_disj_si RL [notE]);
+
+fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
+
+(* ############################################################ *)
+(* Values *)
+(* ############################################################ *)
+
+val v_disjs = [v_disj_const_clos];
+val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
+val v_disj_se = (v_disj_si RL [notE]);
+
+val v_injs = [v_const_inj, v_clos_inj];
+
+fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
+
+(* ############################################################ *)
+(* Evaluations *)
+(* ############################################################ *)
+
+(* Monotonicity of eval_fun *)
+
+goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
+by infsys_mono_tac;
+val eval_fun_mono = result();
+
+(* Introduction rules *)
+
+goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_const = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app(ve,ev)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_var = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_fn = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ ve |- fix ev2(ev1) = e ---> v_clos(cl)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_fix = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
+\ ve |- e1 @ e2 ---> v_const(c_app(c1,c2))";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val eval_app1 = result();
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \
+\ ve |- e2 ---> v2; \
+\ vem + {xm |-> v2} |- em ---> v \
+\ |] ==> \
+\ ve |- e1 @ e2 ---> v";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
+by (fast_tac HOL_cs 1);
+val eval_app2 = result();
+
+(* Strong elimination, induction on evaluations *)
+
+val prems = goalw MT.thy [eval_def, eval_rel_def]
+ " [| ve |- e ---> v; \
+\ !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
+\ !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app(ve,ev)>); \
+\ !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
+\ !!ev1 ev2 ve cl e. \
+\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
+\ !!ve c1 c2 e1 e2. \
+\ [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
+\ P(<<ve,e1 @ e2>,v_const(c_app(c1,c2))>); \
+\ !!ve vem xm e1 e2 em v v2. \
+\ [| P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
+\ P(<<ve,e2>,v2>); \
+\ P(<<vem + {xm |-> v2},em>,v>) \
+\ |] ==> \
+\ P(<<ve,e1 @ e2>,v>) \
+\ |] ==> \
+\ P(<<ve,e>,v>)";
+by (resolve_tac (prems RL [lfp_ind2]) 1);
+by (rtac eval_fun_mono 1);
+by (rewtac eval_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val eval_ind0 = result();
+
+val prems = goal MT.thy
+ " [| ve |- e ---> v; \
+\ !!ve c. P(ve,e_const(c),v_const(c)); \
+\ !!ev ve. ev:ve_dom(ve) ==> P(ve,e_var(ev),ve_app(ve,ev)); \
+\ !!ev ve e. P(ve,fn ev => e,v_clos(<|ev,e,ve|>)); \
+\ !!ev1 ev2 ve cl e. \
+\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
+\ P(ve,fix ev2(ev1) = e,v_clos(cl)); \
+\ !!ve c1 c2 e1 e2. \
+\ [| P(ve,e1,v_const(c1)); P(ve,e2,v_const(c2)) |] ==> \
+\ P(ve,e1 @ e2,v_const(c_app(c1,c2))); \
+\ !!ve vem evm e1 e2 em v v2. \
+\ [| P(ve,e1,v_clos(<|evm,em,vem|>)); \
+\ P(ve,e2,v2); \
+\ P(vem + {evm |-> v2},em,v) \
+\ |] ==> P(ve,e1 @ e2,v) \
+\ |] ==> P(ve,e,v)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac eval_ind0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val eval_ind = result();
+
+(* ############################################################ *)
+(* Elaborations *)
+(* ############################################################ *)
+
+goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
+by infsys_mono_tac;
+val elab_fun_mono = result();
+
+(* Introduction rules *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "c isof ty ==> te |- e_const(c) ===> ty";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_const = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "x:te_dom(te) ==> te |- e_var(x) ===> te_app(te,x)";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_var = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_fn = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
+\ te |- fix f(x) = e ===> ty1->ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
+by (fast_tac HOL_cs 1);
+val elab_fix = result();
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
+\ te |- e1 @ e2 ===> ty2";
+by (cut_facts_tac prems 1);
+by (rtac lfp_intro2 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
+by (fast_tac HOL_cs 1);
+val elab_app = result();
+
+(* Strong elimination, induction on elaborations *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
+\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \
+\ !!te x e t1 t2. \
+\ [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
+\ P(<<te,fn x => e>,t1->t2>); \
+\ !!te f x e t1 t2. \
+\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
+\ P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
+\ |] ==> \
+\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
+\ te |- e2 ===> t1; P(<<te,e2>,t1>) \
+\ |] ==> \
+\ P(<<te,e1 @ e2>,t2>) \
+\ |] ==> \
+\ P(<<te,e>,t>)";
+by (resolve_tac (prems RL [lfp_ind2]) 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val elab_ind0 = result();
+
+val prems = goal MT.thy
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(te,e_const(c),t); \
+\ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \
+\ !!te x e t1 t2. \
+\ [| te + {x |=> t1} |- e ===> t2; P(te + {x |=> t1},e,t2) |] ==> \
+\ P(te,fn x => e,t1->t2); \
+\ !!te f x e t1 t2. \
+\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
+\ P(te + {f |=> t1->t2} + {x |=> t1},e,t2) \
+\ |] ==> \
+\ P(te,fix f(x) = e,t1->t2); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; P(te,e1,t1->t2); \
+\ te |- e2 ===> t1; P(te,e2,t1) \
+\ |] ==> \
+\ P(te,e1 @ e2,t2) \
+\ |] ==> \
+\ P(te,e,t)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac elab_ind0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val elab_ind = result();
+
+(* Weak elimination, case analysis on elaborations *)
+
+val prems = goalw MT.thy [elab_def, elab_rel_def]
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
+\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app(te,x)>); \
+\ !!te x e t1 t2. \
+\ te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
+\ !!te f x e t1 t2. \
+\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
+\ P(<<te,fix f(x) = e>,t1->t2>); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
+\ P(<<te,e1 @ e2>,t2>) \
+\ |] ==> \
+\ P(<<te,e>,t>)";
+by (resolve_tac (prems RL [lfp_elim2]) 1);
+by (rtac elab_fun_mono 1);
+by (rewtac elab_fun_def);
+by (dtac CollectD 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val elab_elim0 = result();
+
+val prems = goal MT.thy
+ " [| te |- e ===> t; \
+\ !!te c t. c isof t ==> P(te,e_const(c),t); \
+\ !!te x. x:te_dom(te) ==> P(te,e_var(x),te_app(te,x)); \
+\ !!te x e t1 t2. \
+\ te + {x |=> t1} |- e ===> t2 ==> P(te,fn x => e,t1->t2); \
+\ !!te f x e t1 t2. \
+\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
+\ P(te,fix f(x) = e,t1->t2); \
+\ !!te e1 e2 t1 t2. \
+\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
+\ P(te,e1 @ e2,t2) \
+\ |] ==> \
+\ P(te,e,t)";
+by (res_inst_tac [("P","P")] infsys_pp2 1);
+by (rtac elab_elim0 1);
+by (ALLGOALS (rtac infsys_pp1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
+val elab_elim = result();
+
+(* Elimination rules for each expression *)
+
+fun elab_e_elim_tac p =
+ ( (rtac elab_elim 1) THEN
+ (resolve_tac p 1) THEN
+ (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
+ );
+
+val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
+by (elab_e_elim_tac prems);
+val elab_const_elim_lem = result();
+
+val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
+by (cut_facts_tac prems 1);
+by (dtac elab_const_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_const_elim = result();
+
+val prems = goal MT.thy
+ "te |- e ===> t ==> (e = e_var(x) --> t=te_app(te,x) & x:te_dom(te))";
+by (elab_e_elim_tac prems);
+val elab_var_elim_lem = result();
+
+val prems = goal MT.thy
+ "te |- e_var(ev) ===> t ==> t=te_app(te,ev) & ev : te_dom(te)";
+by (cut_facts_tac prems 1);
+by (dtac elab_var_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_var_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t ==> \
+\ ( e = fn x1 => e1 --> \
+\ (? t1 t2.t=t_fun(t1,t2) & te + {x1 |=> t1} |- e1 ===> t2) \
+\ )";
+by (elab_e_elim_tac prems);
+val elab_fn_elim_lem = result();
+
+val prems = goal MT.thy
+ " te |- fn x1 => e1 ===> t ==> \
+\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
+by (cut_facts_tac prems 1);
+by (dtac elab_fn_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_fn_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t ==> \
+\ (e = fix f(x) = e1 --> \
+\ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))";
+by (elab_e_elim_tac prems);
+val elab_fix_elim_lem = result();
+
+val prems = goal MT.thy
+ " te |- fix ev1(ev2) = e1 ===> t ==> \
+\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
+by (cut_facts_tac prems 1);
+by (dtac elab_fix_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_fix_elim = result();
+
+val prems = goal MT.thy
+ " te |- e ===> t2 ==> \
+\ (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))";
+by (elab_e_elim_tac prems);
+val elab_app_elim_lem = result();
+
+val prems = goal MT.thy
+ "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim_lem 1);
+by (fast_tac prop_cs 1);
+val elab_app_elim = result();
+
+(* ############################################################ *)
+(* The extended correspondence relation *)
+(* ############################################################ *)
+
+(* Monotonicity of hasty_fun *)
+
+goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
+by infsys_mono_tac;
+val mono_hasty_fun = result();
+
+(*
+ Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
+ enjoys two strong indtroduction (co-induction) rules and an elimination rule.
+*)
+
+(* First strong indtroduction (co-induction) rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
+by (cut_facts_tac prems 1);
+by (rtac gfp_coind2 1);
+by (rewtac MT.hasty_fun_def);
+by (rtac CollectI 1);br disjI1 1;
+by (fast_tac HOL_cs 1);
+by (rtac mono_hasty_fun 1);
+val hasty_rel_const_coind = result();
+
+(* Second strong introduction (co-induction) rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def]
+ " [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ ! ev1. \
+\ ev1:ve_dom(ve) --> \
+\ <ve_app(ve,ev1),te_app(te,ev1)> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
+\ |] ==> \
+\ <v_clos(<|ev,e,ve|>),t> : hasty_rel";
+by (cut_facts_tac prems 1);
+by (rtac gfp_coind2 1);
+by (rewtac hasty_fun_def);
+by (rtac CollectI 1);br disjI2 1;
+by (fast_tac HOL_cs 1);
+by (rtac mono_hasty_fun 1);
+val hasty_rel_clos_coind = result();
+
+(* Elimination rule for hasty_rel *)
+
+val prems = goalw MT.thy [hasty_rel_def]
+ " [| !! c t.c isof t ==> P(<v_const(c),t>); \
+\ !! te ev e t ve. \
+\ [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \
+\ |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
+\ <v,t> : hasty_rel \
+\ |] ==> P(<v,t>)";
+by (cut_facts_tac prems 1);
+by (etac gfp_elim2 1);
+by (rtac mono_hasty_fun 1);
+by (rewtac hasty_fun_def);
+by (dtac CollectD 1);
+by (fold_goals_tac [hasty_fun_def]);
+by (safe_tac HOL_cs);
+by (ALLGOALS (resolve_tac prems));
+by (ALLGOALS (fast_tac set_cs));
+val hasty_rel_elim0 = result();
+
+val prems = goal MT.thy
+ " [| <v,t> : hasty_rel; \
+\ !! c t.c isof t ==> P(v_const(c),t); \
+\ !! te ev e t ve. \
+\ [| te |- fn ev => e ===> t; \
+\ ve_dom(ve) = te_dom(te); \
+\ !ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : hasty_rel \
+\ |] ==> P(v_clos(<|ev,e,ve|>),t) \
+\ |] ==> P(v,t)";
+by (res_inst_tac [("P","P")] infsys_p2 1);
+by (rtac hasty_rel_elim0 1);
+by (ALLGOALS (rtac infsys_p1));
+by (ALLGOALS (resolve_tac prems));
+by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
+val hasty_rel_elim = result();
+
+(* Introduction rules for hasty *)
+
+val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
+by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
+val hasty_const = result();
+
+val prems = goalw MT.thy [hasty_def,hasty_env_def]
+ "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_clos_coind 1);
+by (ALLGOALS (fast_tac set_cs));
+val hasty_clos = result();
+
+(* Elimination on constants for hasty *)
+
+val prems = goalw MT.thy [hasty_def]
+ "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_elim 1);
+by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+val hasty_elim_const_lem = result();
+
+val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
+by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
+by (fast_tac HOL_cs 1);
+val hasty_elim_const = result();
+
+(* Elimination on closures for hasty *)
+
+val prems = goalw MT.thy [hasty_env_def,hasty_def]
+ " v hasty t ==> \
+\ ! x e ve. \
+\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
+by (cut_facts_tac prems 1);
+by (rtac hasty_rel_elim 1);
+by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+val hasty_elim_clos_lem = result();
+
+val prems = goal MT.thy
+ "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
+by (fast_tac HOL_cs 1);
+val hasty_elim_clos = result();
+
+(* ############################################################ *)
+(* The pointwise extension of hasty to environments *)
+(* ############################################################ *)
+
+val prems = goal MT.thy
+ "[| ve hastyenv te; v hasty t |] ==> \
+\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
+by (cut_facts_tac prems 1);
+by (SELECT_GOAL (rewtac hasty_env_def) 1);
+by (safe_tac HOL_cs);
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (rtac (te_dom_owr RS ssubst) 1);
+by (etac subst 1);br refl 1;
+
+by (dtac (ve_dom_owr RS subst) 1);back();back();back();
+by (etac UnSE 1);be conjE 1;
+by (dtac notsingletonI 1);bd not_sym 1;
+by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
+by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
+by (fast_tac HOL_cs 1);
+by (dtac singletonD 1);by (hyp_subst_tac 1);
+
+by (rtac (ve_app_owr1 RS ssubst) 1);
+by (rtac (te_app_owr1 RS ssubst) 1);
+by (assume_tac 1);
+val hasty_env1 = result();
+
+(* ############################################################ *)
+(* The Consistency theorem *)
+(* ############################################################ *)
+
+val prems = goal MT.thy
+ "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_const_elim 1);
+by (etac hasty_const 1);
+val consistency_const = result();
+
+val prems = goalw MT.thy [hasty_env_def]
+ " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
+\ ve_app(ve,ev) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_var_elim 1);
+by (fast_tac HOL_cs 1);
+val consistency_var = result();
+
+val prems = goal MT.thy
+ " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+\ v_clos(<| ev, e, ve |>) hasty t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_clos 1);
+by (fast_tac prop_cs 1);
+val consistency_fn = result();
+
+val prems = goalw MT.thy [hasty_env_def,hasty_def]
+ " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
+\ ve hastyenv te ; \
+\ te |- fix ev2 ev1 = e ===> t \
+\ |] ==> \
+\ v_clos(cl) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_fix_elim 1);
+by (safe_tac HOL_cs);
+by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN
+ (rtac hasty_rel_clos_coind 1));
+by (etac elab_fn 1);
+
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (rtac (te_dom_owr RS ssubst) 1);
+by ((etac subst 1) THEN (rtac refl 1));
+
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (safe_tac HOL_cs);
+by (dtac (Un_commute RS subst) 1);
+by (etac UnSE 1);
+
+by (safe_tac HOL_cs);
+by (dtac notsingletonI 1);bd not_sym 1;
+by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
+by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
+by (fast_tac set_cs 1);
+
+by (etac singletonE 1);
+by (hyp_subst_tac 1);
+by (rtac (ve_app_owr1 RS ssubst) 1);
+by (rtac (te_app_owr1 RS ssubst) 1);
+by (etac subst 1);
+by (fast_tac set_cs 1);
+val consistency_fix = result();
+
+val prems = goal MT.thy
+ " [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \
+\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
+\ ve hastyenv te ; te |- e1 @ e2 ===> t \
+\ |] ==> \
+\ v_const(c_app(c1,c2)) hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim 1);
+by (safe_tac HOL_cs);
+by (rtac hasty_const 1);
+by (rtac isof_app 1);
+by (rtac hasty_elim_const 1);
+by (fast_tac HOL_cs 1);
+by (rtac hasty_elim_const 1);
+by (fast_tac HOL_cs 1);
+val consistency_app1 = result();
+
+val prems = goal MT.thy
+ " [| ! t te. \
+\ ve hastyenv te --> \
+\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
+\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
+\ ! t te. \
+\ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \
+\ ve hastyenv te ; \
+\ te |- e1 @ e2 ===> t \
+\ |] ==> \
+\ v hasty t";
+by (cut_facts_tac prems 1);
+by (dtac elab_app_elim 1);
+by (safe_tac HOL_cs);
+by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
+by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
+by (dtac hasty_elim_clos 1);
+by (safe_tac HOL_cs);
+by (dtac elab_fn_elim 1);
+by (safe_tac HOL_cs);
+by (dtac t_fun_inj 1);
+by (safe_tac prop_cs);
+by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
+val consistency_app2 = result();
+
+val prems = goal MT.thy
+ "ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
+
+(* Proof by induction on the structure of evaluations *)
+
+by (resolve_tac (prems RL [eval_ind]) 1);
+by (safe_tac HOL_cs);
+
+by (rtac consistency_const 1);ba 1;ba 1;
+by (rtac consistency_var 1);ba 1;ba 1;ba 1;
+by (rtac consistency_fn 1);ba 1;ba 1;
+by (rtac consistency_fix 1);ba 1;ba 1;ba 1;
+by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1;
+by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1;
+val consistency = result();
+
+(* ############################################################ *)
+(* The Basic Consistency theorem *)
+(* ############################################################ *)
+
+val prems = goalw MT.thy [isof_env_def,hasty_env_def]
+ "ve isofenv te ==> ve hastyenv te";
+by (cut_facts_tac prems 1);
+by (safe_tac HOL_cs);
+by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1;
+by (dtac hasty_const 1);
+by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1));
+val basic_consistency_lem = result();
+
+val prems = goal MT.thy
+ "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
+by (cut_facts_tac prems 1);
+by (rtac hasty_elim_const 1);
+by (dtac consistency 1);
+by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
+val basic_consistency = result();
+
+
--- /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=<<ve,e_const(c)>,v_const(c)>) | \
+\ (? ve x. pp=<<ve,e_var(x)>,ve_app(ve,x)> & x:ve_dom(ve)) |\
+\ (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
+\ ( ? ve e x f cl. \
+\ pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
+\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \
+\ ) | \
+\ ( ? ve e1 e2 c1 c2. \
+\ pp=<<ve,e1 @ e2>,v_const(c_app(c1,c2))> & \
+\ <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
+\ ) | \
+\ ( ? ve vem e1 e2 em xm v v2. \
+\ pp=<<ve,e1 @ e2>,v> & \
+\ <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
+\ <<ve,e2>,v2>:s & \
+\ <<vem+{xm |-> v2},em>,v>:s \
+\ ) \
+\ }"
+
+ eval_rel_def "eval_rel == lfp(eval_fun)"
+ eval_def "ve |- e ---> v == <<ve,e>,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=<<te,e_const(c)>,t> & c isof t) | \
+\ (? te x. pp=<<te,e_var(x)>,te_app(te,x)> & x:te_dom(te)) | \
+\ (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
+\ (? te f x e t1 t2. \
+\ pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
+\ ) | \
+\ (? te e1 e2 t1 t2. \
+\ pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
+\ ) \
+\ }"
+
+ elab_rel_def "elab_rel == lfp(elab_fun)"
+ elab_def "te |- e ===> t == <<te,e>,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 = <v_const(c),t> & c isof t) | \
+\ ( ? ev e ve t te. \
+\ p = <v_clos(<|ev,e,ve|>),t> & \
+\ te |- fn ev => e ===> t & \
+\ ve_dom(ve) = te_dom(te) & \
+\ (! ev1.ev1:ve_dom(ve) --> <ve_app(ve,ev1),te_app(te,ev1)> : r) \
+\ ) \
+\ } \
+\ "
+
+ hasty_rel_def "hasty_rel == gfp(hasty_fun)"
+ hasty_def "v hasty t == <v,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
+
+
+
+
+
+
+
+