--- 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";
*)