# HG changeset patch
# User wenzelm
# Date 1165363962 -3600
# Node ID f7d652ffef096408a72fefe340af8f8f705dd64c
# Parent  704510b508efe3ccced9610ed8cf9c8ff68639fc
removed legacy ML bindings;
simplified ML setup;
tuned declarations;

diff -r 704510b508ef -r f7d652ffef09 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Dec 06 01:12:41 2006 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 06 01:12:42 2006 +0100
@@ -825,6 +825,7 @@
   val sym = thm "HOL.sym"
   val thin_refl = thm "thin_refl";
 end);
+open Hypsubst;
 
 structure Classical = ClassicalFun(
 struct
@@ -836,6 +837,7 @@
 end);
 
 structure BasicClassical: BASIC_CLASSICAL = Classical; 
+open BasicClassical;
 *}
 
 setup {*
@@ -912,11 +914,13 @@
   val contr_tac = Classical.contr_tac
   val dup_intr = Classical.dup_intr
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
-  val claset	= Classical.claset
+  val claset = Classical.claset
   val rep_cs = Classical.rep_cs
   val cla_modifiers = Classical.cla_modifiers
   val cla_meth' = Classical.cla_meth'
 end);
+val Blast_tac = Blast.Blast_tac;
+val blast_tac = Blast.blast_tac;
 *}
 
 setup Blast.setup
@@ -1180,6 +1184,8 @@
   by blast
 
 use "simpdata.ML"
+ML {* open Simpdata *}
+
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
   #> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy))
@@ -1217,37 +1223,38 @@
   -- {* Miniscoping: pushing in universal quantifiers. *}
   by (iprover | blast)+
 
-declare triv_forall_equality [simp] (*prunes params*)
-  and True_implies_equals [simp] (*prune asms `True'*)
-  and if_True [simp]
-  and if_False [simp]
-  and if_cancel [simp]
-  and if_eq_cancel [simp]
-  and imp_disjL [simp]
+lemmas [simp] =
+  triv_forall_equality (*prunes params*)
+  True_implies_equals  (*prune asms `True'*)
+  if_True
+  if_False
+  if_cancel
+  if_eq_cancel
+  imp_disjL
   (*In general it seems wrong to add distributive laws by default: they
     might cause exponential blow-up.  But imp_disjL has been in for a while
     and cannot be removed without affecting existing proofs.  Moreover,
     rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
     grounds that it allows simplification of R in the two cases.*)
-  and conj_assoc [simp]
-  and disj_assoc [simp]
-  and de_Morgan_conj [simp]
-  and de_Morgan_disj [simp]
-  and imp_disj1 [simp]
-  and imp_disj2 [simp]
-  and not_imp [simp]
-  and disj_not1 [simp]
-  and not_all [simp]
-  and not_ex [simp]
-  and cases_simp [simp]
-  and the_eq_trivial [simp]
-  and the_sym_eq_trivial [simp]
-  and ex_simps [simp]
-  and all_simps [simp]
-  and simp_thms [simp]
-  and imp_cong [cong]
-  and simp_implies_cong [cong]
-  and split_if [split]
+  conj_assoc
+  disj_assoc
+  de_Morgan_conj
+  de_Morgan_disj
+  imp_disj1
+  imp_disj2
+  not_imp
+  disj_not1
+  not_all
+  not_ex
+  cases_simp
+  the_eq_trivial
+  the_sym_eq_trivial
+  ex_simps
+  all_simps
+  simp_thms
+
+lemmas [cong] = imp_cong simp_implies_cong
+lemmas [split] = split_if
 
 ML {*
 val HOL_ss = Simplifier.simpset_of (the_context ());
@@ -1399,4 +1406,78 @@
   shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
 
+
+subsection {* Basic ML bindings *}
+
+ML {*
+val FalseE = thm "FalseE"
+val Let_def = thm "Let_def"
+val TrueI = thm "TrueI";
+val allE = thm "allE";
+val allI = thm "allI";
+val all_dupE = thm "all_dupE"
+val arg_cong = thm "arg_cong";
+val box_equals = thm "box_equals"
+val ccontr = thm "ccontr";
+val classical = thm "classical";
+val conjE = thm "conjE";
+val conjI = thm "conjI";
+val conjunct1 = thm "conjunct1";
+val conjunct2 = thm "conjunct2";
+val disjCI = thm "disjCI";
+val disjE = thm "disjE";
+val disjI1 = thm "disjI1"
+val disjI2 = thm "disjI2"
+val eq_reflection = thm "eq_reflection";
+val ex1E = thm "ex1E"
+val ex1I = thm "ex1I"
+val ex1_implies_ex = thm "ex1_implies_ex"
+val exE = thm "exE";
+val exI = thm "exI";
+val excluded_middle = thm "excluded_middle"
+val ext = thm "ext"
+val fun_cong = thm "fun_cong"
+val iffD1 = thm "iffD1";
+val iffD2 = thm "iffD2";
+val iffI = thm "iffI";
+val impE = thm "impE"
+val impI = thm "impI";
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+val mp = thm "mp";
+val notE = thm "notE";
+val notI = thm "notI";
+val not_all = thm "not_all";
+val not_ex = thm "not_ex";
+val not_iff = thm "not_iff";
+val not_not = thm "not_not";
+val not_sym = thm "not_sym"
+val refl = thm "refl";
+val rev_mp = thm "rev_mp"
+val spec = thm "spec";
+val ssubst = thm "ssubst"
+val subst = thm "subst";
+val sym = thm "sym";
+val trans = thm "trans";
+*}
+
+
+subsection {* Legacy tactics *}
+
+ML {*
+fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
+
+(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+local
+  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
+    | wrong_prem (Bound _) = true
+    | wrong_prem _ = false;
+  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+  val spec = thm "spec"
+  val mp = thm "mp"
+in
+  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+end;
+*}
+
 end