Reorganized simplifier. May now reorient rules.
authornipkow
Wed Mar 04 13:14:11 1998 +0100 (1998-03-04)
changeset 4677c4b07b8579fd
parent 4676 335dfafb1816
child 4678 78715f589655
Reorganized simplifier. May now reorient rules.
src/HOL/simpdata.ML
src/HOLCF/ex/Focus_ex.ML
src/Provers/simplifier.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 03 15:15:04 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Mar 04 13:14:11 1998 +0100
     1.3 @@ -83,13 +83,11 @@
     1.4  in
     1.5  
     1.6    fun mk_meta_eq r = r RS eq_reflection;
     1.7 +  fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True);
     1.8  
     1.9    fun mk_meta_eq_simp r = case concl_of r of
    1.10            Const("==",_)$_$_ => r
    1.11 -      |   _$(Const("op =",_)$lhs$rhs) =>
    1.12 -             (case fst(Logic.rewrite_rule_ok (#sign(rep_thm r)) (prems_of r) lhs rhs) of
    1.13 -                None => mk_meta_eq r
    1.14 -              | Some _ => r RS P_imp_P_eq_True)
    1.15 +      |   _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r
    1.16        |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    1.17        |   _ => r RS P_imp_P_eq_True;
    1.18    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    1.19 @@ -386,7 +384,8 @@
    1.20  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    1.21  			    setSSolver   safe_solver
    1.22  			    setSolver  unsafe_solver
    1.23 -			    setmksimps (mksimps mksimps_pairs);
    1.24 +			    setmksimps (mksimps mksimps_pairs)
    1.25 +			    setmkeqTrue mk_meta_eq_True;
    1.26  
    1.27  val HOL_ss = 
    1.28      HOL_basic_ss addsimps 
     2.1 --- a/src/HOLCF/ex/Focus_ex.ML	Tue Mar 03 15:15:04 1998 +0100
     2.2 +++ b/src/HOLCF/ex/Focus_ex.ML	Wed Mar 04 13:14:11 1998 +0100
     2.3 @@ -100,7 +100,6 @@
     2.4  by (rtac sym 1);
     2.5  by (rtac fix_eqI 1);
     2.6  by (asm_simp_tac HOLCF_ss 1);
     2.7 -by (etac sym 1);
     2.8  by (rtac allI 1);
     2.9  by (simp_tac HOLCF_ss 1);
    2.10  by (strip_tac 1);
     3.1 --- a/src/Provers/simplifier.ML	Tue Mar 03 15:15:04 1998 +0100
     3.2 +++ b/src/Provers/simplifier.ML	Wed Mar 04 13:14:11 1998 +0100
     3.3 @@ -8,8 +8,8 @@
     3.4  
     3.5  infix 4
     3.6    setsubgoaler setloop addloop setSSolver addSSolver setSolver
     3.7 -  addSolver setmksimps addsimps delsimps addeqcongs deleqcongs
     3.8 -  settermless addsimprocs delsimprocs;
     3.9 +  addSolver addsimps delsimps addeqcongs deleqcongs
    3.10 +  setmksimps setmkeqTrue setmksym settermless addsimprocs delsimprocs;
    3.11  
    3.12  
    3.13  signature SIMPLIFIER =
    3.14 @@ -35,6 +35,8 @@
    3.15    val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
    3.16    val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
    3.17    val setmksimps:   simpset * (thm -> thm list) -> simpset
    3.18 +  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    3.19 +  val setmksym:     simpset * (thm -> thm option) -> simpset
    3.20    val settermless:  simpset * (term * term -> bool) -> simpset
    3.21    val addsimps:     simpset * thm list -> simpset
    3.22    val delsimps:     simpset * thm list -> simpset
    3.23 @@ -111,7 +113,8 @@
    3.24      finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
    3.25  
    3.26  val empty_ss =
    3.27 -  make_ss (Thm.empty_mss, K (K no_tac), [], K (K no_tac), K (K no_tac));
    3.28 +  let val mss = Thm.set_mk_sym(Thm.empty_mss, Some o symmetric_fun)
    3.29 +  in make_ss (mss, K (K no_tac), [], K (K no_tac), K (K no_tac)) end;
    3.30  
    3.31  fun rep_ss (Simpset args) = args;
    3.32  fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
    3.33 @@ -172,6 +175,16 @@
    3.34    make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
    3.35      subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    3.36  
    3.37 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    3.38 +    setmkeqTrue mk_eq_True =
    3.39 +  make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
    3.40 +    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    3.41 +
    3.42 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    3.43 +    setmksym mksym =
    3.44 +  make_ss (Thm.set_mk_sym (mss, mksym),
    3.45 +    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    3.46 +
    3.47  fun (Simpset {mss, subgoal_tac, loop_tacs,  finish_tac, unsafe_finish_tac})
    3.48      settermless termless =
    3.49    make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,