Sexp.ML

--- a/Sexp.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Sexp.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -19,17 +19,17 @@
 goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Leaf(a)) = c(a)";
 by (resolve_tac [select_equality] 1);
 by (ALLGOALS (fast_tac sexp_free_cs));
-val sexp_case_Leaf = result();
+qed "sexp_case_Leaf";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Numb(k)) = d(k)";
 by (resolve_tac [select_equality] 1);
 by (ALLGOALS (fast_tac sexp_free_cs));
-val sexp_case_Numb = result();
+qed "sexp_case_Numb";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, M$N) = e(M,N)";
 by (resolve_tac [select_equality] 1);
 by (ALLGOALS (fast_tac sexp_free_cs));
-val sexp_case_Scons = result();
+qed "sexp_case_Scons";
 
 
 (** Introduction rules for sexp constructors **)
@@ -37,31 +37,31 @@
 val [prem] = goalw Sexp.thy [In0_def] 
     "M: sexp ==> In0(M) : sexp";
 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-val sexp_In0I = result();
+qed "sexp_In0I";
 
 val [prem] = goalw Sexp.thy [In1_def] 
     "M: sexp ==> In1(M) : sexp";
 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-val sexp_In1I = result();
+qed "sexp_In1I";
 
 val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
 
 goal Sexp.thy "range(Leaf) <= sexp";
 by (fast_tac sexp_cs 1);
-val range_Leaf_subset_sexp = result();
+qed "range_Leaf_subset_sexp";
 
 val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac sexp.induct 1);
 by (ALLGOALS 
     (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
-val Scons_D = result();
+qed "Scons_D";
 
 (** Introduction rules for 'pred_sexp' **)
 
 goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma(sexp, %u.sexp)";
 by (fast_tac sexp_cs 1);
-val pred_sexp_subset_Sigma = result();
+qed "pred_sexp_subset_Sigma";
 
 (* <a,b> : pred_sexp^+ ==> a : sexp *)
 val trancl_pred_sexpD1 = 
@@ -72,12 +72,12 @@
 val prems = goalw Sexp.thy [pred_sexp_def]
     "[| M: sexp;  N: sexp |] ==> <M, M$N> : pred_sexp";
 by (fast_tac (set_cs addIs prems) 1);
-val pred_sexpI1 = result();
+qed "pred_sexpI1";
 
 val prems = goalw Sexp.thy [pred_sexp_def]
     "[| M: sexp;  N: sexp |] ==> <N, M$N> : pred_sexp";
 by (fast_tac (set_cs addIs prems) 1);
-val pred_sexpI2 = result();
+qed "pred_sexpI2";
 
 (*Combinations involving transitivity and the rules above*)
 val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
@@ -100,7 +100,7 @@
 \    |] ==> R";
 by (cut_facts_tac [major] 1);
 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
-val pred_sexpE = result();
+qed "pred_sexpE";
 
 goal Sexp.thy "wf(pred_sexp)";
 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
@@ -108,7 +108,7 @@
 by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
 by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
 by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
-val wf_pred_sexp = result();
+qed "wf_pred_sexp";
 
 (*** sexp_rec -- by wf recursion on pred_sexp ***)
 
@@ -120,16 +120,16 @@
 goal Sexp.thy "sexp_rec(Leaf(a), c, d, h) = c(a)";
 by (stac sexp_rec_unfold 1);
 by (rtac sexp_case_Leaf 1);
-val sexp_rec_Leaf = result();
+qed "sexp_rec_Leaf";
 
 goal Sexp.thy "sexp_rec(Numb(k), c, d, h) = d(k)";
 by (stac sexp_rec_unfold 1);
 by (rtac sexp_case_Numb 1);
-val sexp_rec_Numb = result();
+qed "sexp_rec_Numb";
 
 goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
 \    sexp_rec(M$N, c, d, h) = h(M, N, sexp_rec(M,c,d,h), sexp_rec(N,c,d,h))";
 by (rtac (sexp_rec_unfold RS trans) 1);
 by (asm_simp_tac(HOL_ss addsimps
                [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
-val sexp_rec_Scons = result();
+qed "sexp_rec_Scons";