Transitive_Closure: added consumes and case_names attributes
authornipkow
Sat Feb 21 08:43:08 2004 +0100 (2004-02-21)
changeset 144044952c5a92e04
parent 14403 32d1526d3237
child 14405 534de3572a65
Transitive_Closure: added consumes and case_names attributes
Isar: fixed parameter name handling in simulatneous induction
which I had not done properly 2 years ago.
src/HOL/Transitive_Closure.thy
src/Provers/induct_method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 20 14:22:51 2004 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Sat Feb 21 08:43:08 2004 +0100
     1.3 @@ -70,11 +70,10 @@
     1.4    thus ?thesis by rules
     1.5  qed
     1.6  
     1.7 -ML_setup {*
     1.8 -  bind_thm ("rtrancl_induct2", split_rule
     1.9 -    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
    1.10 -*}
    1.11 -
    1.12 +lemmas rtrancl_induct2 =
    1.13 +  rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.14 +                 consumes 1, case_names refl step]
    1.15 + 
    1.16  lemma trans_rtrancl: "trans(r^*)"
    1.17    -- {* transitivity of transitive closure!! -- by induction *}
    1.18  proof (rule transI)
    1.19 @@ -165,7 +164,7 @@
    1.20  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    1.21    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
    1.22  
    1.23 -theorem converse_rtrancl_induct:
    1.24 +theorem converse_rtrancl_induct[consumes 1]:
    1.25    assumes major: "(a, b) : r^*"
    1.26      and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
    1.27    shows "P a"
    1.28 @@ -175,10 +174,9 @@
    1.29      by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
    1.30  qed
    1.31  
    1.32 -ML_setup {*
    1.33 -  bind_thm ("converse_rtrancl_induct2", split_rule
    1.34 -    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
    1.35 -*}
    1.36 +lemmas converse_rtrancl_induct2 =
    1.37 +  converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.38 +                 consumes 1, case_names refl step]
    1.39  
    1.40  lemma converse_rtranclE:
    1.41    "[| (x,z):r^*;
     2.1 --- a/src/Provers/induct_method.ML	Fri Feb 20 14:22:51 2004 +0100
     2.2 +++ b/src/Provers/induct_method.ML	Sat Feb 21 08:43:08 2004 +0100
     2.3 @@ -111,7 +111,7 @@
     2.4  
     2.5      fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
     2.6        (Method.multi_resolves (take (n, facts)) [th]);
     2.7 -  in resolveq_cases_tac (RuleCases.make (if is_open then None else Some 0) None) (Seq.flat (Seq.map prep_rule ruleq)) end;
     2.8 +  in resolveq_cases_tac (RuleCases.make is_open None) (Seq.flat (Seq.map prep_rule ruleq)) end;
     2.9  
    2.10  in
    2.11  
    2.12 @@ -225,24 +225,15 @@
    2.13  
    2.14  fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th;
    2.15  
    2.16 -fun nof_params i st =
    2.17 -  let val Bi = RuleCases.hhf_nth_subgoal (sign_of_thm st) (i,prop_of st)
    2.18 -  in length(Logic.strip_params Bi) end
    2.19 -  handle TERM("strip_prems",_) => 0 (* in case i is out of range *)
    2.20 -
    2.21  fun resolveq_cases_tac' make is_open ruleq i st =
    2.22 -  let val n = nof_params i st
    2.23 -      val mk = make (if is_open then None else Some n)
    2.24 -  in
    2.25    ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st
    2.26      |> (Method.insert_tac more_facts THEN' atomize_tac) i
    2.27      |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' =>
    2.28            st' |> Tactic.rtac rule' i
    2.29 -          |> Seq.map (rpair (mk (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
    2.30 +          |> Seq.map (rpair (make is_open (Some (Thm.prop_of rule')) (rulified_term rule') cases)))
    2.31        |> Seq.flat)
    2.32      |> Seq.flat)
    2.33 -  |> Seq.flat
    2.34 -  end;
    2.35 +  |> Seq.flat;
    2.36  
    2.37  infix 1 THEN_ALL_NEW_CASES;
    2.38  
     3.1 --- a/src/Pure/Isar/proof.ML	Fri Feb 20 14:22:51 2004 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Sat Feb 21 08:43:08 2004 +0100
     3.3 @@ -690,7 +690,7 @@
     3.4        (after_qed o map_context gen_binds, pr)))
     3.5      |> map_context (ProofContext.add_cases
     3.6       (if length props = 1 then
     3.7 -      RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
     3.8 +      RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
     3.9        else [(rule_contextN, RuleCases.empty)]))
    3.10      |> auto_bind_goal props
    3.11      |> (if is_chain state then use_facts else reset_facts)
     4.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Feb 20 14:22:51 2004 +0100
     4.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Feb 21 08:43:08 2004 +0100
     4.3 @@ -17,8 +17,7 @@
     4.4    val add: thm -> thm * (string list * int)
     4.5    type T
     4.6    val empty: T
     4.7 -  val hhf_nth_subgoal: Sign.sg -> int * term -> term
     4.8 -  val make: int option -> term option -> Sign.sg * term -> string list -> (string * T) list
     4.9 +  val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list
    4.10    val rename_params: string list list -> thm -> thm
    4.11    val params: string list list -> 'a attribute
    4.12  end;
    4.13 @@ -99,22 +98,15 @@
    4.14  
    4.15  fun nth_subgoal(i,prop) =
    4.16    hd (#1 (Logic.strip_prems (i, [], prop)));
    4.17 -
    4.18 -fun hhf_nth_subgoal sg = Drule.norm_hhf sg o nth_subgoal
    4.19    
    4.20 -(* open_params = None
    4.21 -   ==> all parameters are "open", ie their default names are used.
    4.22 -   open_params = Some k
    4.23 -   ==> only the last k parameters, the ones coming from the original
    4.24 -   goal, not from the induction rule, are "open"
    4.25 -*)
    4.26 -fun prep_case open_params split sg prop name i =
    4.27 +fun prep_case is_open split sg prop name i =
    4.28    let
    4.29 -    val Bi = hhf_nth_subgoal sg (i,prop);
    4.30 +    val Bi = Drule.norm_hhf sg (nth_subgoal(i,prop));
    4.31      val all_xs = Logic.strip_params Bi
    4.32 -    val n = length all_xs - (if_none open_params 0)
    4.33 +    val n = (case split of None => length all_xs
    4.34 +             | Some t => length (Logic.strip_params(nth_subgoal(i,t))))
    4.35      val (ind_xs, goal_xs) = splitAt(n,all_xs)
    4.36 -    val rename = if is_none open_params then I else apfst Syntax.internal
    4.37 +    val rename = if is_open then I else apfst Syntax.internal
    4.38      val xs = map rename ind_xs @ goal_xs
    4.39      val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
    4.40      val named_asms =
    4.41 @@ -127,9 +119,9 @@
    4.42      val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
    4.43    in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
    4.44  
    4.45 -fun make open_params split (sg, prop) names =
    4.46 +fun make is_open split (sg, prop) names =
    4.47    let val nprems = Logic.count_prems (prop, 0) in
    4.48 -    foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1))
    4.49 +    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
    4.50        (Library.drop (length names - nprems, names), ([], length names)) |> #1
    4.51    end;
    4.52