--- 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])
--- 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)
--- 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
------------------------------------------------------------------------*)
--- 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")
--- 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 \<in> IT"
assume uT: "e \<turnstile> u : T"
{
- case (Var n rs)
+ case (Var n rs e_ T'_ u_ i_)
assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
let ?R = "\<lambda>t. \<forall>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\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
and "\<And>e T' u i. PROP ?Q r e T' u i T"
with uIT uT show "Abs r[u/i] \<in> IT"
by fastsimp
next
- case (Beta r a as)
+ case (Beta r a as e_ T'_ u_ i_)
assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
--- 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
--- 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)"
--- 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];
--- 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)
--- 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;