--- a/src/CCL/CCL.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/CCL.ML Wed Nov 30 13:53:46 1994 +0100
@@ -16,17 +16,17 @@
(*** Congruence Rules ***)
(*similar to AP_THM in Gordon's HOL*)
-val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
+qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
-val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)"
+qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
by (fast_tac (set_cs addIs [po_abstractn]) 1);
-val abstractn = standard (allI RS (result() RS mp));
+val abstractn = store_thm("abstractn", standard (allI RS (result() RS mp)));
fun type_of_terms (Const("Trueprop",_) $
(Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
@@ -45,18 +45,18 @@
goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
by (rtac iff_refl 1);
-val Trm_iff = result();
+qed "Trm_iff";
goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
by (rtac iff_refl 1);
-val Dvg_iff = result();
+qed "Dvg_iff";
(*** Constructors are injective ***)
val prems = goal CCL.thy
"[| x=a; y=b; x=y |] ==> a=b";
by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
-val eq_lemma = result();
+qed "eq_lemma";
fun mk_inj_rl thy rews s =
let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
@@ -139,11 +139,11 @@
val major::prems = goal Set.thy "[| A=B; a:B <-> P |] ==> a:A <-> P";
by (resolve_tac (prems RL [major RS ssubst]) 1);
-val XHlemma1 = result();
+qed "XHlemma1";
goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> & P(t,t')} <-> Q)";
by (fast_tac ccl_cs 1);
-val XHlemma2 = result() RS mp;
+val XHlemma2 = store_thm("XHlemma2", result() RS mp);
(*** Pre-Order ***)
@@ -153,14 +153,14 @@
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
-val POgen_mono = result();
+qed "POgen_mono";
goalw CCL.thy [POgen_def,SIM_def]
"<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
by (rtac (iff_refl RS XHlemma2) 1);
-val POgenXH = result();
+qed "POgenXH";
goal CCL.thy
"t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
@@ -170,25 +170,25 @@
br (rewrite_rule [POgen_def,SIM_def]
(POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
by (rtac (iff_refl RS XHlemma2) 1);
-val poXH = result();
+qed "poXH";
goal CCL.thy "bot [= b";
by (rtac (poXH RS iffD2) 1);
by (simp_tac ccl_ss 1);
-val po_bot = result();
+qed "po_bot";
goal CCL.thy "a [= bot --> a=bot";
by (rtac impI 1);
by (dtac (poXH RS iffD1) 1);
by (etac rev_mp 1);
by (simp_tac ccl_ss 1);
-val bot_poleast = result() RS mp;
+val bot_poleast = store_thm("bot_poleast", result() RS mp);
goal CCL.thy "<a,b> [= <a',b'> <-> a [= a' & b [= b'";
by (rtac (poXH RS iff_trans) 1);
by (simp_tac ccl_ss 1);
by (fast_tac ccl_cs 1);
-val po_pair = result();
+qed "po_pair";
goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
by (rtac (poXH RS iff_trans) 1);
@@ -196,7 +196,7 @@
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
by (asm_simp_tac ccl_ss 1);
by (fast_tac ccl_cs 1);
-val po_lam = result();
+qed "po_lam";
val ccl_porews = [po_bot,po_pair,po_lam];
@@ -210,40 +210,40 @@
by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")]
(p5 RS po_abstractn RS po_cong RS po_trans) 1);
by (rtac po_refl 1);
-val case_pocong = result();
+qed "case_pocong";
val [p1,p2] = goalw CCL.thy ccl_data_defs
"[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'";
by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
-val apply_pocong = result();
+qed "apply_pocong";
val prems = goal CCL.thy "~ lam x.b(x) [= bot";
by (rtac notI 1);
by (dtac bot_poleast 1);
by (etac (distinctness RS notE) 1);
-val npo_lam_bot = result();
+qed "npo_lam_bot";
val eq1::eq2::prems = goal CCL.thy
"[| x=a; y=b; x[=y |] ==> a[=b";
by (rtac (eq1 RS subst) 1);
by (rtac (eq2 RS subst) 1);
by (resolve_tac prems 1);
-val po_lemma = result();
+qed "po_lemma";
goal CCL.thy "~ <a,b> [= lam x.f(x)";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
-val npo_pair_lam = result();
+qed "npo_pair_lam";
goal CCL.thy "~ lam x.f(x) [= <a,b>";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
-val npo_lam_pair = result();
+qed "npo_lam_pair";
fun mk_thm s = prove_goal CCL.thy s (fn _ =>
[rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
@@ -262,7 +262,7 @@
val prems = goal CCL.thy "[| <t,u> : R; R <= POgen(R) |] ==> t [= u";
by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
by (REPEAT (ares_tac prems 1));
-val po_coinduct = result();
+qed "po_coinduct";
fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
@@ -274,7 +274,7 @@
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
-val EQgen_mono = result();
+qed "EQgen_mono";
goalw CCL.thy [EQgen_def,SIM_def]
"<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | \
@@ -282,7 +282,7 @@
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
by (rtac (iff_refl RS XHlemma2) 1);
-val EQgenXH = result();
+qed "EQgenXH";
goal CCL.thy
"t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \
@@ -297,18 +297,18 @@
br (rewrite_rule [EQgen_def,SIM_def]
(EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
by (rtac (iff_refl RS XHlemma2) 1);
-val eqXH = result();
+qed "eqXH";
val prems = goal CCL.thy "[| <t,u> : R; R <= EQgen(R) |] ==> t = u";
by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
by (REPEAT (ares_tac prems 1));
-val eq_coinduct = result();
+qed "eq_coinduct";
val prems = goal CCL.thy
"[| <t,u> : R; R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
by (REPEAT (ares_tac (EQgen_mono::prems) 1));
-val eq_coinduct3 = result();
+qed "eq_coinduct3";
fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
@@ -318,17 +318,17 @@
goalw CCL.thy [apply_def] "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
by (safe_tac ccl_cs);
by (simp_tac ccl_ss 1);
-val cond_eta = result() RS mp;
+val cond_eta = store_thm("cond_eta", result() RS mp);
goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
by (fast_tac set_cs 1);
-val exhaustion = result();
+qed "exhaustion";
val prems = goal CCL.thy
"[| P(bot); P(true); P(false); !!x y.P(<x,y>); !!b.P(lam x.b(x)) |] ==> P(t)";
by (cut_facts_tac [exhaustion] 1);
by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
-val term_case = result();
+qed "term_case";
fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;
--- a/src/CCL/Fix.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Fix.ML Wed Nov 30 13:53:46 1994 +0100
@@ -16,30 +16,30 @@
by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
by (ALLGOALS (simp_tac term_ss));
by (REPEAT (ares_tac [base,step] 1));
-val fix_ind = result();
+qed "fix_ind";
(*** Inclusive Predicates ***)
val prems = goalw Fix.thy [INCL_def]
"INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
by (rtac iff_refl 1);
-val inclXH = result();
+qed "inclXH";
val prems = goal Fix.thy
"[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
-val inclI = result();
+qed "inclI";
val incl::prems = goal Fix.thy
"[| INCL(P); !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)]
@ prems)) 1);
-val inclD = result();
+qed "inclD";
val incl::prems = goal Fix.thy
"[| INCL(P); (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
-val inclE = result();
+qed "inclE";
(*** Lemmas for Inclusive Predicates ***)
@@ -53,24 +53,24 @@
by (assume_tac 2);
by (rtac (napplyBzero RS ssubst) 1);
by (rtac po_cong 1 THEN rtac po_bot 1);
-val npo_INCL = result();
+qed "npo_INCL";
val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val conj_INCL = result();
+qed "conj_INCL";
val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val all_INCL = result();
+qed "all_INCL";
val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val ball_INCL = result();
+qed "ball_INCL";
goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
by (simp_tac (term_ss addsimps [eq_iff]) 1);
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
-val eq_INCL = result();
+qed "eq_INCL";
(*** Derivation of Reachability Condition ***)
@@ -78,13 +78,13 @@
goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
by (rtac (fixB RS sym) 1);
-val fix_idgenfp = result();
+qed "fix_idgenfp";
goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
by (simp_tac term_ss 1);
by (rtac (term_case RS allI) 1);
by (ALLGOALS (simp_tac term_ss));
-val id_idgenfp = result();
+qed "id_idgenfp";
(* All fixed points are lam-expressions *)
@@ -92,14 +92,14 @@
by (rtac (prem RS subst) 1);
by (rewtac idgen_def);
by (rtac refl 1);
-val idgenfp_lam = result();
+qed "idgenfp_lam";
(* Lemmas for rewriting fixed points of idgen *)
val prems = goalw Fix.thy [idgen_def]
"[| a = b; a ` t = u |] ==> b ` t = u";
by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
-val l_lemma= result();
+qed "l_lemma";
val idgen_lemmas =
let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
@@ -120,12 +120,12 @@
by (rtac (p2 RS cond_eta RS ssubst) 1);
by (rtac (p3 RS cond_eta RS ssubst) 1);
by (rtac (p1 RS (po_lam RS iffD2)) 1);
-val po_eta = result();
+qed "po_eta";
val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
by (rtac (prem RS subst) 1);
by (rtac refl 1);
-val po_eta_lemma = result();
+qed "po_eta_lemma";
val [prem] = goal Fix.thy
"idgen(d) = d ==> \
@@ -135,14 +135,14 @@
by (term_case_tac "t" 1);
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
-val lemma1 = result();
+qed "lemma1";
val [prem] = goal Fix.thy
"idgen(d) = d ==> fix(idgen) [= d";
by (rtac (allI RS po_eta) 1);
by (rtac (lemma1 RSN(2,po_coinduct)) 1);
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
-val fix_least_idgen = result();
+qed "fix_least_idgen";
val [prem] = goal Fix.thy
"idgen(d) = d ==> \
@@ -151,7 +151,7 @@
by (term_case_tac "a" 1);
by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
-val lemma2 = result();
+qed "lemma2";
val [prem] = goal Fix.thy
"idgen(d) = d ==> lam x.x [= d";
@@ -159,20 +159,20 @@
by (rtac (lemma2 RSN(2,po_coinduct)) 1);
by (simp_tac term_ss 1);
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
-val id_least_idgen = result();
+qed "id_least_idgen";
goal Fix.thy "fix(idgen) = lam x.x";
by (fast_tac (term_cs addIs [eq_iff RS iffD2,
id_idgenfp RS fix_least_idgen,
fix_idgenfp RS id_least_idgen]) 1);
-val reachability = result();
+qed "reachability";
(********)
val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
by (rtac (prem RS sym RS subst) 1);
by (rtac applyB 1);
-val id_apply = result();
+qed "id_apply";
val prems = goal Fix.thy
"[| P(bot); P(true); P(false); \
@@ -190,5 +190,5 @@
by (res_inst_tac [("t","xa")] term_case 1);
by (ALLGOALS (simp_tac term_ss));
by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
-val term_ind = result();
+qed "term_ind";
--- a/src/CCL/Gfp.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Gfp.ML Wed Nov 30 13:53:46 1994 +0100
@@ -18,27 +18,27 @@
val prems = goalw Gfp.thy [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)";
by (rtac (CollectI RS Union_upper) 1);
by (resolve_tac prems 1);
-val gfp_upperbound = result();
+qed "gfp_upperbound";
val prems = goalw Gfp.thy [gfp_def]
"[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A";
by (REPEAT (ares_tac ([Union_least]@prems) 1));
by (etac CollectD 1);
-val gfp_least = result();
+qed "gfp_least";
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
rtac (mono RS monoD), rtac gfp_upperbound, atac]);
-val gfp_lemma2 = result();
+qed "gfp_lemma2";
val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD),
rtac gfp_lemma2, rtac mono]);
-val gfp_lemma3 = result();
+qed "gfp_lemma3";
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
-val gfp_Tarski = result();
+qed "gfp_Tarski";
(*** Coinduction rules for greatest fixed points ***)
@@ -47,7 +47,7 @@
"[| a: A; A <= f(A) |] ==> a : gfp(f)";
by (rtac (gfp_upperbound RS subsetD) 1);
by (REPEAT (ares_tac prems 1));
-val coinduct = result();
+qed "coinduct";
val [prem,mono] = goal Gfp.thy
"[| A <= f(A) Un gfp(f); mono(f) |] ==> \
@@ -57,7 +57,7 @@
by (rtac (mono RS gfp_Tarski RS subst) 1);
by (rtac (prem RS Un_least) 1);
by (rtac Un_upper2 1);
-val coinduct2_lemma = result();
+qed "coinduct2_lemma";
(*strong version, thanks to Martin Coen*)
val ainA::prems = goal Gfp.thy
@@ -65,7 +65,7 @@
by (rtac coinduct 1);
by (rtac (prems MRS coinduct2_lemma) 2);
by (resolve_tac [ainA RS UnI1] 1);
-val coinduct2 = result();
+qed "coinduct2";
(*** Even Stronger version of coinduct [by Martin Coen]
- instead of the condition A <= f(A)
@@ -73,7 +73,7 @@
val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
-val coinduct3_mono_lemma= result();
+qed "coinduct3_mono_lemma";
val [prem,mono] = goal Gfp.thy
"[| A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> \
@@ -87,7 +87,7 @@
by (rtac (mono RS monoD) 1);
by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
by (rtac Un_upper2 1);
-val coinduct3_lemma = result();
+qed "coinduct3_lemma";
val ainA::prems = goal Gfp.thy
"[| a:A; A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
@@ -95,7 +95,7 @@
by (rtac (prems MRS coinduct3_lemma) 2);
by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
by (rtac (ainA RS UnI2 RS UnI1) 1);
-val coinduct3 = result();
+qed "coinduct3";
(** Definition forms of gfp_Tarski, to control unfolding **)
@@ -103,25 +103,25 @@
val [rew,mono] = goal Gfp.thy "[| h==gfp(f); mono(f) |] ==> h = f(h)";
by (rewtac rew);
by (rtac (mono RS gfp_Tarski) 1);
-val def_gfp_Tarski = result();
+qed "def_gfp_Tarski";
val rew::prems = goal Gfp.thy
"[| h==gfp(f); a:A; A <= f(A) |] ==> a: h";
by (rewtac rew);
by (REPEAT (ares_tac (prems @ [coinduct]) 1));
-val def_coinduct = result();
+qed "def_coinduct";
val rew::prems = goal Gfp.thy
"[| h==gfp(f); a:A; A <= f(A) Un h; mono(f) |] ==> a: h";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct2]) 1));
-val def_coinduct2 = result();
+qed "def_coinduct2";
val rew::prems = goal Gfp.thy
"[| h==gfp(f); a:A; A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
by (rewtac rew);
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
-val def_coinduct3 = result();
+qed "def_coinduct3";
(*Monotonicity of gfp!*)
val prems = goal Gfp.thy
@@ -131,4 +131,4 @@
by (rtac gfp_lemma2 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
-val gfp_mono = result();
+qed "gfp_mono";
--- a/src/CCL/Hered.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Hered.ML Wed Nov 30 13:53:46 1994 +0100
@@ -15,13 +15,13 @@
goalw Hered.thy [HTTgen_def] "mono(%X.HTTgen(X))";
by (rtac monoI 1);
by (fast_tac set_cs 1);
-val HTTgen_mono = result();
+qed "HTTgen_mono";
goalw Hered.thy [HTTgen_def]
"t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
\ (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
by (fast_tac set_cs 1);
-val HTTgenXH = result();
+qed "HTTgenXH";
goal Hered.thy
"t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
@@ -29,26 +29,26 @@
br (rewrite_rule [HTTgen_def]
(HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
by (fast_tac set_cs 1);
-val HTTXH = result();
+qed "HTTXH";
(*** Introduction Rules for HTT ***)
goal Hered.thy "~ bot : HTT";
by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
-val HTT_bot = result();
+qed "HTT_bot";
goal Hered.thy "true : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
-val HTT_true = result();
+qed "HTT_true";
goal Hered.thy "false : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
-val HTT_false = result();
+qed "HTT_false";
goal Hered.thy "<a,b> : HTT <-> a : HTT & b : HTT";
by (rtac (HTTXH RS iff_trans) 1);
by (fast_tac term_cs 1);
-val HTT_pair = result();
+qed "HTT_pair";
goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
by (rtac (HTTXH RS iff_trans) 1);
@@ -56,7 +56,7 @@
by (safe_tac term_cs);
by (asm_simp_tac term_ss 1);
by (fast_tac term_cs 1);
-val HTT_lam = result();
+qed "HTT_lam";
local
val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
@@ -80,7 +80,7 @@
val prems = goal Hered.thy "[| t : R; R <= HTTgen(R) |] ==> t : HTT";
by (rtac (HTT_def RS def_coinduct) 1);
by (REPEAT (ares_tac prems 1));
-val HTT_coinduct = result();
+qed "HTT_coinduct";
fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
@@ -88,7 +88,7 @@
"[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
by (REPEAT (ares_tac prems 1));
-val HTT_coinduct3 = result();
+qed "HTT_coinduct3";
val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
@@ -114,23 +114,23 @@
goal Hered.thy "Unit <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
-val UnitF = result();
+qed "UnitF";
goal Hered.thy "Bool <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val BoolF = result();
+qed "BoolF";
val prems = goal Hered.thy "[| A <= HTT; B <= HTT |] ==> A + B <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val PlusF = result();
+qed "PlusF";
val prems = goal Hered.thy
"[| A <= HTT; !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val SigmaF = result();
+qed "SigmaF";
(*** Formation Rules for Recursive types - using coinduction these only need ***)
(*** exhaution rule for type-former ***)
@@ -148,7 +148,7 @@
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
-val NatF = result();
+qed "NatF";
val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
by (safe_tac set_cs);
@@ -156,7 +156,7 @@
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E ListXH]) 1);
-val ListF = result();
+qed "ListF";
val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
by (safe_tac set_cs);
@@ -164,7 +164,7 @@
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E ListsXH]) 1);
-val ListsF = result();
+qed "ListsF";
val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
by (safe_tac set_cs);
@@ -172,7 +172,7 @@
by (fast_tac (set_cs addSIs HTTgenIs
addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)]
addEs [XH_to_E IListsXH]) 1);
-val IListsF = result();
+qed "IListsF";
(*** A possible use for this predicate is proving equality from pre-order ***)
(*** but it seems as easy (and more general) to do this directly by coinduction ***)
@@ -186,9 +186,9 @@
by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
by (ALLGOALS (fast_tac ccl_cs));
-val HTT_po_op = result();
+qed "HTT_po_op";
val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> t = u";
by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
-val HTT_po_eq = result();
+qed "HTT_po_eq";
*)
--- a/src/CCL/Lfp.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Lfp.ML Wed Nov 30 13:53:46 1994 +0100
@@ -18,27 +18,27 @@
val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
by (rtac (CollectI RS Inter_lower) 1);
by (resolve_tac prems 1);
-val lfp_lowerbound = result();
+qed "lfp_lowerbound";
val prems = goalw Lfp.thy [lfp_def]
"[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
by (etac CollectD 1);
-val lfp_greatest = result();
+qed "lfp_greatest";
val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
-val lfp_lemma2 = result();
+qed "lfp_lemma2";
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD),
rtac lfp_lemma2, rtac mono]);
-val lfp_lemma3 = result();
+qed "lfp_lemma3";
val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
-val lfp_Tarski = result();
+qed "lfp_Tarski";
(*** General induction rule for least fixed points ***)
@@ -53,14 +53,14 @@
rtac (Int_lower1 RS (mono RS monoD)),
rtac (mono RS lfp_lemma2),
rtac (CollectI RS subsetI), rtac indhyp, atac]);
-val induct = result();
+qed "induct";
(** Definition forms of lfp_Tarski and induct, to control unfolding **)
val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)";
by (rewtac rew);
by (rtac (mono RS lfp_Tarski) 1);
-val def_lfp_Tarski = result();
+qed "def_lfp_Tarski";
val rew::prems = goal Lfp.thy
"[| A == lfp(f); a:A; mono(f); \
@@ -68,7 +68,7 @@
\ |] ==> P(a)";
by (EVERY1 [rtac induct, (*backtracking to force correct induction*)
REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
-val def_induct = result();
+qed "def_induct";
(*Monotonicity of lfp!*)
val prems = goal Lfp.thy
@@ -78,5 +78,5 @@
by (resolve_tac prems 1);
by (rtac lfp_lemma2 1);
by (resolve_tac prems 1);
-val lfp_mono = result();
+qed "lfp_mono";
--- a/src/CCL/Set.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Set.ML Wed Nov 30 13:53:46 1994 +0100
@@ -16,36 +16,36 @@
val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
by (rtac (mem_Collect_iff RS iffD2) 1);
by (rtac prem 1);
-val CollectI = result();
+qed "CollectI";
val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1);
-val CollectD = result();
+qed "CollectD";
val CollectE = make_elim CollectD;
val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
by (rtac (set_extension RS iffD2) 1);
by (rtac (prem RS allI) 1);
-val set_ext = result();
+qed "set_ext";
(*** Bounded quantifiers ***)
val prems = goalw Set.thy [Ball_def]
"[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
-val ballI = result();
+qed "ballI";
val [major,minor] = goalw Set.thy [Ball_def]
"[| ALL x:A. P(x); x:A |] ==> P(x)";
by (rtac (minor RS (major RS spec RS mp)) 1);
-val bspec = result();
+qed "bspec";
val major::prems = goalw Set.thy [Ball_def]
"[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q";
by (rtac (major RS spec RS impCE) 1);
by (REPEAT (eresolve_tac prems 1));
-val ballE = result();
+qed "ballE";
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
fun ball_tac i = etac ballE i THEN contr_tac (i+1);
@@ -53,9 +53,9 @@
val prems = goalw Set.thy [Bex_def]
"[| P(x); x:A |] ==> EX x:A. P(x)";
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
-val bexI = result();
+qed "bexI";
-val bexCI = prove_goal Set.thy
+qed_goal "bexCI" Set.thy
"[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A.P(x)"
(fn prems=>
[ (rtac classical 1),
@@ -65,13 +65,13 @@
"[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q";
by (rtac (major RS exE) 1);
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
-val bexE = result();
+qed "bexE";
(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*)
val prems = goal Set.thy
"(ALL x:A. True) <-> True";
by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
-val ball_rew = result();
+qed "ball_rew";
(** Congruence rules **)
@@ -81,7 +81,7 @@
by (resolve_tac (prems RL [ssubst,iffD2]) 1);
by (REPEAT (ares_tac [ballI,iffI] 1
ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
-val ball_cong = result();
+qed "ball_cong";
val prems = goal Set.thy
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \
@@ -89,37 +89,37 @@
by (resolve_tac (prems RL [ssubst,iffD2]) 1);
by (REPEAT (etac bexE 1
ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
-val bex_cong = result();
+qed "bex_cong";
(*** Rules for subsets ***)
val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
by (REPEAT (ares_tac (prems @ [ballI]) 1));
-val subsetI = result();
+qed "subsetI";
(*Rule in Modus Ponens style*)
val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B";
by (rtac (major RS bspec) 1);
by (resolve_tac prems 1);
-val subsetD = result();
+qed "subsetD";
(*Classical elimination rule*)
val major::prems = goalw Set.thy [subset_def]
"[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P";
by (rtac (major RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
-val subsetCE = result();
+qed "subsetCE";
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
fun set_mp_tac i = etac subsetCE i THEN mp_tac i;
-val subset_refl = prove_goal Set.thy "A <= A"
+qed_goal "subset_refl" Set.thy "A <= A"
(fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
goal Set.thy "!!A B C. [| A<=B; B<=C |] ==> A<=C";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
-val subset_trans = result();
+qed "subset_trans";
(*** Rules for equality ***)
@@ -128,31 +128,31 @@
val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = B";
by (rtac (iffI RS set_ext) 1);
by (REPEAT (ares_tac (prems RL [subsetD]) 1));
-val subset_antisym = result();
+qed "subset_antisym";
val equalityI = subset_antisym;
(* Equality rules from ZF set theory -- are they appropriate here? *)
val prems = goal Set.thy "A = B ==> A<=B";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
-val equalityD1 = result();
+qed "equalityD1";
val prems = goal Set.thy "A = B ==> B<=A";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
-val equalityD2 = result();
+qed "equalityD2";
val prems = goal Set.thy
"[| A = B; [| A<=B; B<=A |] ==> P |] ==> P";
by (resolve_tac prems 1);
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
-val equalityE = result();
+qed "equalityE";
val major::prems = goal Set.thy
"[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P";
by (rtac (major RS equalityE) 1);
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
-val equalityCE = result();
+qed "equalityCE";
(*Lemma for creating induction formulae -- for "pattern matching" on p
To make the induction hypotheses usable, apply "spec" or "bspec" to
@@ -161,24 +161,24 @@
"[| p:A; !!z. z:A ==> p=z --> R |] ==> R";
by (rtac mp 1);
by (REPEAT (resolve_tac (refl::prems) 1));
-val setup_induction = result();
+qed "setup_induction";
goal Set.thy "{x.x:A} = A";
by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1));
-val trivial_set = result();
+qed "trivial_set";
(*** Rules for binary union -- Un ***)
val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
-val UnI1 = result();
+qed "UnI1";
val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B";
by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1));
-val UnI2 = result();
+qed "UnI2";
(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
+qed_goal "UnCI" Set.thy "(~c:B ==> c:A) ==> c : A Un B"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -188,7 +188,7 @@
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
by (rtac (major RS CollectD RS disjE) 1);
by (REPEAT (eresolve_tac prems 1));
-val UnE = result();
+qed "UnE";
(*** Rules for small intersection -- Int ***)
@@ -196,22 +196,22 @@
val prems = goalw Set.thy [Int_def]
"[| c:A; c:B |] ==> c : A Int B";
by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1));
-val IntI = result();
+qed "IntI";
val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A";
by (rtac (major RS CollectD RS conjunct1) 1);
-val IntD1 = result();
+qed "IntD1";
val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B";
by (rtac (major RS CollectD RS conjunct2) 1);
-val IntD2 = result();
+qed "IntD2";
val [major,minor] = goal Set.thy
"[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P";
by (rtac minor 1);
by (rtac (major RS IntD1) 1);
by (rtac (major RS IntD2) 1);
-val IntE = result();
+qed "IntE";
(*** Rules for set complement -- Compl ***)
@@ -219,7 +219,7 @@
val prems = goalw Set.thy [Compl_def]
"[| c:A ==> False |] ==> c : Compl(A)";
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
-val ComplI = result();
+qed "ComplI";
(*This form, with negated conclusion, works well with the Classical prover.
Negated assumptions behave like formulae on the right side of the notional
@@ -227,7 +227,7 @@
val major::prems = goalw Set.thy [Compl_def]
"[| c : Compl(A) |] ==> ~c:A";
by (rtac (major RS CollectD) 1);
-val ComplD = result();
+qed "ComplD";
val ComplE = make_elim ComplD;
@@ -236,11 +236,11 @@
goalw Set.thy [empty_def] "{x.False} = {}";
by (rtac refl 1);
-val empty_eq = result();
+qed "empty_eq";
val [prem] = goalw Set.thy [empty_def] "a : {} ==> P";
by (rtac (prem RS CollectD RS FalseE) 1);
-val emptyD = result();
+qed "emptyD";
val emptyE = make_elim emptyD;
@@ -248,18 +248,18 @@
by (rtac (prem RS swap) 1);
by (rtac equalityI 1);
by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
-val not_emptyD = result();
+qed "not_emptyD";
(*** Singleton sets ***)
goalw Set.thy [singleton_def] "a : {a}";
by (rtac CollectI 1);
by (rtac refl 1);
-val singletonI = result();
+qed "singletonI";
val [major] = goalw Set.thy [singleton_def] "b : {a} ==> b=a";
by (rtac (major RS CollectD) 1);
-val singletonD = result();
+qed "singletonD";
val singletonE = make_elim singletonD;
@@ -269,13 +269,13 @@
val prems = goalw Set.thy [UNION_def]
"[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))";
by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1));
-val UN_I = result();
+qed "UN_I";
val major::prems = goalw Set.thy [UNION_def]
"[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R";
by (rtac (major RS CollectD RS bexE) 1);
by (REPEAT (ares_tac prems 1));
-val UN_E = result();
+qed "UN_E";
val prems = goal Set.thy
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
@@ -283,27 +283,27 @@
by (REPEAT (etac UN_E 1
ORELSE ares_tac ([UN_I,equalityI,subsetI] @
(prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
-val UN_cong = result();
+qed "UN_cong";
(*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *)
val prems = goalw Set.thy [INTER_def]
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
-val INT_I = result();
+qed "INT_I";
val major::prems = goalw Set.thy [INTER_def]
"[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)";
by (rtac (major RS CollectD RS bspec) 1);
by (resolve_tac prems 1);
-val INT_D = result();
+qed "INT_D";
(*"Classical" elimination rule -- does not require proving X:C *)
val major::prems = goalw Set.thy [INTER_def]
"[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R";
by (rtac (major RS CollectD RS ballE) 1);
by (REPEAT (eresolve_tac prems 1));
-val INT_E = result();
+qed "INT_E";
val prems = goal Set.thy
"[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \
@@ -311,7 +311,7 @@
by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
by (REPEAT (dtac INT_D 1
ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
-val INT_cong = result();
+qed "INT_cong";
(*** Rules for Unions ***)
@@ -319,20 +319,20 @@
val prems = goalw Set.thy [Union_def]
"[| X:C; A:X |] ==> A : Union(C)";
by (REPEAT (resolve_tac (prems @ [UN_I]) 1));
-val UnionI = result();
+qed "UnionI";
val major::prems = goalw Set.thy [Union_def]
"[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R";
by (rtac (major RS UN_E) 1);
by (REPEAT (ares_tac prems 1));
-val UnionE = result();
+qed "UnionE";
(*** Rules for Inter ***)
val prems = goalw Set.thy [Inter_def]
"[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
by (REPEAT (ares_tac ([INT_I] @ prems) 1));
-val InterI = result();
+qed "InterI";
(*A "destruct" rule -- every X in C contains A as an element, but
A:X can hold when X:C does not! This rule is analogous to "spec". *)
@@ -340,11 +340,11 @@
"[| A : Inter(C); X:C |] ==> A:X";
by (rtac (major RS INT_D) 1);
by (resolve_tac prems 1);
-val InterD = result();
+qed "InterD";
(*"Classical" elimination rule -- does not require proving X:C *)
val major::prems = goalw Set.thy [Inter_def]
"[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R";
by (rtac (major RS INT_E) 1);
by (REPEAT (eresolve_tac prems 1));
-val InterE = result();
+qed "InterE";
--- a/src/CCL/Term.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Term.ML Wed Nov 30 13:53:46 1994 +0100
@@ -24,34 +24,34 @@
goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
by (res_inst_tac [("t","t")] term_case 1);
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val letB = result() RS mp;
+val letB = store_thm("letB", result() RS mp);
goalw Term.thy [let_def] "let x be bot in f(x) = bot";
by (rtac caseBbot 1);
-val letBabot = result();
+qed "letBabot";
goalw Term.thy [let_def] "let x be t in bot = bot";
by (resolve_tac ([caseBbot] RL [term_case]) 1);
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val letBbbot = result();
+qed "letBbbot";
goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val applyB = result();
+qed "applyB";
goalw Term.thy [apply_def] "bot ` a = bot";
by (rtac caseBbot 1);
-val applyBbot = result();
+qed "applyBbot";
goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
-val fixB = result();
+qed "fixB";
goalw Term.thy [letrec_def]
"letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
by (resolve_tac [fixB RS ssubst] 1 THEN
resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
-val letrecB = result();
+qed "letrecB";
val rawBs = caseBs @ [applyB,applyBbot];
--- a/src/CCL/Trancl.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Trancl.ML Wed Nov 30 13:53:46 1994 +0100
@@ -17,13 +17,13 @@
val prems = goalw Trancl.thy [trans_def]
"(!! x y z. [| <x,y>:r; <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
-val transI = result();
+qed "transI";
val major::prems = goalw Trancl.thy [trans_def]
"[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
by (cut_facts_tac [major] 1);
by (fast_tac (FOL_cs addIs prems) 1);
-val transD = result();
+qed "transD";
(** Identity relation **)
@@ -31,7 +31,7 @@
by (rtac CollectI 1);
by (rtac exI 1);
by (rtac refl 1);
-val idI = result();
+qed "idI";
val major::prems = goalw Trancl.thy [id_def]
"[| p: id; !!x.[| p = <x,x> |] ==> P \
@@ -39,14 +39,14 @@
by (rtac (major RS CollectE) 1);
by (etac exE 1);
by (eresolve_tac prems 1);
-val idE = result();
+qed "idE";
(** Composition of two relations **)
val prems = goalw Trancl.thy [comp_def]
"[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
by (fast_tac (set_cs addIs prems) 1);
-val compI = result();
+qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
val prems = goalw Trancl.thy [comp_def]
@@ -55,7 +55,7 @@
\ |] ==> P";
by (cut_facts_tac prems 1);
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
-val compE = result();
+qed "compE";
val prems = goal Trancl.thy
"[| <a,c> : r O s; \
@@ -63,7 +63,7 @@
\ |] ==> P";
by (rtac compE 1);
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1));
-val compEpair = result();
+qed "compEpair";
val comp_cs = set_cs addIs [compI,idI]
addEs [compE,idE]
@@ -73,14 +73,14 @@
"[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
by (cut_facts_tac prems 1);
by (fast_tac comp_cs 1);
-val comp_mono = result();
+qed "comp_mono";
(** The relation rtrancl **)
goal Trancl.thy "mono(%s. id Un (r O s))";
by (rtac monoI 1);
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
-val rtrancl_fun_mono = result();
+qed "rtrancl_fun_mono";
val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
@@ -88,20 +88,20 @@
goal Trancl.thy "<a,a> : r^*";
by (rtac (rtrancl_unfold RS ssubst) 1);
by (fast_tac comp_cs 1);
-val rtrancl_refl = result();
+qed "rtrancl_refl";
(*Closure under composition with r*)
val prems = goal Trancl.thy
"[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
by (rtac (rtrancl_unfold RS ssubst) 1);
by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_into_rtrancl = result();
+qed "rtrancl_into_rtrancl";
(*rtrancl of r contains r*)
val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
by (rtac prem 1);
-val r_into_rtrancl = result();
+qed "r_into_rtrancl";
(** standard induction rule **)
@@ -114,7 +114,7 @@
by (rtac (major RS (rtrancl_def RS def_induct)) 1);
by (rtac rtrancl_fun_mono 1);
by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_full_induct = result();
+qed "rtrancl_full_induct";
(*nice induction rule*)
val major::prems = goal Trancl.thy
@@ -130,14 +130,14 @@
by (resolve_tac [major RS rtrancl_full_induct] 1);
by (fast_tac (comp_cs addIs prems) 1);
by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_induct = result();
+qed "rtrancl_induct";
(*transitivity of transitive closure!! -- by induction.*)
goal Trancl.thy "trans(r^*)";
by (rtac transI 1);
by (res_inst_tac [("b","z")] rtrancl_induct 1);
by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
-val trans_rtrancl = result();
+qed "trans_rtrancl";
(*elimination of rtrancl -- by induction on a special formula*)
val major::prems = goal Trancl.thy
@@ -149,7 +149,7 @@
by (fast_tac (set_cs addIs prems) 2);
by (fast_tac (set_cs addIs prems) 2);
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
-val rtranclE = result();
+qed "rtranclE";
(**** The relation trancl ****)
@@ -160,19 +160,19 @@
"[| <a,b> : r^+ |] ==> <a,b> : r^*";
by (resolve_tac [major RS compEpair] 1);
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
-val trancl_into_rtrancl = result();
+qed "trancl_into_rtrancl";
(*r^+ contains r*)
val [prem] = goalw Trancl.thy [trancl_def]
"[| <a,b> : r |] ==> <a,b> : r^+";
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
-val r_into_trancl = result();
+qed "r_into_trancl";
(*intro rule by definition: from rtrancl and r*)
val prems = goalw Trancl.thy [trancl_def]
"[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
by (REPEAT (resolve_tac ([compI]@prems) 1));
-val rtrancl_into_trancl1 = result();
+qed "rtrancl_into_trancl1";
(*intro rule from r and rtrancl*)
val prems = goal Trancl.thy
@@ -182,7 +182,7 @@
by (resolve_tac (prems RL [r_into_trancl]) 1);
by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1);
by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
-val rtrancl_into_trancl2 = result();
+qed "rtrancl_into_trancl2";
(*elimination of r^+ -- NOT an induction rule*)
val major::prems = goal Trancl.thy
@@ -196,7 +196,7 @@
by (etac rtranclE 1);
by (fast_tac comp_cs 1);
by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1);
-val tranclE = result();
+qed "tranclE";
(*Transitivity of r^+.
Proved by unfolding since it uses transitivity of rtrancl. *)
@@ -205,11 +205,11 @@
by (REPEAT (etac compEpair 1));
by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
by (REPEAT (assume_tac 1));
-val trans_trancl = result();
+qed "trans_trancl";
val prems = goal Trancl.thy
"[| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
-val trancl_into_trancl2 = result();
+qed "trancl_into_trancl2";
--- a/src/CCL/Type.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Type.ML Wed Nov 30 13:53:46 1994 +0100
@@ -17,7 +17,7 @@
goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
by (fast_tac set_cs 1);
-val subsetXH = result();
+qed "subsetXH";
(*** Exhaustion Rules ***)
@@ -99,22 +99,22 @@
val prems = goal Type.thy
"[| a:A; P(a) |] ==> a : {x:A. P(x)}";
by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
-val SubtypeI = result();
+qed "SubtypeI";
val prems = goal Type.thy
"[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q";
by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
-val SubtypeE = result();
+qed "SubtypeE";
(*** Monotonicity ***)
goal Type.thy "mono (%X.X)";
by (REPEAT (ares_tac [monoI] 1));
-val idM = result();
+qed "idM";
goal Type.thy "mono(%X.A)";
by (REPEAT (ares_tac [monoI,subset_refl] 1));
-val constM = result();
+qed "constM";
val major::prems = goal Type.thy
"mono(%X.A(X)) ==> mono(%X.[A(X)])";
@@ -125,7 +125,7 @@
by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
by (etac (major RS monoD RS subsetD) 1);
by (assume_tac 1);
-val LiftM = result();
+qed "LiftM";
val prems = goal Type.thy
"[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
@@ -134,7 +134,7 @@
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
hyp_subst_tac 1));
-val SgM = result();
+qed "SgM";
val prems = goal Type.thy
"[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
@@ -142,7 +142,7 @@
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
hyp_subst_tac 1));
-val PiM = result();
+qed "PiM";
val prems = goal Type.thy
"[| mono(%X.A(X)); mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
@@ -150,7 +150,7 @@
eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
(resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
hyp_subst_tac 1));
-val PlusM = result();
+qed "PlusM";
(**************** RECURSIVE TYPES ******************)
@@ -158,19 +158,19 @@
goal Type.thy "mono(%X.Unit+X)";
by (REPEAT (ares_tac [PlusM,constM,idM] 1));
-val NatM = result();
-val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
+qed "NatM";
+val def_NatB = store_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
-val ListM = result();
-val def_ListB = result() RS (List_def RS def_lfp_Tarski);
-val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
+qed "ListM";
+val def_ListB = store_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
+val def_ListsB = store_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
-val IListsM = result();
-val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
+qed "IListsM";
+val def_IListsB = store_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
@@ -264,7 +264,7 @@
by (rtac (major RS (XH_to_E SgXH)) 1);
by (rtac minor 1);
by (ALLGOALS (fast_tac term_cs));
-val SgE2 = result();
+qed "SgE2";
(* General theorem proving ignores non-canonical term-formers, *)
(* - intro rules are type rules for canonical terms *)
@@ -280,7 +280,7 @@
by (rtac (lfp_lowerbound RS subset_trans) 1);
by (rtac (mono RS gfp_lemma3) 1);
by (rtac subset_refl 1);
-val lfp_subset_gfp = result();
+qed "lfp_subset_gfp";
val prems = goal Type.thy
"[| a:A; !!x X.[| x:A; ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
@@ -288,14 +288,14 @@
by (rtac coinduct 1);
by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
-val gfpI = result();
+qed "gfpI";
val rew::prem::prems = goal Type.thy
"[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
\ t(a) : C";
by (rewtac rew);
by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
-val def_gfpI = result();
+qed "def_gfpI";
(* EG *)
--- a/src/CCL/Wfd.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Wfd.ML Wed Nov 30 13:53:46 1994 +0100
@@ -20,7 +20,7 @@
\ P(a)";
by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
-val wfd_induct = result();
+qed "wfd_induct";
val [p1,p2,p3] = goal Wfd.thy
"[| !!x y.<x,y> : R ==> Q(x); \
@@ -28,7 +28,7 @@
\ !!x.Q(x) ==> x:P |] ==> a:P";
by (rtac (p2 RS spec RS mp) 1);
by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
-val wfd_strengthen_lemma = result();
+qed "wfd_strengthen_lemma";
fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
assume_tac (i+1);
@@ -38,12 +38,12 @@
by (fast_tac (FOL_cs addIs prems) 1);
by (rtac (wfd RS wfd_induct) 1);
by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
-val wf_anti_sym = result();
+qed "wf_anti_sym";
val prems = goal Wfd.thy "[| Wfd(r); <a,a>: r |] ==> P";
by (rtac wf_anti_sym 1);
by (REPEAT (resolve_tac prems 1));
-val wf_anti_refl = result();
+qed "wf_anti_refl";
(*** Irreflexive transitive closure ***)
@@ -59,24 +59,24 @@
by (fast_tac ccl_cs 1);
by (etac (spec RS mp RS spec RS mp) 1);
by (REPEAT (atac 1));
-val trancl_wf = result();
+qed "trancl_wf";
(*** Lexicographic Ordering ***)
goalw Wfd.thy [lex_def]
"p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
by (fast_tac ccl_cs 1);
-val lexXH = result();
+qed "lexXH";
val prems = goal Wfd.thy
"<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
-val lexI1 = result();
+qed "lexI1";
val prems = goal Wfd.thy
"<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
-val lexI2 = result();
+qed "lexI2";
val major::prems = goal Wfd.thy
"[| p : ra**rb; \
@@ -86,13 +86,13 @@
by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
by (ALLGOALS (fast_tac ccl_cs));
-val lexE = result();
+qed "lexE";
val [major,minor] = goal Wfd.thy
"[| p : r**s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
by (rtac (major RS lexE) 1);
by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
-val lex_pair = result();
+qed "lex_pair";
val [wfa,wfb] = goal Wfd.thy
"[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
@@ -105,26 +105,26 @@
by (rtac (wfa RS wfd_induct RS allI) 1);
by (rtac (wfb RS wfd_induct RS allI) 1);back();
by (fast_tac (type_cs addSEs [lexE]) 1);
-val lex_wf = result();
+qed "lex_wf";
(*** Mapping ***)
goalw Wfd.thy [wmap_def]
"p : wmap(f,r) <-> (EX x y. p=<x,y> & <f(x),f(y)> : r)";
by (fast_tac ccl_cs 1);
-val wmapXH = result();
+qed "wmapXH";
val prems = goal Wfd.thy
"<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
-val wmapI = result();
+qed "wmapI";
val major::prems = goal Wfd.thy
"[| p : wmap(f,r); !!a b.[| <f(a),f(b)> : r; p=<a,b> |] ==> R |] ==> R";
by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
by (ALLGOALS (fast_tac ccl_cs));
-val wmapE = result();
+qed "wmapE";
val [wf] = goal Wfd.thy
"Wfd(r) ==> Wfd(wmap(f,r))";
@@ -139,49 +139,49 @@
by (etac (spec RS mp RS spec RS mp) 1);
by (assume_tac 1);
by (rtac refl 1);
-val wmap_wf = result();
+qed "wmap_wf";
(* Projections *)
val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
by (rtac wmapI 1);
by (simp_tac (term_ss addsimps prems) 1);
-val wfstI = result();
+qed "wfstI";
val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
by (rtac wmapI 1);
by (simp_tac (term_ss addsimps prems) 1);
-val wsndI = result();
+qed "wsndI";
val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
by (rtac wmapI 1);
by (simp_tac (term_ss addsimps prems) 1);
-val wthdI = result();
+qed "wthdI";
(*** Ground well-founded relations ***)
val prems = goalw Wfd.thy [wf_def]
"[| Wfd(r); a : r |] ==> a : wf(r)";
by (fast_tac (set_cs addSIs prems) 1);
-val wfI = result();
+qed "wfI";
val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
-val Empty_wf = result();
+qed "Empty_wf";
val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
by (ALLGOALS (asm_simp_tac CCL_ss));
by (rtac Empty_wf 1);
-val wf_wf = result();
+qed "wf_wf";
goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
by (fast_tac set_cs 1);
-val NatPRXH = result();
+qed "NatPRXH";
goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
by (fast_tac set_cs 1);
-val ListPRXH = result();
+qed "ListPRXH";
val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
@@ -192,7 +192,7 @@
by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
by (etac Nat_ind 1);
by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
-val NatPR_wf = result();
+qed "NatPR_wf";
goalw Wfd.thy [Wfd_def] "Wfd(ListPR(A))";
by (safe_tac set_cs);
@@ -200,5 +200,5 @@
by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
by (etac List_ind 1);
by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
-val ListPR_wf = result();
+qed "ListPR_wf";
--- a/src/CCL/coinduction.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/coinduction.ML Wed Nov 30 13:53:46 1994 +0100
@@ -9,15 +9,15 @@
val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)";
by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
by (rtac prem 1);
-val lfpI = result();
+qed "lfpI";
val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A";
by (simp_tac (term_ss addsimps prems) 1);
-val ssubst_single = result();
+qed "ssubst_single";
val prems = goal CCL.thy "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : A";
by (simp_tac (term_ss addsimps prems) 1);
-val ssubst_pair = result();
+qed "ssubst_pair";
(***)
@@ -42,7 +42,7 @@
goal Term.thy "<a,a> : PO";
by (rtac (po_refl RS (XH_to_D PO_iff)) 1);
-val PO_refl = result();
+qed "PO_refl";
val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono)
["<true,true> : POgen(R)",
@@ -72,7 +72,7 @@
goal Term.thy "<a,a> : EQ";
by (rtac (refl RS (EQ_iff RS iffD1)) 1);
-val EQ_refl = result();
+qed "EQ_refl";
val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)
["<true,true> : EQgen(R)",
--- a/src/CCL/equalities.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/equalities.ML Wed Nov 30 13:53:46 1994 +0100
@@ -17,118 +17,118 @@
goal Set.thy "A Int A = A";
by (fast_tac eq_cs 1);
-val Int_absorb = result();
+qed "Int_absorb";
goal Set.thy "A Int B = B Int A";
by (fast_tac eq_cs 1);
-val Int_commute = result();
+qed "Int_commute";
goal Set.thy "(A Int B) Int C = A Int (B Int C)";
by (fast_tac eq_cs 1);
-val Int_assoc = result();
+qed "Int_assoc";
goal Set.thy "(A Un B) Int C = (A Int C) Un (B Int C)";
by (fast_tac eq_cs 1);
-val Int_Un_distrib = result();
+qed "Int_Un_distrib";
goal Set.thy "(A<=B) <-> (A Int B = A)";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val subset_Int_eq = result();
+qed "subset_Int_eq";
(** Binary Union **)
goal Set.thy "A Un A = A";
by (fast_tac eq_cs 1);
-val Un_absorb = result();
+qed "Un_absorb";
goal Set.thy "A Un B = B Un A";
by (fast_tac eq_cs 1);
-val Un_commute = result();
+qed "Un_commute";
goal Set.thy "(A Un B) Un C = A Un (B Un C)";
by (fast_tac eq_cs 1);
-val Un_assoc = result();
+qed "Un_assoc";
goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)";
by (fast_tac eq_cs 1);
-val Un_Int_distrib = result();
+qed "Un_Int_distrib";
goal Set.thy
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
by (fast_tac eq_cs 1);
-val Un_Int_crazy = result();
+qed "Un_Int_crazy";
goal Set.thy "(A<=B) <-> (A Un B = B)";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val subset_Un_eq = result();
+qed "subset_Un_eq";
(** Simple properties of Compl -- complement of a set **)
goal Set.thy "A Int Compl(A) = {x.False}";
by (fast_tac eq_cs 1);
-val Compl_disjoint = result();
+qed "Compl_disjoint";
goal Set.thy "A Un Compl(A) = {x.True}";
by (fast_tac eq_cs 1);
-val Compl_partition = result();
+qed "Compl_partition";
goal Set.thy "Compl(Compl(A)) = A";
by (fast_tac eq_cs 1);
-val double_complement = result();
+qed "double_complement";
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
by (fast_tac eq_cs 1);
-val Compl_Un = result();
+qed "Compl_Un";
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
by (fast_tac eq_cs 1);
-val Compl_Int = result();
+qed "Compl_Int";
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
by (fast_tac eq_cs 1);
-val Compl_UN = result();
+qed "Compl_UN";
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
by (fast_tac eq_cs 1);
-val Compl_INT = result();
+qed "Compl_INT";
(*Halmos, Naive Set Theory, page 16.*)
goal Set.thy "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val Un_Int_assoc_eq = result();
+qed "Un_Int_assoc_eq";
(** Big Union and Intersection **)
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
by (fast_tac eq_cs 1);
-val Union_Un_distrib = result();
+qed "Union_Un_distrib";
val prems = goal Set.thy
"(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val Union_disjoint = result();
+qed "Union_disjoint";
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
by (best_tac eq_cs 1);
-val Inter_Un_distrib = result();
+qed "Inter_Un_distrib";
(** Unions and Intersections of Families **)
goal Set.thy "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
by (fast_tac eq_cs 1);
-val UN_eq = result();
+qed "UN_eq";
(*Look: it has an EXISTENTIAL quantifier*)
goal Set.thy "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
by (fast_tac eq_cs 1);
-val INT_eq = result();
+qed "INT_eq";
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
by (fast_tac eq_cs 1);
-val Int_Union_image = result();
+qed "Int_Union_image";
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
by (fast_tac eq_cs 1);
-val Un_Inter_image = result();
+qed "Un_Inter_image";
--- a/src/CCL/eval.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/eval.ML Wed Nov 30 13:53:46 1994 +0100
@@ -16,7 +16,7 @@
val prems = goalw thy [apply_def]
"[| f ---> lam x.b(x); b(a) ---> c |] ==> f ` a ---> c";
by (ceval_tac prems);
-val applyV = result();
+qed "applyV";
EVal_rls := !EVal_rls @ [applyV];
@@ -25,20 +25,20 @@
by (rtac (major RS canonical) 1);
by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
etac substitute 1)));
-val letV = result();
+qed "letV";
val prems = goalw thy [fix_def]
"f(fix(f)) ---> c ==> fix(f) ---> c";
by (rtac applyV 1);
by (rtac lamV 1);
by (resolve_tac prems 1);
-val fixV = result();
+qed "fixV";
val prems = goalw thy [letrec_def]
"h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
\ letrec g x be h(x,g) in g(t) ---> c";
by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
-val letrecV = result();
+qed "letrecV";
EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
--- a/src/CCL/ex/List.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/List.ML Wed Nov 30 13:53:46 1994 +0100
@@ -34,52 +34,52 @@
val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
br (prem RS Nat_ind) 1;
by (ALLGOALS (asm_simp_tac list_ss));
-val nmapBnil = result();
+qed "nmapBnil";
val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
br (prem RS Nat_ind) 1;
by (ALLGOALS (asm_simp_tac list_ss));
-val nmapBcons = result();
+qed "nmapBcons";
(***)
val prems = goalw List.thy [map_def]
"[| !!x.x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)";
by (typechk_tac prems 1);
-val mapT = result();
+qed "mapT";
val prems = goalw List.thy [append_def]
"[| l : List(A); m : List(A) |] ==> l @ m : List(A)";
by (typechk_tac prems 1);
-val appendT = result();
+qed "appendT";
val prems = goal List.thy
"[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}";
by (cut_facts_tac prems 1);
by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1);
-val appendTS = result();
+qed "appendTS";
val prems = goalw List.thy [filter_def]
"[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)";
by (typechk_tac prems 1);
-val filterT = result();
+qed "filterT";
val prems = goalw List.thy [flat_def]
"l : List(List(A)) ==> flat(l) : List(A)";
by (typechk_tac (appendT::prems) 1);
-val flatT = result();
+qed "flatT";
val prems = goalw List.thy [insert_def]
"[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)";
by (typechk_tac prems 1);
-val insertT = result();
+qed "insertT";
val prems = goal List.thy
"[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \
\ insert(f,a,l) : {x:List(A). P(x)}";
by (cut_facts_tac prems 1);
by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1);
-val insertTS = result();
+qed "insertTS";
val prems = goalw List.thy [partition_def]
"[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
@@ -88,7 +88,7 @@
br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
by (REPEAT (atac 1));
-val partitionT = result();
+qed "partitionT";
(*** Correctness Conditions for Insertion Sort ***)
--- a/src/CCL/ex/Nat.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/Nat.ML Wed Nov 30 13:53:46 1994 +0100
@@ -27,34 +27,34 @@
val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
br (prem RS Nat_ind) 1;
by (ALLGOALS (asm_simp_tac nat_ss));
-val napply_f = result();
+qed "napply_f";
(****)
val prems = goalw Nat.thy [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat";
by (typechk_tac prems 1);
-val addT = result();
+qed "addT";
val prems = goalw Nat.thy [mult_def] "[| a:Nat; b:Nat |] ==> a #* b : Nat";
by (typechk_tac (addT::prems) 1);
-val multT = result();
+qed "multT";
(* Defined to return zero if a<b *)
val prems = goalw Nat.thy [sub_def] "[| a:Nat; b:Nat |] ==> a #- b : Nat";
by (typechk_tac (prems) 1);
by clean_ccs_tac;
be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
-val subT = result();
+qed "subT";
val prems = goalw Nat.thy [le_def] "[| a:Nat; b:Nat |] ==> a #<= b : Bool";
by (typechk_tac (prems) 1);
by clean_ccs_tac;
be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
-val leT = result();
+qed "leT";
val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat; b:Nat |] ==> a #< b : Bool";
by (typechk_tac (prems@[leT]) 1);
-val ltT = result();
+qed "ltT";
(* Correctness conditions for subtractive division **)
--- a/src/CCL/ex/Stream.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/Stream.ML Wed Nov 30 13:53:46 1994 +0100
@@ -23,7 +23,7 @@
by (EQgen_tac list_ss [] 1);
by (simp_tac list_ss 1);
by (fast_tac ccl_cs 1);
-val map_comp = result();
+qed "map_comp";
(*** Mapping the identity function leaves a list unchanged ***)
@@ -35,7 +35,7 @@
be (XH_to_E ListsXH) 1;
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
-val map_id = result();
+qed "map_id";
(*** Mapping distributes over append ***)
@@ -50,7 +50,7 @@
be (XH_to_E ListsXH) 1;
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
-val map_append = result();
+qed "map_append";
(*** Append is associative ***)
@@ -67,7 +67,7 @@
be (XH_to_E ListsXH) 1;
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
-val append_assoc = result();
+qed "append_assoc";
(*** Appending anything to an infinite list doesn't alter it ****)
@@ -78,7 +78,7 @@
be (XH_to_E IListsXH) 1;
by (EQgen_tac list_ss [] 1);
by (fast_tac ccl_cs 1);
-val ilist_append = result();
+qed "ilist_append";
(*** The equivalance of two versions of an iteration function ***)
(* *)
@@ -88,18 +88,18 @@
goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
br (letrecB RS trans) 1;
by (simp_tac term_ss 1);
-val iter1B = result();
+qed "iter1B";
goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
br (letrecB RS trans) 1;
br refl 1;
-val iter2B = result();
+qed "iter2B";
val [prem] =goal Stream.thy
"n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
br (iter2B RS ssubst) 1;back();back();
by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
-val iter2Blemma = result();
+qed "iter2Blemma";
goal Stream.thy "iter1(f,a) = iter2(f,a)";
by (eq_coinduct3_tac
@@ -111,4 +111,4 @@
by (rtac (napply_f RS ssubst) 1 THEN atac 1);
by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
by (fast_tac type_cs 1);
-val iter1_iter2_eq = result();
+qed "iter1_iter2_eq";
--- a/src/CCL/genrec.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/genrec.ML Wed Nov 30 13:53:46 1994 +0100
@@ -20,12 +20,12 @@
by (rtac ballI 1);
by (etac (spec RS mp RS mp) 1);
by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
-val letrecT = result();
+qed "letrecT";
goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
by (rtac set_ext 1);
by (fast_tac ccl_cs 1);
-val SPLITB = result();
+qed "SPLITB";
val prems = goalw Wfd.thy [letrec2_def]
"[| a : A; b : B; \
@@ -40,11 +40,11 @@
by (rtac (SPLITB RS subst) 1);
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE
eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
-val letrec2T = result();
+qed "letrec2T";
goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
-val lemma = result();
+qed "lemma";
val prems = goalw Wfd.thy [letrec3_def]
"[| a : A; b : B; c : C; \
@@ -60,7 +60,7 @@
by (rtac (lemma RS subst) 1);
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE
eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
-val letrec3T = result();
+qed "letrec3T";
val letrecTs = [letrecT,letrec2T,letrec3T];
@@ -72,14 +72,14 @@
\ g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) |] ==> \
\ g(a) : E";
by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1));
-val rcallT = result();
+qed "rcallT";
val major::prems = goal Wfd.thy
"[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \
\ g(a,b) : E";
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
-val rcall2T = result();
+qed "rcall2T";
val major::prems = goal Wfd.thy
"[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
@@ -87,7 +87,7 @@
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
\ g(a,b,c) : E";
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1));
-val rcall3T = result();
+qed "rcall3T";
val rcallTs = [rcallT,rcall2T,rcall3T];
@@ -113,7 +113,7 @@
by (resolve_tac (prems RL [sym]) 1);
by (rtac rcallT 1);
by (REPEAT (ares_tac prems 1));
-val hyprcallT = result();
+qed "hyprcallT";
val prems = goal Wfd.thy
"[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
@@ -124,7 +124,7 @@
by (resolve_tac (prems RL [sym]) 1);
by (rtac rcall2T 1);
by (REPEAT (ares_tac prems 1));
-val hyprcall2T = result();
+qed "hyprcall2T";
val prems = goal Wfd.thy
"[| g(a,b,c) = d; \
@@ -136,7 +136,7 @@
by (resolve_tac (prems RL [sym]) 1);
by (rtac rcall3T 1);
by (REPEAT (ares_tac prems 1));
-val hyprcall3T = result();
+qed "hyprcall3T";
val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T];
@@ -146,20 +146,20 @@
"[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
-val rmIH1 = result();
+qed "rmIH1";
val prems = goal Wfd.thy
"[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
-val rmIH2 = result();
+qed "rmIH2";
val prems = goal Wfd.thy
"[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ P |] ==> \
\ P";
by (REPEAT (ares_tac prems 1));
-val rmIH3 = result();
+qed "rmIH3";
val rmIHs = [rmIH1,rmIH2,rmIH3];
--- a/src/CCL/mono.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/mono.ML Wed Nov 30 13:53:46 1994 +0100
@@ -13,34 +13,34 @@
val prems = goal Set.thy "A<=B ==> Union(A) <= Union(B)";
by (cfast_tac prems 1);
-val Union_mono = result();
+qed "Union_mono";
val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)";
by (cfast_tac prems 1);
-val Inter_anti_mono = result();
+qed "Inter_anti_mono";
val prems = goal Set.thy
"[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (UN x:A. f(x)) <= (UN x:B. g(x))";
by (REPEAT (eresolve_tac [UN_E,ssubst] 1
ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1));
-val UN_mono = result();
+qed "UN_mono";
val prems = goal Set.thy
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
\ (INT x:A. f(x)) <= (INT x:A. g(x))";
by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1
ORELSE etac INT_D 1));
-val INT_anti_mono = result();
+qed "INT_anti_mono";
val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Un B <= C Un D";
by (cfast_tac prems 1);
-val Un_mono = result();
+qed "Un_mono";
val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Int B <= C Int D";
by (cfast_tac prems 1);
-val Int_mono = result();
+qed "Int_mono";
val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)";
by (cfast_tac prems 1);
-val Compl_anti_mono = result();
+qed "Compl_anti_mono";
--- a/src/CCL/subset.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/subset.ML Wed Nov 30 13:53:46 1994 +0100
@@ -15,13 +15,13 @@
val prems = goal Set.thy
"B:A ==> B <= Union(A)";
by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
-val Union_upper = result();
+qed "Union_upper";
val prems = goal Set.thy
"[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
by (REPEAT (ares_tac [subsetI] 1
ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1));
-val Union_least = result();
+qed "Union_least";
(*** Big Intersection -- greatest lower bound of a set ***)
@@ -30,70 +30,70 @@
"B:A ==> Inter(A) <= B";
by (REPEAT (resolve_tac (prems@[subsetI]) 1
ORELSE etac InterD 1));
-val Inter_lower = result();
+qed "Inter_lower";
val prems = goal Set.thy
"[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
by (REPEAT (ares_tac [subsetI,InterI] 1
ORELSE eresolve_tac (prems RL [subsetD]) 1));
-val Inter_greatest = result();
+qed "Inter_greatest";
(*** Finite Union -- the least upper bound of 2 sets ***)
goal Set.thy "A <= A Un B";
by (REPEAT (ares_tac [subsetI,UnI1] 1));
-val Un_upper1 = result();
+qed "Un_upper1";
goal Set.thy "B <= A Un B";
by (REPEAT (ares_tac [subsetI,UnI2] 1));
-val Un_upper2 = result();
+qed "Un_upper2";
val prems = goal Set.thy "[| A<=C; B<=C |] ==> A Un B <= C";
by (cut_facts_tac prems 1);
by (DEPTH_SOLVE (ares_tac [subsetI] 1
ORELSE eresolve_tac [UnE,subsetD] 1));
-val Un_least = result();
+qed "Un_least";
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
goal Set.thy "A Int B <= A";
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
-val Int_lower1 = result();
+qed "Int_lower1";
goal Set.thy "A Int B <= B";
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
-val Int_lower2 = result();
+qed "Int_lower2";
val prems = goal Set.thy "[| C<=A; C<=B |] ==> C <= A Int B";
by (cut_facts_tac prems 1);
by (REPEAT (ares_tac [subsetI,IntI] 1
ORELSE etac subsetD 1));
-val Int_greatest = result();
+qed "Int_greatest";
(*** Monotonicity ***)
val [prem] = goalw Set.thy [mono_def]
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
by (REPEAT (ares_tac [allI, impI, prem] 1));
-val monoI = result();
+qed "monoI";
val [major,minor] = goalw Set.thy [mono_def]
"[| mono(f); A <= B |] ==> f(A) <= f(B)";
by (rtac (major RS spec RS spec RS mp) 1);
by (rtac minor 1);
-val monoD = result();
+qed "monoD";
val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
by (rtac Un_least 1);
by (rtac (Un_upper1 RS (prem RS monoD)) 1);
by (rtac (Un_upper2 RS (prem RS monoD)) 1);
-val mono_Un = result();
+qed "mono_Un";
val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
by (rtac Int_greatest 1);
by (rtac (Int_lower1 RS (prem RS monoD)) 1);
by (rtac (Int_lower2 RS (prem RS monoD)) 1);
-val mono_Int = result();
+qed "mono_Int";
(****)
--- a/src/CCL/typecheck.ML Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/typecheck.ML Wed Nov 30 13:53:46 1994 +0100
@@ -46,23 +46,23 @@
by (cut_facts_tac prems 1);
by (etac (letB RS ssubst) 1);
by (assume_tac 1);
-val letT = result();
+qed "letT";
val prems = goal Type.thy
"[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)";
by (REPEAT (ares_tac (applyT::prems) 1));
-val applyT2 = result();
+qed "applyT2";
val prems = goal Type.thy
"[| a:A; a:A ==> P(a) |] ==> a : {x:A.P(x)}";
by (fast_tac (type_cs addSIs prems) 1);
-val rcall_lemma1 = result();
+qed "rcall_lemma1";
val prems = goal Type.thy
"[| a:{x:A.Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
by (cut_facts_tac prems 1);
by (fast_tac (type_cs addSIs prems) 1);
-val rcall_lemma2 = result();
+qed "rcall_lemma2";
val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2];