--- a/ex/MT.ML Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/MT.ML Mon Nov 21 17:50:34 1994 +0100
@@ -22,7 +22,7 @@
by (hyp_subst_tac 1);
by (rtac singletonI 1);
by (assume_tac 1);
-val notsingletonI = result();
+qed "notsingletonI";
val prems = goalw MT.thy [Un_def]
"[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P";
@@ -31,7 +31,7 @@
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();
+qed "UnSE";
(* ############################################################ *)
(* Inference systems *)
@@ -49,14 +49,14 @@
by (rtac (fst_conv RS ssubst) 1);
by (rtac (snd_conv RS ssubst) 1);
by (resolve_tac prems 1);
-val infsys_p1 = result();
+qed "infsys_p1";
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();
+qed "infsys_p2";
val prems = goal MT.thy
"P(a,b,c) ==> P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>))";
@@ -65,7 +65,7 @@
by (rtac (snd_conv RS ssubst) 1);
by (rtac (snd_conv RS ssubst) 1);
by (resolve_tac prems 1);
-val infsys_pp1 = result();
+qed "infsys_pp1";
val prems = goal MT.thy
"P(fst(fst(<<a,b>,c>)),snd(fst(<<a,b>,c>)),snd(<<a,b>,c>)) ==> P(a,b,c)";
@@ -75,7 +75,7 @@
by (dtac (snd_conv RS subst) 1);
by (dtac (snd_conv RS subst) 1);
by (assume_tac 1);
-val infsys_pp2 = result();
+qed "infsys_pp2";
(* ############################################################ *)
(* Fixpoints *)
@@ -87,7 +87,7 @@
by (rtac subsetD 1);
by (rtac lfp_lemma2 1);
by (resolve_tac prems 1);brs prems 1;
-val lfp_intro2 = result();
+qed "lfp_intro2";
val prems = goal MT.thy
" [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
@@ -95,7 +95,7 @@
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();
+qed "lfp_elim2";
val prems = goal MT.thy
" [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
@@ -103,7 +103,7 @@
by (cut_facts_tac prems 1);
by (etac induct 1);ba 1;
by (eresolve_tac prems 1);
-val lfp_ind2 = result();
+qed "lfp_ind2";
(* Greatest fixpoints *)
@@ -117,12 +117,12 @@
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();
+qed "gfp_coind2";
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();
+qed "gfp_elim2";
(* ############################################################ *)
(* Expressions *)
@@ -168,7 +168,7 @@
goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
by infsys_mono_tac;
-val eval_fun_mono = result();
+qed "eval_fun_mono";
(* Introduction rules *)
@@ -178,7 +178,7 @@
by (rewtac eval_fun_def);
by (rtac CollectI 1);br disjI1 1;
by (fast_tac HOL_cs 1);
-val eval_const = result();
+qed "eval_const";
val prems = goalw MT.thy [eval_def, eval_rel_def]
"ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app(ve,ev)";
@@ -188,7 +188,7 @@
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();
+qed "eval_var";
val prems = goalw MT.thy [eval_def, eval_rel_def]
"ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
@@ -198,7 +198,7 @@
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();
+qed "eval_fn";
val prems = goalw MT.thy [eval_def, eval_rel_def]
" cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
@@ -209,7 +209,7 @@
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();
+qed "eval_fix";
val prems = goalw MT.thy [eval_def, eval_rel_def]
" [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
@@ -220,7 +220,7 @@
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();
+qed "eval_app1";
val prems = goalw MT.thy [eval_def, eval_rel_def]
" [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \
@@ -234,7 +234,7 @@
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();
+qed "eval_app2";
(* Strong elimination, induction on evaluations *)
@@ -264,7 +264,7 @@
by (safe_tac HOL_cs);
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (fast_tac set_cs));
-val eval_ind0 = result();
+qed "eval_ind0";
val prems = goal MT.thy
" [| ve |- e ---> v; \
@@ -288,7 +288,7 @@
by (ALLGOALS (rtac infsys_pp1));
by (ALLGOALS (resolve_tac prems));
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
-val eval_ind = result();
+qed "eval_ind";
(* ############################################################ *)
(* Elaborations *)
@@ -296,7 +296,7 @@
goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
by infsys_mono_tac;
-val elab_fun_mono = result();
+qed "elab_fun_mono";
(* Introduction rules *)
@@ -308,7 +308,7 @@
by (rewtac elab_fun_def);
by (rtac CollectI 1);br disjI1 1;
by (fast_tac HOL_cs 1);
-val elab_const = result();
+qed "elab_const";
val prems = goalw MT.thy [elab_def, elab_rel_def]
"x:te_dom(te) ==> te |- e_var(x) ===> te_app(te,x)";
@@ -318,7 +318,7 @@
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();
+qed "elab_var";
val prems = goalw MT.thy [elab_def, elab_rel_def]
"te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
@@ -328,7 +328,7 @@
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();
+qed "elab_fn";
val prems = goalw MT.thy [elab_def, elab_rel_def]
" te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
@@ -339,7 +339,7 @@
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();
+qed "elab_fix";
val prems = goalw MT.thy [elab_def, elab_rel_def]
" [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
@@ -350,7 +350,7 @@
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();
+qed "elab_app";
(* Strong elimination, induction on elaborations *)
@@ -380,7 +380,7 @@
by (safe_tac HOL_cs);
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (fast_tac set_cs));
-val elab_ind0 = result();
+qed "elab_ind0";
val prems = goal MT.thy
" [| te |- e ===> t; \
@@ -406,7 +406,7 @@
by (ALLGOALS (rtac infsys_pp1));
by (ALLGOALS (resolve_tac prems));
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
-val elab_ind = result();
+qed "elab_ind";
(* Weak elimination, case analysis on elaborations *)
@@ -431,7 +431,7 @@
by (safe_tac HOL_cs);
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (fast_tac set_cs));
-val elab_elim0 = result();
+qed "elab_elim0";
val prems = goal MT.thy
" [| te |- e ===> t; \
@@ -452,7 +452,7 @@
by (ALLGOALS (rtac infsys_pp1));
by (ALLGOALS (resolve_tac prems));
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
-val elab_elim = result();
+qed "elab_elim";
(* Elimination rules for each expression *)
@@ -464,25 +464,25 @@
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();
+qed "elab_const_elim_lem";
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();
+qed "elab_const_elim";
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();
+qed "elab_var_elim_lem";
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();
+qed "elab_var_elim";
val prems = goal MT.thy
" te |- e ===> t ==> \
@@ -490,7 +490,7 @@
\ (? t1 t2.t=t_fun(t1,t2) & te + {x1 |=> t1} |- e1 ===> t2) \
\ )";
by (elab_e_elim_tac prems);
-val elab_fn_elim_lem = result();
+qed "elab_fn_elim_lem";
val prems = goal MT.thy
" te |- fn x1 => e1 ===> t ==> \
@@ -498,14 +498,14 @@
by (cut_facts_tac prems 1);
by (dtac elab_fn_elim_lem 1);
by (fast_tac prop_cs 1);
-val elab_fn_elim = result();
+qed "elab_fn_elim";
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();
+qed "elab_fix_elim_lem";
val prems = goal MT.thy
" te |- fix ev1(ev2) = e1 ===> t ==> \
@@ -513,20 +513,20 @@
by (cut_facts_tac prems 1);
by (dtac elab_fix_elim_lem 1);
by (fast_tac prop_cs 1);
-val elab_fix_elim = result();
+qed "elab_fix_elim";
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();
+qed "elab_app_elim_lem";
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();
+qed "elab_app_elim";
(* ############################################################ *)
(* The extended correspondence relation *)
@@ -536,7 +536,7 @@
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
by infsys_mono_tac;
-val mono_hasty_fun = result();
+val mono_hasty_fun = store_thm("mono_hasty_fun", result());
(*
Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
@@ -552,7 +552,7 @@
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();
+qed "hasty_rel_const_coind";
(* Second strong introduction (co-induction) rule for hasty_rel *)
@@ -570,7 +570,7 @@
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();
+qed "hasty_rel_clos_coind";
(* Elimination rule for hasty_rel *)
@@ -592,7 +592,7 @@
by (safe_tac HOL_cs);
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (fast_tac set_cs));
-val hasty_rel_elim0 = result();
+qed "hasty_rel_elim0";
val prems = goal MT.thy
" [| <v,t> : hasty_rel; \
@@ -608,20 +608,20 @@
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();
+qed "hasty_rel_elim";
(* 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();
+qed "hasty_const";
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();
+qed "hasty_clos";
(* Elimination on constants for hasty *)
@@ -630,12 +630,12 @@
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();
+qed "hasty_elim_const_lem";
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();
+qed "hasty_elim_const";
(* Elimination on closures for hasty *)
@@ -646,13 +646,13 @@
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();
+qed "hasty_elim_clos_lem";
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();
+qed "hasty_elim_clos";
(* ############################################################ *)
(* The pointwise extension of hasty to environments *)
@@ -679,7 +679,7 @@
by (rtac (ve_app_owr1 RS ssubst) 1);
by (rtac (te_app_owr1 RS ssubst) 1);
by (assume_tac 1);
-val hasty_env1 = result();
+qed "hasty_env1";
(* ############################################################ *)
(* The Consistency theorem *)
@@ -690,7 +690,7 @@
by (cut_facts_tac prems 1);
by (dtac elab_const_elim 1);
by (etac hasty_const 1);
-val consistency_const = result();
+qed "consistency_const";
val prems = goalw MT.thy [hasty_env_def]
" [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
@@ -698,7 +698,7 @@
by (cut_facts_tac prems 1);
by (dtac elab_var_elim 1);
by (fast_tac HOL_cs 1);
-val consistency_var = result();
+qed "consistency_var";
val prems = goal MT.thy
" [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
@@ -706,7 +706,7 @@
by (cut_facts_tac prems 1);
by (rtac hasty_clos 1);
by (fast_tac prop_cs 1);
-val consistency_fn = result();
+qed "consistency_fn";
val prems = goalw MT.thy [hasty_env_def,hasty_def]
" [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
@@ -742,7 +742,7 @@
by (rtac (te_app_owr1 RS ssubst) 1);
by (etac subst 1);
by (fast_tac set_cs 1);
-val consistency_fix = result();
+qed "consistency_fix";
val prems = goal MT.thy
" [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \
@@ -759,7 +759,7 @@
by (fast_tac HOL_cs 1);
by (rtac hasty_elim_const 1);
by (fast_tac HOL_cs 1);
-val consistency_app1 = result();
+qed "consistency_app1";
val prems = goal MT.thy
" [| ! t te. \
@@ -784,7 +784,7 @@
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();
+qed "consistency_app2";
val prems = goal MT.thy
"ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
@@ -800,7 +800,7 @@
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();
+qed "consistency";
(* ############################################################ *)
(* The Basic Consistency theorem *)
@@ -813,7 +813,7 @@
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();
+qed "basic_consistency_lem";
val prems = goal MT.thy
"[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
@@ -821,6 +821,6 @@
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
-val basic_consistency = result();
+qed "basic_consistency";