src/Pure/meta_simplifier.ML
changeset 28839 32d498cf7595
parent 28620 9846d772b306
child 29269 5c25a2012975
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
    77   val addSolver: simpset * solver -> simpset
    77   val addSolver: simpset * solver -> simpset
    78 
    78 
    79   val rewrite_rule: thm list -> thm -> thm
    79   val rewrite_rule: thm list -> thm -> thm
    80   val rewrite_goals_rule: thm list -> thm -> thm
    80   val rewrite_goals_rule: thm list -> thm -> thm
    81   val rewrite_goals_tac: thm list -> tactic
    81   val rewrite_goals_tac: thm list -> tactic
    82   val rewrite_tac: thm list -> tactic
       
    83   val rewrite_goal_tac: thm list -> int -> tactic
    82   val rewrite_goal_tac: thm list -> int -> tactic
    84   val rewtac: thm -> tactic
    83   val rewtac: thm -> tactic
    85   val prune_params_tac: tactic
    84   val prune_params_tac: tactic
    86   val fold_rule: thm list -> thm -> thm
    85   val fold_rule: thm list -> thm -> thm
    87   val fold_tac: thm list -> tactic
       
    88   val fold_goals_tac: thm list -> tactic
    86   val fold_goals_tac: thm list -> tactic
    89 end;
    87 end;
    90 
    88 
    91 signature META_SIMPLIFIER =
    89 signature META_SIMPLIFIER =
    92 sig
    90 sig
  1283   else raise THM ("rewrite_goal_rule", i, [thm]);
  1281   else raise THM ("rewrite_goal_rule", i, [thm]);
  1284 
  1282 
  1285 
  1283 
  1286 (** meta-rewriting tactics **)
  1284 (** meta-rewriting tactics **)
  1287 
  1285 
  1288 (*Rewrite throughout proof state. *)
  1286 (*Rewrite all subgoals*)
  1289 fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs);
       
  1290 
       
  1291 (*Rewrite subgoals only, not main goal. *)
       
  1292 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
  1287 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
  1293 fun rewtac def = rewrite_goals_tac [def];
  1288 fun rewtac def = rewrite_goals_tac [def];
  1294 
  1289 
  1295 (*Rewrite subgoal i only.*)
  1290 (*Rewrite one subgoal*)
  1296 fun asm_rewrite_goal_tac mode prover_tac ss i thm =
  1291 fun asm_rewrite_goal_tac mode prover_tac ss i thm =
  1297   if 0 < i andalso i <= Thm.nprems_of thm then
  1292   if 0 < i andalso i <= Thm.nprems_of thm then
  1298     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
  1293     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
  1299   else Seq.empty;
  1294   else Seq.empty;
  1300 
  1295 
  1327   in map (AList.find (op =) keylist) keys end;
  1322   in map (AList.find (op =) keylist) keys end;
  1328 
  1323 
  1329 val rev_defs = sort_lhs_depths o map symmetric;
  1324 val rev_defs = sort_lhs_depths o map symmetric;
  1330 
  1325 
  1331 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
  1326 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
  1332 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
       
  1333 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
  1327 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
  1334 
  1328 
  1335 
  1329 
  1336 (* HHF normal form: !! before ==>, outermost !! generalized *)
  1330 (* HHF normal form: !! before ==>, outermost !! generalized *)
  1337 
  1331