cleaned up HOL bootstrap
authorhaftmann
Wed Oct 11 14:51:24 2006 +0200 (2006-10-11)
changeset 209730b8e436ed071
parent 20972 db0425645cc7
child 20974 2a29a21825d1
cleaned up HOL bootstrap
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/blastdata.ML
src/HOL/cladata.ML
src/HOL/hologic.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Oct 11 10:49:36 2006 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Oct 11 14:51:24 2006 +0200
     1.3 @@ -1,6 +1,24 @@
     1.4  (* legacy ML bindings *)
     1.5  
     1.6 +val HOL_cs = HOL.claset;
     1.7 +val HOL_basic_ss = HOL.simpset_basic;
     1.8 +val HOL_ss = HOL.simpset;
     1.9 +val HOL_css = (HOL.claset, HOL.simpset);
    1.10 +val hol_simplify = HOL.simplify;
    1.11 +
    1.12 +val split_tac        = Splitter.split_tac;
    1.13 +val split_inside_tac = Splitter.split_inside_tac;
    1.14 +val split_asm_tac    = Splitter.split_asm_tac;
    1.15 +val op addsplits     = Splitter.addsplits;
    1.16 +val op delsplits     = Splitter.delsplits;
    1.17 +val Addsplits        = Splitter.Addsplits;
    1.18 +val Delsplits        = Splitter.Delsplits;
    1.19 +
    1.20  open HOL;
    1.21 +val claset = Classical.claset;
    1.22 +val simpset = Simplifier.simpset;
    1.23 +val simplify = Simplifier.simplify;
    1.24 +open Clasimp;
    1.25  
    1.26  val ext = thm "ext"
    1.27  val True_def = thm "True_def"
     2.1 --- a/src/HOL/HOL.thy	Wed Oct 11 10:49:36 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Oct 11 14:51:24 2006 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4  
     2.5  subsection {* Fundamental rules *}
     2.6  
     2.7 -subsubsection {*Equality*}
     2.8 +subsubsection {* Equality *}
     2.9  
    2.10  text {* Thanks to Stephan Merz *}
    2.11  lemma subst:
    2.12 @@ -862,12 +862,11 @@
    2.13    "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
    2.14  
    2.15  use "cladata.ML"
    2.16 -ML {* val HOL_cs = HOL.cs *}
    2.17  setup Hypsubst.hypsubst_setup
    2.18  setup {* ContextRules.addSWrapper (fn tac => HOL.hyp_subst_tac' ORELSE' tac) *}
    2.19  setup Classical.setup
    2.20  setup ResAtpset.setup
    2.21 -setup {* fn thy => (Classical.change_claset_of thy (K HOL.cs); thy) *}
    2.22 +setup {* fn thy => (Classical.change_claset_of thy (K HOL.claset); thy) *}
    2.23  
    2.24  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    2.25    apply (erule swap)
    2.26 @@ -881,7 +880,7 @@
    2.27    and [elim?] = ex1_implies_ex
    2.28  
    2.29  (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
    2.30 -lemma alt_ex1E:
    2.31 +lemma alt_ex1E [elim!]:
    2.32    assumes major: "\<exists>!x. P x"
    2.33        and prem: "\<And>x. \<lbrakk> P x; \<forall>y y'. P y \<and> P y' \<longrightarrow> y = y' \<rbrakk> \<Longrightarrow> R"
    2.34    shows R
    2.35 @@ -1197,11 +1196,54 @@
    2.36  
    2.37  use "simpdata.ML"
    2.38  setup "Simplifier.method_setup Splitter.split_modifiers"
    2.39 -setup simpsetup
    2.40 +setup "(fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))"
    2.41  setup Splitter.setup
    2.42  setup Clasimp.setup
    2.43  setup EqSubst.setup
    2.44  
    2.45 +declare triv_forall_equality [simp] (*prunes params*)
    2.46 +  and True_implies_equals [simp] (*prune asms `True'*)
    2.47 +  and if_True [simp]
    2.48 +  and if_False [simp]
    2.49 +  and if_cancel [simp]
    2.50 +  and if_eq_cancel [simp]
    2.51 +  and imp_disjL [simp]
    2.52 +  (*In general it seems wrong to add distributive laws by default: they
    2.53 +    might cause exponential blow-up.  But imp_disjL has been in for a while
    2.54 +    and cannot be removed without affecting existing proofs.  Moreover,
    2.55 +    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
    2.56 +    grounds that it allows simplification of R in the two cases.*)
    2.57 +  and conj_assoc [simp]
    2.58 +  and disj_assoc [simp]
    2.59 +  and de_Morgan_conj [simp]
    2.60 +  and de_Morgan_disj [simp]
    2.61 +  and imp_disj1 [simp]
    2.62 +  and imp_disj2 [simp]
    2.63 +  and not_imp [simp]
    2.64 +  and disj_not1 [simp]
    2.65 +  and not_all [simp]
    2.66 +  and not_ex [simp]
    2.67 +  and cases_simp [simp]
    2.68 +  and the_eq_trivial [simp]
    2.69 +  and the_sym_eq_trivial [simp]
    2.70 +  and ex_simps [simp]
    2.71 +  and all_simps [simp]
    2.72 +  and simp_thms [simp]
    2.73 +  and imp_cong [cong]
    2.74 +  and simp_implies_cong [cong]
    2.75 +  and split_if [split]
    2.76 +
    2.77 +ML {*
    2.78 +structure HOL =
    2.79 +struct
    2.80 +
    2.81 +open HOL;
    2.82 +
    2.83 +val simpset = Simplifier.simpset_of (the_context ());
    2.84 +
    2.85 +end;
    2.86 +*}
    2.87 +
    2.88  text {* Simplifies x assuming c and y assuming ~c *}
    2.89  lemma if_cong:
    2.90    assumes "b = c"
     3.1 --- a/src/HOL/blastdata.ML	Wed Oct 11 10:49:36 2006 +0200
     3.2 +++ b/src/HOL/blastdata.ML	Wed Oct 11 14:51:24 2006 +0200
     3.3 @@ -1,5 +1,3 @@
     3.4 -Classical.AddSEs [thm "alt_ex1E"];
     3.5 -
     3.6  structure Blast_Data = 
     3.7  struct
     3.8    type claset = Classical.claset
     4.1 --- a/src/HOL/cladata.ML	Wed Oct 11 10:49:36 2006 +0200
     4.2 +++ b/src/HOL/cladata.ML	Wed Oct 11 14:51:24 2006 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  structure Hypsubst_Data =
     4.5  struct
     4.6    structure Simplifier = Simplifier
     4.7 -  fun dest_eq (Const ("op =", T) $ t $ u) = (t, u, domain_type T)
     4.8 +  val dest_eq = HOLogic.dest_eq_typ
     4.9    val dest_Trueprop = HOLogic.dest_Trueprop
    4.10    val dest_imp = HOLogic.dest_imp
    4.11    val eq_reflection = HOL.eq_reflection
    4.12 @@ -52,7 +52,7 @@
    4.13                         addSEs [HOL.conjE, HOL.disjE, HOL.impCE, HOL.FalseE, HOL.iffCE];
    4.14  
    4.15  (*Quantifier rules*)
    4.16 -val cs = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] 
    4.17 +val claset = prop_cs addSIs [HOL.allI, HOL.ex_ex1I] addIs [HOL.exI, HOL.the_equality] 
    4.18                       addSEs [HOL.exE] addEs [HOL.allE];
    4.19  
    4.20  end;
     5.1 --- a/src/HOL/hologic.ML	Wed Oct 11 10:49:36 2006 +0200
     5.2 +++ b/src/HOL/hologic.ML	Wed Oct 11 14:51:24 2006 +0200
     5.3 @@ -39,6 +39,7 @@
     5.4    val Collect_const: typ -> term
     5.5    val mk_eq: term * term -> term
     5.6    val dest_eq: term -> term * term
     5.7 +  val dest_eq_typ: term -> (term * term) * typ
     5.8    val mk_all: string * typ * term -> term
     5.9    val list_all: (string * typ) list * term -> term
    5.10    val mk_exists: string * typ * term -> term
    5.11 @@ -158,6 +159,9 @@
    5.12  fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
    5.13    | dest_eq t = raise TERM ("dest_eq", [t])
    5.14  
    5.15 +fun dest_eq_typ (Const ("op =", T) $ lhs $ rhs) = ((lhs, rhs), domain_type T)
    5.16 +  | dest_eq_typ t = raise TERM ("dest_eq_typ", [t])
    5.17 +
    5.18  fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    5.19  fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    5.20  fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
     6.1 --- a/src/HOL/simpdata.ML	Wed Oct 11 10:49:36 2006 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Wed Oct 11 14:51:24 2006 +0200
     6.3 @@ -6,40 +6,16 @@
     6.4  Instantiation of the generic simplifier for HOL.
     6.5  *)
     6.6  
     6.7 -(* legacy ML bindings - FIXME get rid of this *)
     6.8 -
     6.9 -val Eq_FalseI = thm "Eq_FalseI";
    6.10 -val Eq_TrueI = thm "Eq_TrueI";
    6.11 -val de_Morgan_conj = thm "de_Morgan_conj";
    6.12 -val de_Morgan_disj = thm "de_Morgan_disj";
    6.13 -val iff_conv_conj_imp = thm "iff_conv_conj_imp";
    6.14 -val imp_cong = thm "imp_cong";
    6.15 -val imp_conv_disj = thm "imp_conv_disj";
    6.16 -val imp_disj1 = thm "imp_disj1";
    6.17 -val imp_disj2 = thm "imp_disj2";
    6.18 -val imp_disjL = thm "imp_disjL";
    6.19 -val simp_impliesI = thm "simp_impliesI";
    6.20 -val simp_implies_cong = thm "simp_implies_cong";
    6.21 -val simp_implies_def = thm "simp_implies_def";
    6.22 -
    6.23 -local
    6.24 -  val uncurry = thm "uncurry"
    6.25 -  val iff_allI = thm "iff_allI"
    6.26 -  val iff_exI = thm "iff_exI"
    6.27 -  val all_comm = thm "all_comm"
    6.28 -  val ex_comm = thm "ex_comm"
    6.29 -in
    6.30 -
    6.31 -(*** make simplification procedures for quantifier elimination ***)
    6.32 +(** tools setup **)
    6.33  
    6.34  structure Quantifier1 = Quantifier1Fun
    6.35  (struct
    6.36    (*abstract syntax*)
    6.37 -  fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t)
    6.38 +  fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
    6.39      | dest_eq _ = NONE;
    6.40 -  fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t)
    6.41 +  fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
    6.42      | dest_conj _ = NONE;
    6.43 -  fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t)
    6.44 +  fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
    6.45      | dest_imp _ = NONE;
    6.46    val conj = HOLogic.conj
    6.47    val imp  = HOLogic.imp
    6.48 @@ -51,32 +27,162 @@
    6.49    val conjE= HOL.conjE
    6.50    val impI = HOL.impI
    6.51    val mp   = HOL.mp
    6.52 -  val uncurry = uncurry
    6.53 +  val uncurry = thm "uncurry"
    6.54    val exI  = HOL.exI
    6.55    val exE  = HOL.exE
    6.56 -  val iff_allI = iff_allI
    6.57 -  val iff_exI = iff_exI
    6.58 -  val all_comm = all_comm
    6.59 -  val ex_comm = ex_comm
    6.60 +  val iff_allI = thm "iff_allI"
    6.61 +  val iff_exI = thm "iff_exI"
    6.62 +  val all_comm = thm "all_comm"
    6.63 +  val ex_comm = thm "ex_comm"
    6.64  end);
    6.65  
    6.66 +structure HOL =
    6.67 +struct
    6.68 +
    6.69 +open HOL;
    6.70 +
    6.71 +val Eq_FalseI = thm "Eq_FalseI";
    6.72 +val Eq_TrueI = thm "Eq_TrueI";
    6.73 +val simp_implies_def = thm "simp_implies_def";
    6.74 +val simp_impliesI = thm "simp_impliesI";
    6.75 +
    6.76 +fun mk_meta_eq r = r RS eq_reflection;
    6.77 +fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    6.78 +
    6.79 +fun mk_eq thm = case concl_of thm
    6.80 +  (*expects Trueprop if not == *)
    6.81 +  of Const ("==",_) $ _ $ _ => thm
    6.82 +   | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm
    6.83 +   | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI
    6.84 +   | _ => thm RS Eq_TrueI;
    6.85 +
    6.86 +fun mk_eq_True r =
    6.87 +  SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
    6.88 +
    6.89 +(* Produce theorems of the form
    6.90 +  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
    6.91 +*)
    6.92 +fun lift_meta_eq_to_obj_eq i st =
    6.93 +  let
    6.94 +    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
    6.95 +      | count_imp _ = 0;
    6.96 +    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    6.97 +  in if j = 0 then meta_eq_to_obj_eq
    6.98 +    else
    6.99 +      let
   6.100 +        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   6.101 +        fun mk_simp_implies Q = foldr (fn (R, S) =>
   6.102 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
   6.103 +        val aT = TFree ("'a", HOLogic.typeS);
   6.104 +        val x = Free ("x", aT);
   6.105 +        val y = Free ("y", aT)
   6.106 +      in Goal.prove_global (Thm.theory_of_thm st) []
   6.107 +        [mk_simp_implies (Logic.mk_equals (x, y))]
   6.108 +        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   6.109 +        (fn prems => EVERY
   6.110 +         [rewrite_goals_tac [simp_implies_def],
   6.111 +          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   6.112 +      end
   6.113 +  end;
   6.114 +
   6.115 +(*Congruence rules for = (instead of ==)*)
   6.116 +fun mk_meta_cong rl = zero_var_indexes
   6.117 +  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
   6.118 +     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
   6.119 +   in mk_meta_eq rl' handle THM _ =>
   6.120 +     if can Logic.dest_equals (concl_of rl') then rl'
   6.121 +     else error "Conclusion of congruence rules must be =-equality"
   6.122 +   end);
   6.123 +
   6.124 +(*
   6.125 +val mk_atomize:      (string * thm list) list -> thm -> thm list
   6.126 +looks too specific to move it somewhere else
   6.127 +*)
   6.128 +fun mk_atomize pairs =
   6.129 +  let
   6.130 +    fun atoms thm = case concl_of thm
   6.131 +     of Const("Trueprop", _) $ p => (case head_of p
   6.132 +        of Const(a, _) => (case AList.lookup (op =) pairs a
   6.133 +           of SOME rls => maps atoms ([thm] RL rls)
   6.134 +            | NONE => [thm])
   6.135 +         | _ => [thm])
   6.136 +      | _ => [thm]
   6.137 +  in atoms end;
   6.138 +
   6.139 +fun mksimps pairs =
   6.140 +  (map_filter (try mk_eq) o mk_atomize pairs o gen_all);
   6.141 +
   6.142 +fun unsafe_solver_tac prems =
   6.143 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   6.144 +  FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE];
   6.145 +val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   6.146 +
   6.147 +(*No premature instantiation of variables during simplification*)
   6.148 +fun safe_solver_tac prems =
   6.149 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   6.150 +  FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems),
   6.151 +         eq_assume_tac, ematch_tac [FalseE]];
   6.152 +val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   6.153 +
   6.154  end;
   6.155  
   6.156 -val defEX_regroup =
   6.157 -  Simplifier.simproc (the_context ())
   6.158 -    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   6.159 +structure SplitterData =
   6.160 +struct
   6.161 +  structure Simplifier = Simplifier
   6.162 +  val mk_eq           = HOL.mk_eq
   6.163 +  val meta_eq_to_iff  = HOL.meta_eq_to_obj_eq
   6.164 +  val iffD            = HOL.iffD2
   6.165 +  val disjE           = HOL.disjE
   6.166 +  val conjE           = HOL.conjE
   6.167 +  val exE             = HOL.exE
   6.168 +  val contrapos       = HOL.contrapos_nn
   6.169 +  val contrapos2      = HOL.contrapos_pp
   6.170 +  val notnotD         = HOL.notnotD
   6.171 +end;
   6.172 +
   6.173 +structure Splitter = SplitterFun(SplitterData);
   6.174 +
   6.175 +(* integration of simplifier with classical reasoner *)
   6.176 +
   6.177 +structure Clasimp = ClasimpFun
   6.178 + (structure Simplifier = Simplifier and Splitter = Splitter
   6.179 +  and Classical  = Classical and Blast = Blast
   6.180 +  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
   6.181  
   6.182 -val defALL_regroup =
   6.183 -  Simplifier.simproc (the_context ())
   6.184 -    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   6.185 +structure HOL =
   6.186 +struct
   6.187 +
   6.188 +open HOL;
   6.189 +
   6.190 +val mksimps_pairs =
   6.191 +  [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
   6.192 +   ("All", [spec]), ("True", []), ("False", []),
   6.193 +   ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])];
   6.194  
   6.195 +val simpset_basic =
   6.196 +  Simplifier.theory_context (the_context ()) empty_ss
   6.197 +    setsubgoaler asm_simp_tac
   6.198 +    setSSolver safe_solver
   6.199 +    setSolver unsafe_solver
   6.200 +    setmksimps (mksimps mksimps_pairs)
   6.201 +    setmkeqTrue mk_eq_True
   6.202 +    setmkcong mk_meta_cong;
   6.203 +
   6.204 +fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
   6.205 +
   6.206 +fun unfold_tac ths =
   6.207 +  let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
   6.208 +  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   6.209 +
   6.210 +(** simprocs **)
   6.211  
   6.212  (* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
   6.213  
   6.214  val use_neq_simproc = ref true;
   6.215  
   6.216  local
   6.217 -  val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
   6.218 +  val thy = the_context ();
   6.219 +  val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI;
   6.220    fun neq_prover sg ss (eq $ lhs $ rhs) =
   6.221      let
   6.222        fun test thm = (case #prop (rep_thm thm) of
   6.223 @@ -91,10 +197,9 @@
   6.224      end
   6.225  in
   6.226  
   6.227 -val neq_simproc = Simplifier.simproc (the_context ())
   6.228 -  "neq_simproc" ["x = y"] neq_prover;
   6.229 +val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
   6.230  
   6.231 -end;
   6.232 +end; (*local*)
   6.233  
   6.234  
   6.235  (* Simproc for Let *)
   6.236 @@ -102,23 +207,24 @@
   6.237  val use_let_simproc = ref true;
   6.238  
   6.239  local
   6.240 +  val thy = the_context ();
   6.241    val Let_folded = thm "Let_folded";
   6.242    val Let_unfold = thm "Let_unfold";
   6.243 -  val (f_Let_unfold,x_Let_unfold) =
   6.244 +  val (f_Let_unfold, x_Let_unfold) =
   6.245        let val [(_$(f$x)$_)] = prems_of Let_unfold
   6.246 -      in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end
   6.247 -  val (f_Let_folded,x_Let_folded) =
   6.248 +      in (cterm_of thy f, cterm_of thy x) end
   6.249 +  val (f_Let_folded, x_Let_folded) =
   6.250        let val [(_$(f$x)$_)] = prems_of Let_folded
   6.251 -      in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end;
   6.252 +      in (cterm_of thy f, cterm_of thy x) end;
   6.253    val g_Let_folded =
   6.254 -      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end;
   6.255 +      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end;
   6.256  in
   6.257  
   6.258  val let_simproc =
   6.259 -  Simplifier.simproc (the_context ()) "let_simp" ["Let x f"]
   6.260 +  Simplifier.simproc thy "let_simp" ["Let x f"]
   6.261     (fn sg => fn ss => fn t =>
   6.262       let val ctxt = Simplifier.the_context ss;
   6.263 -         val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
   6.264 +         val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
   6.265       in Option.map (hd o Variable.export ctxt' ctxt o single)
   6.266        (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
   6.267           if not (!use_let_simproc) then NONE
   6.268 @@ -153,192 +259,9 @@
   6.269          | _ => NONE)
   6.270       end)
   6.271  
   6.272 -end
   6.273 -
   6.274 -(*** Case splitting ***)
   6.275 -
   6.276 -(*Make meta-equalities.  The operator below is Trueprop*)
   6.277 -
   6.278 -fun mk_meta_eq r = r RS HOL.eq_reflection;
   6.279 -fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
   6.280 -
   6.281 -fun mk_eq th = case concl_of th of
   6.282 -        Const("==",_)$_$_       => th
   6.283 -    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
   6.284 -    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
   6.285 -    |   _                       => th RS Eq_TrueI;
   6.286 -(* Expects Trueprop(.) if not == *)
   6.287 -
   6.288 -fun mk_eq_True r =
   6.289 -  SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
   6.290 -
   6.291 -(* Produce theorems of the form
   6.292 -  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
   6.293 -*)
   6.294 -fun lift_meta_eq_to_obj_eq i st =
   6.295 -  let
   6.296 -    val {sign, ...} = rep_thm st;
   6.297 -    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
   6.298 -      | count_imp _ = 0;
   6.299 -    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
   6.300 -  in if j = 0 then HOL.meta_eq_to_obj_eq
   6.301 -    else
   6.302 -      let
   6.303 -        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   6.304 -        fun mk_simp_implies Q = foldr (fn (R, S) =>
   6.305 -          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
   6.306 -        val aT = TFree ("'a", HOLogic.typeS);
   6.307 -        val x = Free ("x", aT);
   6.308 -        val y = Free ("y", aT)
   6.309 -      in Goal.prove_global (Thm.theory_of_thm st) []
   6.310 -        [mk_simp_implies (Logic.mk_equals (x, y))]
   6.311 -        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   6.312 -        (fn prems => EVERY
   6.313 -         [rewrite_goals_tac [simp_implies_def],
   6.314 -          REPEAT (ares_tac (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   6.315 -      end
   6.316 -  end;
   6.317 -
   6.318 -(*Congruence rules for = (instead of ==)*)
   6.319 -fun mk_meta_cong rl = zero_var_indexes
   6.320 -  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
   6.321 -     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
   6.322 -   in mk_meta_eq rl' handle THM _ =>
   6.323 -     if can Logic.dest_equals (concl_of rl') then rl'
   6.324 -     else error "Conclusion of congruence rules must be =-equality"
   6.325 -   end);
   6.326 -
   6.327 -structure SplitterData =
   6.328 -struct
   6.329 -  structure Simplifier = Simplifier
   6.330 -  val mk_eq          = mk_eq
   6.331 -  val meta_eq_to_iff = HOL.meta_eq_to_obj_eq
   6.332 -  val iffD           = HOL.iffD2
   6.333 -  val disjE          = HOL.disjE
   6.334 -  val conjE          = HOL.conjE
   6.335 -  val exE            = HOL.exE
   6.336 -  val contrapos      = HOL.contrapos_nn
   6.337 -  val contrapos2     = HOL.contrapos_pp
   6.338 -  val notnotD        = HOL.notnotD
   6.339 -end;
   6.340 -
   6.341 -structure Splitter = SplitterFun(SplitterData);
   6.342 -
   6.343 -val split_tac        = Splitter.split_tac;
   6.344 -val split_inside_tac = Splitter.split_inside_tac;
   6.345 -val split_asm_tac    = Splitter.split_asm_tac;
   6.346 -val op addsplits     = Splitter.addsplits;
   6.347 -val op delsplits     = Splitter.delsplits;
   6.348 -val Addsplits        = Splitter.Addsplits;
   6.349 -val Delsplits        = Splitter.Delsplits;
   6.350 -
   6.351 -val mksimps_pairs =
   6.352 -  [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
   6.353 -   ("All", [HOL.spec]), ("True", []), ("False", []),
   6.354 -   ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])];
   6.355 +end; (*local*)
   6.356  
   6.357 -(*
   6.358 -val mk_atomize:      (string * thm list) list -> thm -> thm list
   6.359 -looks too specific to move it somewhere else
   6.360 -*)
   6.361 -fun mk_atomize pairs =
   6.362 -  let fun atoms th =
   6.363 -        (case concl_of th of
   6.364 -           Const("Trueprop",_) $ p =>
   6.365 -             (case head_of p of
   6.366 -                Const(a,_) =>
   6.367 -                  (case AList.lookup (op =) pairs a of
   6.368 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
   6.369 -                   | NONE => [th])
   6.370 -              | _ => [th])
   6.371 -         | _ => [th])
   6.372 -  in atoms end;
   6.373 -
   6.374 -fun mksimps pairs =
   6.375 -  (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all);
   6.376 -
   6.377 -fun unsafe_solver_tac prems =
   6.378 -  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   6.379 -  FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE];
   6.380 -val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   6.381 -
   6.382 -(*No premature instantiation of variables during simplification*)
   6.383 -fun safe_solver_tac prems =
   6.384 -  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   6.385 -  FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems),
   6.386 -         eq_assume_tac, ematch_tac [HOL.FalseE]];
   6.387 -val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   6.388 -
   6.389 -val HOL_basic_ss =
   6.390 -  Simplifier.theory_context (the_context ()) empty_ss
   6.391 -    setsubgoaler asm_simp_tac
   6.392 -    setSSolver safe_solver
   6.393 -    setSolver unsafe_solver
   6.394 -    setmksimps (mksimps mksimps_pairs)
   6.395 -    setmkeqTrue mk_eq_True
   6.396 -    setmkcong mk_meta_cong;
   6.397 -
   6.398 -fun unfold_tac ths =
   6.399 -  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
   6.400 -  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   6.401 -
   6.402 -(*In general it seems wrong to add distributive laws by default: they
   6.403 -  might cause exponential blow-up.  But imp_disjL has been in for a while
   6.404 -  and cannot be removed without affecting existing proofs.  Moreover,
   6.405 -  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   6.406 -  grounds that it allows simplification of R in the two cases.*)
   6.407 -
   6.408 -local
   6.409 -  val ex_simps = thms "ex_simps";
   6.410 -  val all_simps = thms "all_simps";
   6.411 -  val simp_thms = thms "simp_thms";
   6.412 -  val cases_simp = thm "cases_simp";
   6.413 -  val conj_assoc = thm "conj_assoc";
   6.414 -  val if_False = thm "if_False";
   6.415 -  val if_True = thm "if_True";
   6.416 -  val disj_assoc = thm "disj_assoc";
   6.417 -  val disj_not1 = thm "disj_not1";
   6.418 -  val if_cancel = thm "if_cancel";
   6.419 -  val if_eq_cancel = thm "if_eq_cancel";
   6.420 -  val True_implies_equals = thm "True_implies_equals";
   6.421 -in
   6.422 -
   6.423 -val HOL_ss =
   6.424 -    HOL_basic_ss addsimps
   6.425 -     ([triv_forall_equality, (* prunes params *)
   6.426 -       True_implies_equals, (* prune asms `True' *)
   6.427 -       if_True, if_False, if_cancel, if_eq_cancel,
   6.428 -       imp_disjL, conj_assoc, disj_assoc,
   6.429 -       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp",
   6.430 -       disj_not1, thm "not_all", thm "not_ex", cases_simp,
   6.431 -       thm "the_eq_trivial", HOL.the_sym_eq_trivial]
   6.432 -     @ ex_simps @ all_simps @ simp_thms)
   6.433 -     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
   6.434 -     addcongs [imp_cong, simp_implies_cong]
   6.435 -     addsplits [thm "split_if"];
   6.436 -
   6.437 -end;
   6.438 -
   6.439 -fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   6.440 -
   6.441 -(* default simpset *)
   6.442 -val simpsetup =
   6.443 -  (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy));
   6.444 -
   6.445 -
   6.446 -(*** integration of simplifier with classical reasoner ***)
   6.447 -
   6.448 -structure Clasimp = ClasimpFun
   6.449 - (structure Simplifier = Simplifier and Splitter = Splitter
   6.450 -  and Classical  = Classical and Blast = Blast
   6.451 -  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
   6.452 -open Clasimp;
   6.453 -
   6.454 -val HOL_css = (HOL_cs, HOL_ss);
   6.455 -
   6.456 -
   6.457 -
   6.458 -(*** A general refutation procedure ***)
   6.459 +(* A general refutation procedure *)
   6.460  
   6.461  (* Parameters:
   6.462  
   6.463 @@ -361,7 +284,7 @@
   6.464    val nnf_simpset =
   6.465      empty_ss setmkeqTrue mk_eq_True
   6.466      setmksimps (mksimps mksimps_pairs)
   6.467 -    addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
   6.468 +    addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj",
   6.469        thm "not_all", thm "not_ex", thm "not_not"];
   6.470    fun prem_nnf_tac i st =
   6.471      full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
   6.472 @@ -369,13 +292,27 @@
   6.473  fun refute_tac test prep_tac ref_tac =
   6.474    let val refute_prems_tac =
   6.475          REPEAT_DETERM
   6.476 -              (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE
   6.477 +              (eresolve_tac [conjE, exE] 1 ORELSE
   6.478                 filter_prems_tac test 1 ORELSE
   6.479 -               etac HOL.disjE 1) THEN
   6.480 -        ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE
   6.481 +               etac disjE 1) THEN
   6.482 +        ((etac notE 1 THEN eq_assume_tac 1) ORELSE
   6.483           ref_tac 1);
   6.484    in EVERY'[TRY o filter_prems_tac test,
   6.485 -            REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac,
   6.486 +            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
   6.487              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   6.488    end;
   6.489 -end;
   6.490 +end; (*local*)
   6.491 +
   6.492 +val defALL_regroup =
   6.493 +  Simplifier.simproc (the_context ())
   6.494 +    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   6.495 +
   6.496 +val defEX_regroup =
   6.497 +  Simplifier.simproc (the_context ())
   6.498 +    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   6.499 +
   6.500 +
   6.501 +val simpset_simprocs = simpset_basic
   6.502 +  addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
   6.503 +
   6.504 +end; (*struct*)
   6.505 \ No newline at end of file