src/Pure/drule.ML
changeset 4713 bea2ab2e360b
parent 4691 b159f5d98ceb
child 4789 9cf0073bbe2b
equal deleted inserted replaced
4712:facfbbca7242 4713:bea2ab2e360b
    51   val symmetric_thm	: thm
    51   val symmetric_thm	: thm
    52   val transitive_thm	: thm
    52   val transitive_thm	: thm
    53   val refl_implies      : thm
    53   val refl_implies      : thm
    54   val symmetric_fun     : thm -> thm
    54   val symmetric_fun     : thm -> thm
    55   val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    55   val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    56   val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
    56   val rewrite_thm	: bool * bool * bool
    57 	-> meta_simpset -> thm -> thm
    57                           -> (meta_simpset -> thm -> thm option)
       
    58                           -> meta_simpset -> thm -> thm
    58   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    59   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    59   val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
    60   val rewrite_goal_rule	: bool* bool * bool
    60         -> meta_simpset -> int -> thm -> thm
    61                           -> (meta_simpset -> thm -> thm option)
    61 
    62                           -> meta_simpset -> int -> thm -> thm
    62   val equal_abs_elim	: cterm  -> thm -> thm
    63   val equal_abs_elim	: cterm  -> thm -> thm
    63   val equal_abs_elim_list: cterm list -> thm -> thm
    64   val equal_abs_elim_list: cterm list -> thm -> thm
    64   val flexpair_abs_elim_list: cterm list -> thm -> thm
    65   val flexpair_abs_elim_list: cterm list -> thm -> thm
    65   val asm_rl		: thm
    66   val asm_rl		: thm
    66   val cut_rl		: thm
    67   val cut_rl		: thm
   444 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   445 fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   445 
   446 
   446 (*Rewrite a theorem*)
   447 (*Rewrite a theorem*)
   447 fun rewrite_rule_aux _ []   th = th
   448 fun rewrite_rule_aux _ []   th = th
   448   | rewrite_rule_aux prover thms th =
   449   | rewrite_rule_aux prover thms th =
   449       fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
   450       fconv_rule (rew_conv (true,false,false) prover (Thm.mss_of thms)) th;
   450 
   451 
   451 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   452 fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
   452 
   453 
   453 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   454 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   454 fun rewrite_goals_rule_aux _ []   th = th
   455 fun rewrite_goals_rule_aux _ []   th = th
   455   | rewrite_goals_rule_aux prover thms th =
   456   | rewrite_goals_rule_aux prover thms th =
   456       fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
   457       fconv_rule (goals_conv (K true) (rew_conv (true, true, false) prover
   457         (Thm.mss_of thms))) th;
   458         (Thm.mss_of thms))) th;
   458 
   459 
   459 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   460 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   460 fun rewrite_goal_rule mode prover mss i thm =
   461 fun rewrite_goal_rule mode prover mss i thm =
   461   if 0 < i  andalso  i <= nprems_of thm
   462   if 0 < i  andalso  i <= nprems_of thm