Little reorganization. Loop tactics have names now.
authornipkow
Sat Feb 28 15:40:50 1998 +0100 (1998-02-28)
changeset 4668131989b78417
parent 4667 6328d427a339
child 4669 06f3c56dcba8
Little reorganization. Loop tactics have names now.
src/Provers/simplifier.ML
src/Provers/splitter.ML
     1.1 --- a/src/Provers/simplifier.ML	Sat Feb 28 15:40:03 1998 +0100
     1.2 +++ b/src/Provers/simplifier.ML	Sat Feb 28 15:40:50 1998 +0100
     1.3 @@ -22,14 +22,14 @@
     1.4    val rep_ss: simpset ->
     1.5     {mss: meta_simpset,
     1.6      subgoal_tac:        simpset -> int -> tactic,
     1.7 -    loop_tac:                      int -> tactic,
     1.8 +    loop_tacs:          (string * (int -> tactic))list,
     1.9             finish_tac: thm list -> int -> tactic,
    1.10      unsafe_finish_tac: thm list -> int -> tactic};
    1.11    val print_ss: simpset -> unit
    1.12    val print_simpset: theory -> unit
    1.13    val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    1.14    val setloop:      simpset *             (int -> tactic) -> simpset
    1.15 -  val addloop:      simpset *             (int -> tactic) -> simpset
    1.16 +  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    1.17    val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    1.18    val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    1.19    val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
    1.20 @@ -102,16 +102,16 @@
    1.21    Simpset of {
    1.22      mss: meta_simpset,
    1.23      subgoal_tac:        simpset -> int -> tactic,
    1.24 -    loop_tac:                      int -> tactic,
    1.25 +    loop_tacs:          (string * (int -> tactic))list,
    1.26             finish_tac: thm list -> int -> tactic,
    1.27      unsafe_finish_tac: thm list -> int -> tactic};
    1.28  
    1.29 -fun make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) =
    1.30 -  Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tac = loop_tac,
    1.31 +fun make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) =
    1.32 +  Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
    1.33      finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
    1.34  
    1.35  val empty_ss =
    1.36 -  make_ss (Thm.empty_mss, K (K no_tac), K no_tac, K (K no_tac), K (K no_tac));
    1.37 +  make_ss (Thm.empty_mss, K (K no_tac), [], K (K no_tac), K (K no_tac));
    1.38  
    1.39  fun rep_ss (Simpset args) = args;
    1.40  fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
    1.41 @@ -136,90 +136,89 @@
    1.42  
    1.43  (* extend simpsets *)
    1.44  
    1.45 -fun (Simpset {mss, subgoal_tac = _, loop_tac, finish_tac, unsafe_finish_tac})
    1.46 +fun (Simpset {mss, subgoal_tac = _, loop_tacs, finish_tac, unsafe_finish_tac})
    1.47      setsubgoaler subgoal_tac =
    1.48 -  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.49 +  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    1.50  
    1.51 -fun (Simpset {mss, subgoal_tac, loop_tac = _, finish_tac, unsafe_finish_tac})
    1.52 -    setloop loop_tac =
    1.53 -  make_ss (mss, subgoal_tac, DETERM o loop_tac, finish_tac, unsafe_finish_tac);
    1.54 +fun (Simpset {mss, subgoal_tac, loop_tacs = _, finish_tac, unsafe_finish_tac})
    1.55 +    setloop tac =
    1.56 +  make_ss (mss, subgoal_tac, [("",tac)], finish_tac, unsafe_finish_tac);
    1.57  
    1.58 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
    1.59 -    addloop tac =
    1.60 -  make_ss (mss, subgoal_tac, loop_tac ORELSE' (DETERM o tac), finish_tac, unsafe_finish_tac);
    1.61 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    1.62 +    addloop atac =
    1.63 +  make_ss (mss, subgoal_tac, overwrite(loop_tacs,atac),
    1.64 +           finish_tac, unsafe_finish_tac);
    1.65  
    1.66 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac = _, unsafe_finish_tac})
    1.67 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac = _, unsafe_finish_tac})
    1.68      setSSolver finish_tac =
    1.69 -  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.70 +  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    1.71  
    1.72 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
    1.73 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    1.74      addSSolver tac =
    1.75 -  make_ss (mss, subgoal_tac, loop_tac, fn hyps => finish_tac hyps ORELSE' tac hyps,
    1.76 +  make_ss (mss, subgoal_tac, loop_tacs, fn hyps => finish_tac hyps ORELSE' tac hyps,
    1.77      unsafe_finish_tac);
    1.78  
    1.79 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac = _})
    1.80 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac = _})
    1.81      setSolver unsafe_finish_tac =
    1.82 -  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.83 +  make_ss (mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    1.84  
    1.85 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
    1.86 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    1.87      addSolver tac =
    1.88 -  make_ss (mss, subgoal_tac, loop_tac, finish_tac,
    1.89 +  make_ss (mss, subgoal_tac, loop_tacs, finish_tac,
    1.90      fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
    1.91  
    1.92 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
    1.93 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
    1.94      setmksimps mk_simps =
    1.95    make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
    1.96 -    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.97 +    subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
    1.98  
    1.99 -fun (Simpset {mss, subgoal_tac, loop_tac,  finish_tac, unsafe_finish_tac})
   1.100 +fun (Simpset {mss, subgoal_tac, loop_tacs,  finish_tac, unsafe_finish_tac})
   1.101      settermless termless =
   1.102 -  make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tac,
   1.103 +  make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
   1.104      finish_tac, unsafe_finish_tac);
   1.105  
   1.106 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.107 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.108      addsimps rews =
   1.109 -  let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
   1.110 -    make_ss (Thm.add_simps (mss, rews'), subgoal_tac, loop_tac,
   1.111 -      finish_tac, unsafe_finish_tac)
   1.112 -  end;
   1.113 +  make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs,
   1.114 +           finish_tac, unsafe_finish_tac);
   1.115  
   1.116 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.117 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.118      delsimps rews =
   1.119 -  let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
   1.120 -    make_ss (Thm.del_simps (mss, rews'), subgoal_tac, loop_tac,
   1.121 -      finish_tac, unsafe_finish_tac)
   1.122 -  end;
   1.123 +  make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs,
   1.124 +           finish_tac, unsafe_finish_tac);
   1.125  
   1.126 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.127 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.128      addeqcongs newcongs =
   1.129 -  make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tac,
   1.130 +  make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs,
   1.131      finish_tac, unsafe_finish_tac);
   1.132  
   1.133 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.134 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.135      deleqcongs oldcongs =
   1.136 -  make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tac,
   1.137 +  make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs,
   1.138      finish_tac, unsafe_finish_tac);
   1.139  
   1.140 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.141 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.142      addsimprocs simprocs =
   1.143    make_ss
   1.144      (Thm.add_simprocs (mss, map rep_simproc simprocs),
   1.145 -      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   1.146 +      subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
   1.147  
   1.148 -fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   1.149 +fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
   1.150      delsimprocs simprocs =
   1.151    make_ss
   1.152      (Thm.del_simprocs (mss, map rep_simproc simprocs),
   1.153 -      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   1.154 +      subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
   1.155  
   1.156  
   1.157  (* merge simpsets *)	(*NOTE: ignores tactics of 2nd simpset*)
   1.158  
   1.159  fun merge_ss
   1.160 -   (Simpset {mss = mss1, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac},
   1.161 -    Simpset {mss = mss2, ...}) =
   1.162 -  make_ss (Thm.merge_mss (mss1, mss2),
   1.163 -    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   1.164 +   (Simpset {mss = mss1, loop_tacs = loop_tacs1,
   1.165 +             subgoal_tac, finish_tac, unsafe_finish_tac},
   1.166 +    Simpset {mss = mss2, loop_tacs = loop_tacs2, ...}) =
   1.167 +  make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
   1.168 +           foldl overwrite (loop_tacs1,loop_tacs2),
   1.169 +           finish_tac, unsafe_finish_tac);
   1.170  
   1.171  
   1.172  
   1.173 @@ -278,24 +277,25 @@
   1.174  
   1.175  (** simplification tactics **)
   1.176  
   1.177 -fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
   1.178 +fun solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac) mss =
   1.179    let
   1.180      val ss =
   1.181 -      make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
   1.182 +      make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, unsafe_finish_tac);
   1.183      val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   1.184    in DEPTH_SOLVE solve1_tac end;
   1.185  
   1.186 +fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   1.187  
   1.188  (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   1.189  fun basic_gen_simp_tac mode =
   1.190 -  fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
   1.191 +  fn (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) =>
   1.192      let
   1.193        fun simp_loop_tac i =
   1.194          asm_rewrite_goal_tac mode
   1.195 -          (solve_all_tac (subgoal_tac,loop_tac,finish_tac,unsafe_finish_tac))
   1.196 +          (solve_all_tac (subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac))
   1.197            mss i
   1.198          THEN (finish_tac (prems_of_mss mss) i ORELSE
   1.199 -              TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i))
   1.200 +              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   1.201      in simp_loop_tac end;
   1.202  
   1.203  fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
   1.204 @@ -321,9 +321,9 @@
   1.205  
   1.206  (** simplification meta rules **)
   1.207  
   1.208 -fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
   1.209 +fun simp mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm =
   1.210    let
   1.211 -    val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   1.212 +    val tacf = solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac);
   1.213      fun prover m th = apsome fst (Seq.pull (tacf m th));
   1.214    in
   1.215      Drule.rewrite_thm mode prover mss thm
     2.1 --- a/src/Provers/splitter.ML	Sat Feb 28 15:40:03 1998 +0100
     2.2 +++ b/src/Provers/splitter.ML	Sat Feb 28 15:40:50 1998 +0100
     2.3 @@ -18,6 +18,8 @@
     2.4  
     2.5  local
     2.6  
     2.7 +fun split_format_err() = error("Wrong format for split rule");
     2.8 +
     2.9  fun mk_case_split_tac_2 iffD order =
    2.10  let
    2.11  
    2.12 @@ -242,7 +244,6 @@
    2.13      term_lift_inst_rule (state, i, ixnTs, [((P2, T), abss (cntxt, Ts))], thm)
    2.14    end;
    2.15  
    2.16 -
    2.17  (*****************************************************************************
    2.18     The split-tactic
    2.19     
    2.20 @@ -256,8 +257,8 @@
    2.21              (case concl_of thm of _$(t as _$lhs)$_ =>
    2.22                 (case strip_comb lhs of (Const(a,_),args) =>
    2.23                    (a,(thm,fastype_of t,length args))
    2.24 -                | _ => error("Wrong format for split rule"))
    2.25 -             | _ => error("Wrong format for split rule"))
    2.26 +                | _ => split_format_err())
    2.27 +             | _ => split_format_err())
    2.28        val cmap = map const splits;
    2.29        fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
    2.30        fun lift_split_tac st = st |>
    2.31 @@ -278,6 +279,16 @@
    2.32  
    2.33  in split_tac end;
    2.34  
    2.35 +(* FIXME: this junk is only HOL specific and should therefore not go here! *)
    2.36 +(* const_of_split_thm is used in HOL/simpdata.ML *)
    2.37 +
    2.38 +fun const_of_split_thm thm =
    2.39 +  (case concl_of thm of
    2.40 +     Const("Trueprop",_) $ (Const("op =", _)$(Var _$t)$_) =>
    2.41 +        (case strip_comb t of
    2.42 +           (Const(a,_),_) => a
    2.43 +         | _              => split_format_err())
    2.44 +   | _ => split_format_err());
    2.45  
    2.46  fun mk_case_split_asm_tac split_tac 
    2.47  			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
    2.48 @@ -292,13 +303,7 @@
    2.49  
    2.50  fun split_asm_tac []     = K no_tac
    2.51    | split_asm_tac splits = 
    2.52 -  let fun const thm =
    2.53 -            (case concl_of thm of Const ("Trueprop",_)$
    2.54 -				 (Const ("op =", _)$(Var _$t)$_) =>
    2.55 -               (case strip_comb t of (Const(a,_),_) => a
    2.56 -                | _ => error("Wrong format for split rule"))
    2.57 -             | _ =>    error("Wrong format for split rule"))
    2.58 -      val cname_list = map const splits;
    2.59 +  let val cname_list = map const_of_split_thm splits;
    2.60        fun is_case (a,_) = a mem cname_list;
    2.61        fun tac (t,i) = 
    2.62  	  let val n = find_index (exists_Const is_case) 
    2.63 @@ -330,6 +335,8 @@
    2.64  
    2.65  in
    2.66  
    2.67 +val const_of_split_thm = const_of_split_thm;
    2.68 +
    2.69  fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
    2.70  
    2.71  fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);