src/HOL/Sexp.ML
changeset 1760 6f41a494f3b1
parent 1642 21db0cf9a1a4
child 1985 84cf16192e03
     1.1 --- a/src/HOL/Sexp.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -16,19 +16,24 @@
     1.4                     Numb_neq_Scons, Numb_neq_Leaf,
     1.5                     Scons_neq_Leaf, Scons_neq_Numb];
     1.6  
     1.7 +AddSDs [Leaf_inject, Numb_inject, Scons_inject];
     1.8 +AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
     1.9 +                   Numb_neq_Scons, Numb_neq_Leaf,
    1.10 +                   Scons_neq_Leaf, Scons_neq_Numb];
    1.11 +
    1.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    1.13  by (resolve_tac [select_equality] 1);
    1.14 -by (ALLGOALS (fast_tac sexp_free_cs));
    1.15 +by (ALLGOALS (Fast_tac));
    1.16  qed "sexp_case_Leaf";
    1.17  
    1.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.19  by (resolve_tac [select_equality] 1);
    1.20 -by (ALLGOALS (fast_tac sexp_free_cs));
    1.21 +by (ALLGOALS (Fast_tac));
    1.22  qed "sexp_case_Numb";
    1.23  
    1.24  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    1.25  by (resolve_tac [select_equality] 1);
    1.26 -by (ALLGOALS (fast_tac sexp_free_cs));
    1.27 +by (ALLGOALS (Fast_tac));
    1.28  qed "sexp_case_Scons";
    1.29  
    1.30  
    1.31 @@ -46,21 +51,23 @@
    1.32  
    1.33  val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
    1.34  
    1.35 +AddIs (sexp.intrs@[SigmaI, uprodI]);
    1.36 +
    1.37  goal Sexp.thy "range(Leaf) <= sexp";
    1.38 -by (fast_tac sexp_cs 1);
    1.39 +by (Fast_tac 1);
    1.40  qed "range_Leaf_subset_sexp";
    1.41  
    1.42  val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    1.43  by (rtac (major RS setup_induction) 1);
    1.44  by (etac sexp.induct 1);
    1.45  by (ALLGOALS 
    1.46 -    (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    1.47 +    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    1.48  qed "Scons_D";
    1.49  
    1.50  (** Introduction rules for 'pred_sexp' **)
    1.51  
    1.52  goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
    1.53 -by (fast_tac sexp_cs 1);
    1.54 +by (Fast_tac 1);
    1.55  qed "pred_sexp_subset_Sigma";
    1.56  
    1.57  (* (a,b) : pred_sexp^+ ==> a : sexp *)
    1.58 @@ -71,12 +78,12 @@
    1.59  
    1.60  val prems = goalw Sexp.thy [pred_sexp_def]
    1.61      "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    1.62 -by (fast_tac (set_cs addIs prems) 1);
    1.63 +by (fast_tac (!claset addIs prems) 1);
    1.64  qed "pred_sexpI1";
    1.65  
    1.66  val prems = goalw Sexp.thy [pred_sexp_def]
    1.67      "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    1.68 -by (fast_tac (set_cs addIs prems) 1);
    1.69 +by (fast_tac (!claset addIs prems) 1);
    1.70  qed "pred_sexpI2";
    1.71  
    1.72  (*Combinations involving transitivity and the rules above*)
    1.73 @@ -102,9 +109,9 @@
    1.74  goal Sexp.thy "wf(pred_sexp)";
    1.75  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    1.76  by (etac sexp.induct 1);
    1.77 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    1.78 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    1.79 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    1.80 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    1.81 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    1.82 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    1.83  qed "wf_pred_sexp";
    1.84  
    1.85  (*** sexp_rec -- by wf recursion on pred_sexp ***)