# HG changeset patch # User nipkow # Date 1033393461 -7200 # Node ID ee5f79b210c166357c0ca8859b26bdb85040d1e9 # Parent 7e6cdcd113a246aa752cff1427905bf96a6f60c9 modified induct method diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Mon Sep 30 15:44:21 2002 +0200 @@ -424,7 +424,7 @@ subsubsection{*monotonicity of knows*} lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)" -by (cases A, (induct evs, (induct ev, auto simp: knows.simps)+)) +by(cases A, induct evs, auto simp: knows.simps split:event.split) lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)" by (auto dest: knows_sub_Cons [THEN subsetD]) diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/HOL.thy Mon Sep 30 15:44:21 2002 +0200 @@ -857,8 +857,6 @@ apply (blast intro: order_less_trans) done -declare order_less_irrefl [iff] - lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)" apply(simp add:max_def) apply(rule conjI) @@ -897,9 +895,6 @@ lemmas min_ac = min_assoc min_commute mk_left_commute[of min,OF min_assoc min_commute] -declare order_less_irrefl [iff del] -declare order_less_irrefl [simp] - lemma split_min: "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" by (simp add: min_def) diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Hyperreal/HyperNat.ML --- a/src/HOL/Hyperreal/HyperNat.ML Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Hyperreal/HyperNat.ML Mon Sep 30 15:44:21 2002 +0200 @@ -4,7 +4,11 @@ Description : Explicit construction of hypernaturals using ultrafilters *) - + +(* blast confuses different versions of < *) +DelIffs [order_less_irrefl]; +Addsimps [order_less_irrefl]; + (*------------------------------------------------------------------------ Properties of hypnatrel ------------------------------------------------------------------------*) diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/IMP/VC.thy --- a/src/HOL/IMP/VC.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/IMP/VC.thy Mon Sep 30 15:44:21 2002 +0200 @@ -110,28 +110,44 @@ apply (fast elim: awp_mono) done -lemma vc_complete: "|- {P}c{Q} ==> - (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))" -apply (erule hoare.induct) - apply (rule_tac x = "Askip" in exI) - apply (simp (no_asm)) - apply (rule_tac x = "Aass x a" in exI) - apply (simp (no_asm)) - apply clarify - apply (rule_tac x = "Asemi ac aca" in exI) - apply (simp (no_asm_simp)) - apply (fast elim!: awp_mono vc_mono) - apply clarify - apply (rule_tac x = "Aif b ac aca" in exI) - apply (simp (no_asm_simp)) - apply clarify - apply (rule_tac x = "Awhile b P ac" in exI) - apply (simp (no_asm_simp)) -apply safe -apply (rule_tac x = "ac" in exI) -apply (simp (no_asm_simp)) -apply (fast elim!: awp_mono vc_mono) -done +lemma vc_complete: assumes der: "|- {P}c{Q}" + shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))" + (is "? ac. ?Eq P c Q ac") +using der +proof induct + case skip + show ?case (is "? ac. ?C ac") + proof show "?C Askip" by simp qed +next + case (ass P a x) + show ?case (is "? ac. ?C ac") + proof show "?C(Aass x a)" by simp qed +next + case (semi P Q R c1 c2) + from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast + from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast + show ?case (is "? ac. ?C ac") + proof + show "?C(Asemi ac1 ac2)" + using ih1 ih2 by simp (fast elim!: awp_mono vc_mono) + qed +next + case (If P Q b c1 c2) + from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast + from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast + show ?case (is "? ac. ?C ac") + proof + show "?C(Aif b ac1 ac2)" + using ih1 ih2 by simp + qed +next + case (While P b c) + from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast + show ?case (is "? ac. ?C ac") + proof show "?C(Awhile b P ac)" using ih by simp qed +next + case conseq thus ?case by(fast elim!: awp_mono vc_mono) +qed lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)" apply (induct_tac "c") diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Lambda/Type.thy --- a/src/HOL/Lambda/Type.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Lambda/Type.thy Mon Sep 30 15:44:21 2002 +0200 @@ -332,7 +332,7 @@ assume uIT: "u \ IT" assume uT: "e \ u : T" { - case (Var n rs) + case (Var n rs e_ T'_ u_ i_) assume nT: "e\i:T\ \ Var n \\ rs : T'" let ?ty = "{t. \T'. e\i:T\ \ t : T'}" let ?R = "\t. \e T' u i. @@ -440,13 +440,13 @@ with False show ?thesis by (auto simp add: subst_Var) qed next - case (Lambda r) + case (Lambda r e_ T'_ u_ i_) assume "e\i:T\ \ Abs r : T'" and "\e T' u i. PROP ?Q r e T' u i T" with uIT uT show "Abs r[u/i] \ IT" by fastsimp next - case (Beta r a as) + case (Beta r a as e_ T'_ u_ i_) assume T: "e\i:T\ \ Abs r \ a \\ as : T'" assume SI1: "\e T' u i. PROP ?Q (r[a/0] \\ as) e T' u i T" assume SI2: "\e T' u i. PROP ?Q a e T' u i T" diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Library/Multiset.thy Mon Sep 30 15:44:21 2002 +0200 @@ -691,7 +691,7 @@ lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R" apply (insert mult_less_not_refl) - apply blast + apply fast done diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Nat.thy Mon Sep 30 15:44:21 2002 +0200 @@ -448,7 +448,6 @@ by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)" - -- {* @{text order_less_irrefl} could make this proof fail *} by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)" diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/SetInterval.ML --- a/src/HOL/SetInterval.ML Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/SetInterval.ML Mon Sep 30 15:44:21 2002 +0200 @@ -36,8 +36,7 @@ "!!k:: 'a::linorder. -lessThan k = atLeast k"; by Auto_tac; by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1); -by (blast_tac (claset() addIs [order_le_less_trans RS - (order_less_irrefl RS notE)]) 1); +by (blast_tac (claset() addDs [order_le_less_trans]) 1); qed "Compl_lessThan"; Goal "!!k:: 'a::order. {k} - lessThan k = {k}"; @@ -69,8 +68,7 @@ "!!k:: 'a::linorder. -greaterThan k = atMost k"; by Auto_tac; by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1); -by (blast_tac (claset() addIs [order_le_less_trans RS - (order_less_irrefl RS notE)]) 1); +by (blast_tac (claset() addDs [order_le_less_trans]) 1); qed "Compl_greaterThan"; Goal "!!k:: 'a::linorder. -atMost k = greaterThan k"; @@ -105,8 +103,7 @@ "!!k:: 'a::linorder. -atLeast k = lessThan k"; by Auto_tac; by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1); -by (blast_tac (claset() addIs [order_le_less_trans RS - (order_less_irrefl RS notE)]) 1); +by (blast_tac (claset() addDs [order_le_less_trans]) 1); qed "Compl_atLeast"; Addsimps [Compl_lessThan, Compl_atLeast]; diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Sep 27 16:44:50 2002 +0200 +++ b/src/Pure/Isar/proof.ML Mon Sep 30 15:44:21 2002 +0200 @@ -685,7 +685,7 @@ (after_qed o map_context gen_binds, pr))) |> map_context (ProofContext.add_cases (if length props = 1 then - RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] + RuleCases.make None 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 7e6cdcd113a2 -r ee5f79b210c1 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Fri Sep 27 16:44:50 2002 +0200 +++ b/src/Pure/Isar/rule_cases.ML Mon Sep 30 15:44:21 2002 +0200 @@ -17,7 +17,8 @@ val add: thm -> thm * (string list * int) type T val empty: T - val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list + val hhf_nth_subgoal: Sign.sg -> int * term -> term + val make: int option -> 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; @@ -96,24 +97,38 @@ val empty = {fixes = [], assumes = [], binds = []}; -fun prep_case is_open split sg prop name i = +fun nth_subgoal(i,prop) = + hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs 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 = let - val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop)))); - val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi); + val Bi = hhf_nth_subgoal sg (i,prop); + val all_xs = Logic.strip_params Bi + val n = length all_xs - (if_none open_params 0) + val ind_xs = take(n,all_xs) and goal_xs = drop(n,all_xs) + val rename = if is_none open_params 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 = (case split of None => [("", asms)] | Some t => - let val h = length (Logic.strip_assums_hyp - (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t))))) + let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t))) in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end); val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi); val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl)); in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end; -fun make is_open split (sg, prop) names = +fun make open_params split (sg, prop) names = let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in - foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1)) + foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1)) (Library.drop (length names - nprems, names), ([], length names)) |> #1 end;