clasohm@1465: (*  Title:      HOL/ex/MT.ML
clasohm@969:     ID:         $Id$
clasohm@1465:     Author:     Jacob Frost, Cambridge University Computer Laboratory
clasohm@969:     Copyright   1993  University of Cambridge
clasohm@969: 
clasohm@969: Based upon the article
clasohm@969:     Robin Milner and Mads Tofte,
clasohm@969:     Co-induction in Relational Semantics,
clasohm@969:     Theoretical Computer Science 87 (1991), pages 209-220.
clasohm@969: 
clasohm@969: Written up as
clasohm@969:     Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
clasohm@969:     Report 308, Computer Lab, University of Cambridge (1993).
lcp@1047: 
lcp@1047: NEEDS TO USE INDUCTIVE DEFS PACKAGE
clasohm@969: *)
clasohm@969: 
clasohm@969: open MT;
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Inference systems                                            *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
paulson@2935: val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
clasohm@969: 
clasohm@972: val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
wenzelm@4089: by (simp_tac (simpset() addsimps prems) 1);
clasohm@969: qed "infsys_p1";
clasohm@969: 
lcp@1047: val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
clasohm@1266: by (Asm_full_simp_tac 1);
clasohm@969: qed "infsys_p2";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
lcp@1047:  "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
clasohm@1266: by (Asm_full_simp_tac 1);
clasohm@969: qed "infsys_pp1";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
lcp@1047:  "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
clasohm@1266: by (Asm_full_simp_tac 1);
clasohm@969: qed "infsys_pp2";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Fixpoints                                                    *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: (* Least fixpoints *)
clasohm@969: 
clasohm@969: val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
clasohm@969: by (rtac subsetD 1);
clasohm@969: by (rtac lfp_lemma2 1);
lcp@1047: by (resolve_tac prems 1);
lcp@1047: by (resolve_tac prems 1);
clasohm@969: qed "lfp_intro2";
clasohm@969: 
clasohm@969: val prems = goal MT.thy
clasohm@969:   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
clasohm@969: \   P(x)";
clasohm@969: by (cut_facts_tac prems 1);
lcp@1047: by (resolve_tac prems 1);
lcp@1047: by (rtac subsetD 1);
lcp@1047: by (rtac lfp_lemma3 1);
lcp@1047: by (assume_tac 1);
lcp@1047: by (assume_tac 1);
clasohm@969: qed "lfp_elim2";
clasohm@969: 
clasohm@969: val prems = goal MT.thy
wenzelm@3842:   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
clasohm@969: \   P(x)";
clasohm@969: by (cut_facts_tac prems 1);
lcp@1047: by (etac induct 1);
lcp@1047: by (assume_tac 1);
clasohm@969: by (eresolve_tac prems 1);
clasohm@969: qed "lfp_ind2";
clasohm@969: 
clasohm@969: (* Greatest fixpoints *)
clasohm@969: 
clasohm@969: (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
clasohm@969: 
clasohm@969: val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
clasohm@969: by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
clasohm@969: by (rtac (monoh RS monoD) 1);
lcp@1047: by (rtac (UnE RS subsetI) 1);
lcp@1047: by (assume_tac 1);
wenzelm@4089: by (blast_tac (claset() addSIs [cih]) 1);
clasohm@969: by (rtac (monoh RS monoD RS subsetD) 1);
clasohm@969: by (rtac Un_upper2 1);
clasohm@969: by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
clasohm@969: qed "gfp_coind2";
clasohm@969: 
clasohm@969: val [gfph,monoh,caseh] = goal MT.thy 
clasohm@969:   "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
lcp@1047: by (rtac caseh 1);
lcp@1047: by (rtac subsetD 1);
lcp@1047: by (rtac gfp_lemma2 1);
lcp@1047: by (rtac monoh 1);
lcp@1047: by (rtac gfph 1);
clasohm@969: qed "gfp_elim2";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Expressions                                                  *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
clasohm@969: 
clasohm@969: val e_disjs = 
clasohm@969:   [ e_disj_const_var, 
clasohm@969:     e_disj_const_fn, 
clasohm@969:     e_disj_const_fix, 
clasohm@969:     e_disj_const_app,
clasohm@969:     e_disj_var_fn, 
clasohm@969:     e_disj_var_fix, 
clasohm@969:     e_disj_var_app, 
clasohm@969:     e_disj_fn_fix, 
clasohm@969:     e_disj_fn_app, 
clasohm@969:     e_disj_fix_app
clasohm@969:   ];
clasohm@969: 
clasohm@969: val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
clasohm@969: val e_disj_se = (e_disj_si RL [notE]);
clasohm@969: 
clasohm@969: fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Values                                                      *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: val v_disjs = [v_disj_const_clos];
clasohm@969: val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
clasohm@969: val v_disj_se = (v_disj_si RL [notE]);
clasohm@969: 
clasohm@969: val v_injs = [v_const_inj, v_clos_inj];
clasohm@969: 
clasohm@969: fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Evaluations                                                  *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: (* Monotonicity of eval_fun *)
clasohm@969: 
clasohm@969: goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
clasohm@969: by infsys_mono_tac;
clasohm@969: qed "eval_fun_mono";
clasohm@969: 
clasohm@969: (* Introduction rules *)
clasohm@969: 
clasohm@969: goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
paulson@2935: 	(*Naughty!  But the quantifiers are nested VERY deeply...*)
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "eval_const";
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969:   "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@1266: qed "eval_var2";
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969:   "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "eval_fn";
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969:   " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969: \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "eval_fix";
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def]
clasohm@969:   " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
clasohm@969: \   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "eval_app1";
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def] 
clasohm@969:   " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
clasohm@969: \       ve |- e2 ---> v2; \
clasohm@969: \       vem + {xm |-> v2} |- em ---> v \
clasohm@969: \   |] ==> \
clasohm@969: \   ve |- e1 @ e2 ---> v";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [disjI2]) 1);
clasohm@969: qed "eval_app2";
clasohm@969: 
clasohm@969: (* Strong elimination, induction on evaluations *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [eval_def, eval_rel_def]
clasohm@969:   " [| ve |- e ---> v; \
clasohm@972: \      !!ve c. P(((ve,e_const(c)),v_const(c))); \
clasohm@972: \      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
clasohm@972: \      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
clasohm@969: \      !!ev1 ev2 ve cl e. \
clasohm@969: \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@972: \        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
clasohm@969: \      !!ve c1 c2 e1 e2. \
clasohm@972: \        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
clasohm@972: \        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
clasohm@969: \      !!ve vem xm e1 e2 em v v2. \
clasohm@972: \        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
clasohm@972: \            P(((ve,e2),v2)); \
clasohm@972: \            P(((vem + {xm |-> v2},em),v)) \
clasohm@969: \        |] ==> \
clasohm@972: \        P(((ve,e1 @ e2),v)) \
clasohm@969: \   |] ==> \
clasohm@972: \   P(((ve,e),v))";
clasohm@969: by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969: by (rtac eval_fun_mono 1);
clasohm@969: by (rewtac eval_fun_def);
clasohm@969: by (dtac CollectD 1);
paulson@4153: by Safe_tac;
clasohm@969: by (ALLGOALS (resolve_tac prems));
paulson@2935: by (ALLGOALS (Blast_tac));
clasohm@969: qed "eval_ind0";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " [| ve |- e ---> v; \
clasohm@969: \      !!ve c. P ve (e_const c) (v_const c); \
clasohm@969: \      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
clasohm@969: \      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
clasohm@969: \      !!ev1 ev2 ve cl e. \
clasohm@969: \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
clasohm@969: \        P ve (fix ev2(ev1) = e) (v_clos cl); \
clasohm@969: \      !!ve c1 c2 e1 e2. \
clasohm@969: \        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
clasohm@969: \        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
clasohm@969: \      !!ve vem evm e1 e2 em v v2. \
clasohm@969: \        [|  P ve e1 (v_clos <|evm,em,vem|>); \
clasohm@969: \            P ve e2 v2; \
clasohm@969: \            P (vem + {evm |-> v2}) em v \
clasohm@969: \        |] ==> P ve (e1 @ e2) v \
clasohm@969: \   |] ==> P ve e v";
clasohm@969: by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969: by (rtac eval_ind0 1);
clasohm@969: by (ALLGOALS (rtac infsys_pp1));
clasohm@969: by (ALLGOALS (resolve_tac prems));
clasohm@969: by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969: qed "eval_ind";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* Elaborations                                                 *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
clasohm@969: by infsys_mono_tac;
clasohm@969: qed "elab_fun_mono";
clasohm@969: 
clasohm@969: (* Introduction rules *)
clasohm@969: 
paulson@2935: goalw MT.thy [elab_def, elab_rel_def] 
paulson@2935:   "!!te. c isof ty ==> te |- e_const(c) ===> ty";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "elab_const";
clasohm@969: 
paulson@2935: goalw MT.thy [elab_def, elab_rel_def] 
paulson@2935:   "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "elab_var";
clasohm@969: 
paulson@2935: goalw MT.thy [elab_def, elab_rel_def] 
paulson@2935:   "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "elab_fn";
clasohm@969: 
paulson@2935: goalw MT.thy [elab_def, elab_rel_def]
paulson@2935:   "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
paulson@2935: \        te |- fix f(x) = e ===> ty1->ty2";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [exI]) 1);
clasohm@969: qed "elab_fix";
clasohm@969: 
paulson@2935: goalw MT.thy [elab_def, elab_rel_def] 
paulson@2935:   "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
paulson@2935: \        te |- e1 @ e2 ===> ty2";
clasohm@969: by (rtac lfp_intro2 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
wenzelm@4089: by (blast_tac (claset() addSIs [disjI2]) 1);
clasohm@969: qed "elab_app";
clasohm@969: 
clasohm@969: (* Strong elimination, induction on elaborations *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [elab_def, elab_rel_def]
clasohm@969:   " [| te |- e ===> t; \
clasohm@972: \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
clasohm@972: \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
clasohm@969: \      !!te x e t1 t2. \
clasohm@972: \        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
clasohm@972: \        P(((te,fn x => e),t1->t2)); \
clasohm@969: \      !!te f x e t1 t2. \
clasohm@969: \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@972: \           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
clasohm@969: \        |] ==> \
clasohm@972: \        P(((te,fix f(x) = e),t1->t2)); \
clasohm@969: \      !!te e1 e2 t1 t2. \
clasohm@972: \        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
clasohm@972: \           te |- e2 ===> t1; P(((te,e2),t1)) \
clasohm@969: \        |] ==> \
clasohm@972: \        P(((te,e1 @ e2),t2)) \
clasohm@969: \   |] ==> \
clasohm@972: \   P(((te,e),t))";
clasohm@969: by (resolve_tac (prems RL [lfp_ind2]) 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
clasohm@969: by (dtac CollectD 1);
paulson@4153: by Safe_tac;
clasohm@969: by (ALLGOALS (resolve_tac prems));
paulson@2935: by (ALLGOALS (Blast_tac));
clasohm@969: qed "elab_ind0";
clasohm@969: 
clasohm@969: val prems = goal MT.thy
clasohm@969:   " [| te |- e ===> t; \
clasohm@969: \       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969: \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969: \      !!te x e t1 t2. \
clasohm@969: \        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
clasohm@969: \        P te (fn x => e) (t1->t2); \
clasohm@969: \      !!te f x e t1 t2. \
clasohm@969: \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
clasohm@969: \           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
clasohm@969: \        |] ==> \
clasohm@969: \        P te (fix f(x) = e) (t1->t2); \
clasohm@969: \      !!te e1 e2 t1 t2. \
clasohm@969: \        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
clasohm@969: \           te |- e2 ===> t1; P te e2 t1 \
clasohm@969: \        |] ==> \
clasohm@969: \        P te (e1 @ e2) t2 \ 
clasohm@969: \   |] ==> \
clasohm@969: \   P te e t";
clasohm@969: by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969: by (rtac elab_ind0 1);
clasohm@969: by (ALLGOALS (rtac infsys_pp1));
clasohm@969: by (ALLGOALS (resolve_tac prems));
clasohm@969: by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969: qed "elab_ind";
clasohm@969: 
clasohm@969: (* Weak elimination, case analysis on elaborations *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [elab_def, elab_rel_def]
clasohm@969:   " [| te |- e ===> t; \
clasohm@972: \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
clasohm@972: \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
clasohm@969: \      !!te x e t1 t2. \
clasohm@972: \        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
clasohm@969: \      !!te f x e t1 t2. \
clasohm@969: \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@972: \        P(((te,fix f(x) = e),t1->t2)); \
clasohm@969: \      !!te e1 e2 t1 t2. \
clasohm@969: \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
clasohm@972: \        P(((te,e1 @ e2),t2)) \
clasohm@969: \   |] ==> \
clasohm@972: \   P(((te,e),t))";
clasohm@969: by (resolve_tac (prems RL [lfp_elim2]) 1);
clasohm@969: by (rtac elab_fun_mono 1);
clasohm@969: by (rewtac elab_fun_def);
clasohm@969: by (dtac CollectD 1);
paulson@4153: by Safe_tac;
clasohm@969: by (ALLGOALS (resolve_tac prems));
paulson@2935: by (ALLGOALS (Blast_tac));
clasohm@969: qed "elab_elim0";
clasohm@969: 
clasohm@969: val prems = goal MT.thy
clasohm@969:   " [| te |- e ===> t; \
clasohm@969: \       !!te c t. c isof t ==> P te (e_const c) t; \
clasohm@969: \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
clasohm@969: \      !!te x e t1 t2. \
clasohm@969: \        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
clasohm@969: \      !!te f x e t1 t2. \
clasohm@969: \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
clasohm@969: \        P te (fix f(x) = e) (t1->t2); \
clasohm@969: \      !!te e1 e2 t1 t2. \
clasohm@969: \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
clasohm@969: \        P te (e1 @ e2) t2 \ 
clasohm@969: \   |] ==> \
clasohm@969: \   P te e t";
clasohm@969: by (res_inst_tac [("P","P")] infsys_pp2 1);
clasohm@969: by (rtac elab_elim0 1);
clasohm@969: by (ALLGOALS (rtac infsys_pp1));
clasohm@969: by (ALLGOALS (resolve_tac prems));
clasohm@969: by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
clasohm@969: qed "elab_elim";
clasohm@969: 
clasohm@969: (* Elimination rules for each expression *)
clasohm@969: 
clasohm@969: fun elab_e_elim_tac p = 
clasohm@969:   ( (rtac elab_elim 1) THEN 
clasohm@969:     (resolve_tac p 1) THEN 
paulson@2935:     (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
clasohm@969:   );
clasohm@969: 
clasohm@969: val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
clasohm@969: by (elab_e_elim_tac prems);
clasohm@969: qed "elab_const_elim_lem";
clasohm@969: 
clasohm@969: val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (dtac elab_const_elim_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "elab_const_elim";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
clasohm@969: by (elab_e_elim_tac prems);
clasohm@969: qed "elab_var_elim_lem";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (dtac elab_var_elim_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "elab_var_elim";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " te |- e ===> t ==> \
clasohm@969: \   ( e = fn x1 => e1 --> \
wenzelm@3842: \     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
clasohm@969: \   )";
clasohm@969: by (elab_e_elim_tac prems);
clasohm@969: qed "elab_fn_elim_lem";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " te |- fn x1 => e1 ===> t ==> \
clasohm@969: \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (dtac elab_fn_elim_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "elab_fn_elim";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " te |- e ===> t ==> \
clasohm@969: \   (e = fix f(x) = e1 --> \
clasohm@969: \   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
clasohm@969: by (elab_e_elim_tac prems);
clasohm@969: qed "elab_fix_elim_lem";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " te |- fix ev1(ev2) = e1 ===> t ==> \
clasohm@969: \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (dtac elab_fix_elim_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "elab_fix_elim";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@969:   " te |- e ===> t2 ==> \
clasohm@969: \   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
clasohm@969: by (elab_e_elim_tac prems);
clasohm@969: qed "elab_app_elim_lem";
clasohm@969: 
clasohm@1266: val prems = goal MT.thy
clasohm@1266:  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (dtac elab_app_elim_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "elab_app_elim";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* The extended correspondence relation                       *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: (* Monotonicity of hasty_fun *)
clasohm@969: 
clasohm@969: goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
clasohm@969: by infsys_mono_tac;
paulson@2935: by (Blast_tac 1);
paulson@2935: qed "mono_hasty_fun";
clasohm@969: 
clasohm@969: (* 
clasohm@969:   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
clasohm@969:   enjoys two strong indtroduction (co-induction) rules and an elimination rule.
clasohm@969: *)
clasohm@969: 
clasohm@969: (* First strong indtroduction (co-induction) rule for hasty_rel *)
clasohm@969: 
clasohm@1266: val prems =
clasohm@1266:   goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac gfp_coind2 1);
clasohm@969: by (rewtac MT.hasty_fun_def);
lcp@1047: by (rtac CollectI 1);
lcp@1047: by (rtac disjI1 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: by (rtac mono_hasty_fun 1);
clasohm@969: qed "hasty_rel_const_coind";
clasohm@969: 
clasohm@969: (* Second strong introduction (co-induction) rule for hasty_rel *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [hasty_rel_def]
clasohm@969:   " [|  te |- fn ev => e ===> t; \
clasohm@969: \       ve_dom(ve) = te_dom(te); \
clasohm@969: \       ! ev1. \
clasohm@969: \         ev1:ve_dom(ve) --> \
clasohm@972: \         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
clasohm@969: \   |] ==> \
clasohm@972: \   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac gfp_coind2 1);
clasohm@969: by (rewtac hasty_fun_def);
lcp@1047: by (rtac CollectI 1);
lcp@1047: by (rtac disjI2 1);
paulson@2935: by (blast_tac HOL_cs 1);
clasohm@969: by (rtac mono_hasty_fun 1);
clasohm@969: qed "hasty_rel_clos_coind";
clasohm@969: 
clasohm@969: (* Elimination rule for hasty_rel *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [hasty_rel_def]
wenzelm@3842:   " [| !! c t. c isof t ==> P((v_const(c),t)); \
clasohm@969: \      !! te ev e t ve. \
clasohm@969: \        [| te |- fn ev => e ===> t; \
clasohm@969: \           ve_dom(ve) = te_dom(te); \
wenzelm@3842: \           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
clasohm@972: \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
clasohm@972: \      (v,t) : hasty_rel \
clasohm@972: \   |] ==> P((v,t))";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (etac gfp_elim2 1);
clasohm@969: by (rtac mono_hasty_fun 1);
clasohm@969: by (rewtac hasty_fun_def);
clasohm@969: by (dtac CollectD 1);
clasohm@969: by (fold_goals_tac [hasty_fun_def]);
paulson@4153: by Safe_tac;
paulson@2935: by (REPEAT (ares_tac prems 1));
clasohm@969: qed "hasty_rel_elim0";
clasohm@969: 
clasohm@969: val prems = goal MT.thy 
clasohm@972:   " [| (v,t) : hasty_rel; \
wenzelm@3842: \      !! c t. c isof t ==> P (v_const c) t; \
clasohm@969: \      !! te ev e t ve. \
clasohm@969: \        [| te |- fn ev => e ===> t; \
clasohm@969: \           ve_dom(ve) = te_dom(te); \
wenzelm@3842: \           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
clasohm@969: \        |] ==> P (v_clos <|ev,e,ve|>) t \
clasohm@969: \   |] ==> P v t";
clasohm@969: by (res_inst_tac [("P","P")] infsys_p2 1);
clasohm@969: by (rtac hasty_rel_elim0 1);
clasohm@969: by (ALLGOALS (rtac infsys_p1));
clasohm@969: by (ALLGOALS (resolve_tac prems));
clasohm@969: by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
clasohm@969: qed "hasty_rel_elim";
clasohm@969: 
clasohm@969: (* Introduction rules for hasty *)
clasohm@969: 
paulson@2935: goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
paulson@2935: by (etac hasty_rel_const_coind 1);
clasohm@969: qed "hasty_const";
clasohm@969: 
paulson@2935: goalw MT.thy [hasty_def,hasty_env_def] 
paulson@2935:  "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
clasohm@969: by (rtac hasty_rel_clos_coind 1);
wenzelm@4089: by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
clasohm@969: qed "hasty_clos";
clasohm@969: 
clasohm@969: (* Elimination on constants for hasty *)
clasohm@969: 
paulson@2935: goalw MT.thy [hasty_def] 
paulson@2935:   "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
clasohm@969: by (rtac hasty_rel_elim 1);
paulson@2935: by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
clasohm@969: qed "hasty_elim_const_lem";
clasohm@969: 
paulson@2935: goal MT.thy "!!c. v_const(c) hasty t ==> c isof t";
paulson@2935: by (dtac hasty_elim_const_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "hasty_elim_const";
clasohm@969: 
clasohm@969: (* Elimination on closures for hasty *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [hasty_env_def,hasty_def] 
clasohm@969:   " v hasty t ==> \
clasohm@969: \   ! x e ve. \
wenzelm@3842: \     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac hasty_rel_elim 1);
paulson@2935: by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
clasohm@969: qed "hasty_elim_clos_lem";
clasohm@969: 
paulson@2935: goal MT.thy 
paulson@2935:   "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
wenzelm@3842: \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
paulson@2935: by (dtac hasty_elim_clos_lem 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "hasty_elim_clos";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* The pointwise extension of hasty to environments             *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
lcp@1047: goal MT.thy
lcp@1047:   "!!ve. [| ve hastyenv te; v hasty t |] ==> \
lcp@1047: \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
lcp@1047: by (rewtac hasty_env_def);
wenzelm@4089: by (asm_full_simp_tac (simpset() delsimps mem_simps
clasohm@1266:                                 addsimps [ve_dom_owr, te_dom_owr]) 1);
paulson@2935: by (safe_tac HOL_cs);
lcp@1047: by (excluded_middle_tac "ev=x" 1);
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
paulson@2935: by (Blast_tac 1);
wenzelm@4089: by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
clasohm@969: qed "hasty_env1";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* The Consistency theorem                                      *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
paulson@2935: goal MT.thy 
paulson@2935:   "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
clasohm@969: by (dtac elab_const_elim 1);
clasohm@969: by (etac hasty_const 1);
clasohm@969: qed "consistency_const";
clasohm@969: 
paulson@2935: goalw MT.thy [hasty_env_def]
paulson@2935:   "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
paulson@2935: \       ve_app ve ev hasty t";
clasohm@969: by (dtac elab_var_elim 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "consistency_var";
clasohm@969: 
paulson@2935: goal MT.thy
paulson@2935:   "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
paulson@2935: \       v_clos(<| ev, e, ve |>) hasty t";
clasohm@969: by (rtac hasty_clos 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "consistency_fn";
clasohm@969: 
paulson@2935: goalw MT.thy [hasty_env_def,hasty_def]
paulson@2935:   "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
clasohm@969: \      ve hastyenv te ; \
clasohm@969: \      te |- fix ev2  ev1  = e ===> t \
clasohm@969: \   |] ==> \
clasohm@969: \   v_clos(cl) hasty t";
clasohm@969: by (dtac elab_fix_elim 1);
paulson@2935: by (safe_tac HOL_cs);
lcp@1047: (*Do a single unfolding of cl*)
lcp@1047: by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
lcp@1047: by (rtac hasty_rel_clos_coind 1);
clasohm@969: by (etac elab_fn 1);
wenzelm@4089: by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
clasohm@969: 
wenzelm@4089: by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1);
paulson@2935: by (safe_tac HOL_cs);
lcp@1047: by (excluded_middle_tac "ev2=ev1a" 1);
wenzelm@4089: by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: 
wenzelm@4089: by (asm_simp_tac (simpset() delsimps mem_simps
clasohm@1266:                            addsimps [ve_app_owr1, te_app_owr1]) 1);
clasohm@969: by (hyp_subst_tac 1);
clasohm@969: by (etac subst 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "consistency_fix";
clasohm@969: 
paulson@2935: goal MT.thy 
paulson@2935:   "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
clasohm@969: \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
clasohm@969: \      ve hastyenv te ; te |- e1 @ e2 ===> t \
clasohm@969: \   |] ==> \
clasohm@969: \   v_const(c_app c1 c2) hasty t";
clasohm@969: by (dtac elab_app_elim 1);
paulson@4153: by Safe_tac;
clasohm@969: by (rtac hasty_const 1);
clasohm@969: by (rtac isof_app 1);
clasohm@969: by (rtac hasty_elim_const 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: by (rtac hasty_elim_const 1);
paulson@2935: by (Blast_tac 1);
clasohm@969: qed "consistency_app1";
clasohm@969: 
paulson@2935: goal MT.thy 
paulson@2935:   "!!t.  [| ! t te. \
clasohm@969: \        ve hastyenv te  --> \
clasohm@969: \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
clasohm@969: \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
clasohm@969: \      ! t te. \
clasohm@969: \        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
clasohm@969: \      ve hastyenv te ; \
clasohm@969: \      te |- e1 @ e2 ===> t \
clasohm@969: \   |] ==> \
clasohm@969: \   v hasty t";
clasohm@969: by (dtac elab_app_elim 1);
paulson@4153: by Safe_tac;
lcp@1047: by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
lcp@1047: by (assume_tac 1);
lcp@1047: by (etac impE 1);
lcp@1047: by (assume_tac 1);
lcp@1047: by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
lcp@1047: by (assume_tac 1);
lcp@1047: by (etac impE 1);
lcp@1047: by (assume_tac 1);
clasohm@969: by (dtac hasty_elim_clos 1);
paulson@4153: by Safe_tac;
clasohm@969: by (dtac elab_fn_elim 1);
wenzelm@4089: by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
clasohm@969: qed "consistency_app2";
clasohm@969: 
lcp@1047: val [major] = goal MT.thy 
lcp@1047:   "ve |- e ---> v ==> \
lcp@1047: \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
clasohm@969: 
clasohm@969: (* Proof by induction on the structure of evaluations *)
clasohm@969: 
lcp@1047: by (rtac (major RS eval_ind) 1);
paulson@4153: by Safe_tac;
lcp@1047: by (DEPTH_SOLVE 
lcp@1047:     (ares_tac [consistency_const, consistency_var, consistency_fn,
clasohm@1465:                consistency_fix, consistency_app1, consistency_app2] 1));
clasohm@969: qed "consistency";
clasohm@969: 
clasohm@969: (* ############################################################ *)
clasohm@969: (* The Basic Consistency theorem                                *)
clasohm@969: (* ############################################################ *)
clasohm@969: 
clasohm@969: val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
clasohm@969:   "ve isofenv te ==> ve hastyenv te";
clasohm@969: by (cut_facts_tac prems 1);
paulson@4153: by Safe_tac;
lcp@1047: by (etac allE 1);
lcp@1047: by (etac impE 1);
lcp@1047: by (assume_tac 1);
lcp@1047: by (etac exE 1);
lcp@1047: by (etac conjE 1);
clasohm@969: by (dtac hasty_const 1);
clasohm@1266: by (Asm_simp_tac 1);
clasohm@969: qed "basic_consistency_lem";
clasohm@969: 
clasohm@969: val prems = goal MT.thy
clasohm@969:   "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
clasohm@969: by (cut_facts_tac prems 1);
clasohm@969: by (rtac hasty_elim_const 1);
clasohm@969: by (dtac consistency 1);
wenzelm@4089: by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
clasohm@969: qed "basic_consistency";
paulson@1584: 
paulson@1584: writeln"Reached end of file.";