# HG changeset patch # User nipkow # Date 1077349388 -3600 # Node ID 4952c5a92e04eb99f8810892552cfa11c31d814d # Parent 32d1526d32370846ca4bc91eb4811bc67d8fa4f2 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. diff -r 32d1526d3237 -r 4952c5a92e04 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Feb 20 14:22:51 2004 +0100 +++ b/src/HOL/Transitive_Closure.thy Sat Feb 21 08:43:08 2004 +0100 @@ -70,11 +70,10 @@ thus ?thesis by rules qed -ML_setup {* - bind_thm ("rtrancl_induct2", split_rule - (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct"))); -*} - +lemmas rtrancl_induct2 = + rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), + consumes 1, case_names refl step] + lemma trans_rtrancl: "trans(r^*)" -- {* transitivity of transitive closure!! -- by induction *} proof (rule transI) @@ -165,7 +164,7 @@ lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) -theorem converse_rtrancl_induct: +theorem converse_rtrancl_induct[consumes 1]: assumes major: "(a, b) : r^*" and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y" shows "P a" @@ -175,10 +174,9 @@ by induct (rules intro: cases dest!: converseD rtrancl_converseD)+ qed -ML_setup {* - bind_thm ("converse_rtrancl_induct2", split_rule - (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct"))); -*} +lemmas converse_rtrancl_induct2 = + converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), + consumes 1, case_names refl step] lemma converse_rtranclE: "[| (x,z):r^*; diff -r 32d1526d3237 -r 4952c5a92e04 src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Fri Feb 20 14:22:51 2004 +0100 +++ b/src/Provers/induct_method.ML Sat Feb 21 08:43:08 2004 +0100 @@ -111,7 +111,7 @@ fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases) (Method.multi_resolves (take (n, facts)) [th]); - in resolveq_cases_tac (RuleCases.make (if is_open then None else Some 0) None) (Seq.flat (Seq.map prep_rule ruleq)) end; + in resolveq_cases_tac (RuleCases.make is_open None) (Seq.flat (Seq.map prep_rule ruleq)) end; in @@ -225,24 +225,15 @@ fun internalize k th = if k > 0 then internalize (k - 1) (imp_intr k th) else th; -fun nof_params i st = - let val Bi = RuleCases.hhf_nth_subgoal (sign_of_thm st) (i,prop_of st) - in length(Logic.strip_params Bi) end - handle TERM("strip_prems",_) => 0 (* in case i is out of range *) - fun resolveq_cases_tac' make is_open ruleq i st = - let val n = nof_params i st - val mk = make (if is_open then None else Some n) - in ruleq |> Seq.map (fn (rule, (cases, k, more_facts)) => st |> (Method.insert_tac more_facts THEN' atomize_tac) i |> Seq.map (fn st' => divinate_inst (internalize k rule) i st' |> Seq.map (fn rule' => st' |> Tactic.rtac rule' i - |> Seq.map (rpair (mk (Some (Thm.prop_of rule')) (rulified_term rule') cases))) + |> Seq.map (rpair (make is_open (Some (Thm.prop_of rule')) (rulified_term rule') cases))) |> Seq.flat) |> Seq.flat) - |> Seq.flat - end; + |> Seq.flat; infix 1 THEN_ALL_NEW_CASES; diff -r 32d1526d3237 -r 4952c5a92e04 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Feb 20 14:22:51 2004 +0100 +++ b/src/Pure/Isar/proof.ML Sat Feb 21 08:43:08 2004 +0100 @@ -690,7 +690,7 @@ (after_qed o map_context gen_binds, pr))) |> map_context (ProofContext.add_cases (if length props = 1 then - RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] + RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] else [(rule_contextN, RuleCases.empty)])) |> auto_bind_goal props |> (if is_chain state then use_facts else reset_facts) diff -r 32d1526d3237 -r 4952c5a92e04 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Feb 20 14:22:51 2004 +0100 +++ b/src/Pure/Isar/rule_cases.ML Sat Feb 21 08:43:08 2004 +0100 @@ -17,8 +17,7 @@ val add: thm -> thm * (string list * int) type T val empty: T - val hhf_nth_subgoal: Sign.sg -> int * term -> term - val make: int option -> term option -> Sign.sg * term -> string list -> (string * T) list + val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list val rename_params: string list list -> thm -> thm val params: string list list -> 'a attribute end; @@ -99,22 +98,15 @@ fun nth_subgoal(i,prop) = hd (#1 (Logic.strip_prems (i, [], prop))); - -fun hhf_nth_subgoal sg = Drule.norm_hhf sg o nth_subgoal -(* open_params = None - ==> all parameters are "open", ie their default names are used. - open_params = Some k - ==> only the last k parameters, the ones coming from the original - goal, not from the induction rule, are "open" -*) -fun prep_case open_params split sg prop name i = +fun prep_case is_open split sg prop name i = let - val Bi = hhf_nth_subgoal sg (i,prop); + val Bi = Drule.norm_hhf sg (nth_subgoal(i,prop)); val all_xs = Logic.strip_params Bi - val n = length all_xs - (if_none open_params 0) + val n = (case split of None => length all_xs + | Some t => length (Logic.strip_params(nth_subgoal(i,t)))) val (ind_xs, goal_xs) = splitAt(n,all_xs) - val rename = if is_none open_params then I else apfst Syntax.internal + val rename = if is_open then I else apfst Syntax.internal val xs = map rename ind_xs @ goal_xs val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); val named_asms = @@ -127,9 +119,9 @@ val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; -fun make open_params split (sg, prop) names = +fun make is_open split (sg, prop) names = let val nprems = Logic.count_prems (prop, 0) in - foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1)) + foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1)) (Library.drop (length names - nprems, names), ([], length names)) |> #1 end;