--- a/src/HOL/Hilbert_Choice.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Hilbert_Choice.thy Wed Jul 25 17:58:26 2001 +0200
@@ -29,6 +29,11 @@
someI: "P (x::'a) ==> P (SOME x. P x)"
+(*used in TFL*)
+lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
+ by (blast intro: someI)
+
+
constdefs
inv :: "('a => 'b) => ('b => 'a)"
"inv(f::'a=>'b) == % y. @x. f(x)=y"
@@ -71,6 +76,38 @@
apply (blast intro!: order_antisym)
done
+lemma wf_linord_ex_has_least:
+ "[|wf r; ALL x y. ((x,y):r^+) = ((y,x)~:r^*); P k|] \
+\ ==> EX x. P x & (!y. P y --> (m x,m y):r^*)"
+apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
+apply (drule_tac x = "m`Collect P" in spec)
+apply force
+done
+
+(* successor of obsolete nonempty_has_least *)
+lemma ex_has_least_nat:
+ "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
+apply (simp only: pred_nat_trancl_eq_le [symmetric])
+apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
+apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
+apply assumption
+done
+
+lemma LeastM_nat_lemma:
+ "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
+apply (unfold LeastM_def)
+apply (rule someI_ex)
+apply (erule ex_has_least_nat)
+done
+
+lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
+
+lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
+apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
+apply assumption
+apply assumption
+done
+
(** Greatest value operator **)
--- a/src/HOL/Hilbert_Choice_lemmas.ML Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Hilbert_Choice_lemmas.ML Wed Jul 25 17:58:26 2001 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Hilbert_Choice_lemmas
- ID: $Id$
+ ID: $Id$
Author: Lawrence C Paulson
Copyright 2001 University of Cambridge
@@ -263,3 +263,36 @@
by (Blast_tac 1);
qed "Eps_split_eq";
Addsimps [Eps_split_eq];
+
+
+(*---------------------------------------------------------------------------
+ * A relation is wellfounded iff it has no infinite descending chain
+ * Cannot go into WF because it needs type nat.
+ *---------------------------------------------------------------------------*)
+
+Goalw [wf_eq_minimal RS eq_reflection]
+ "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac contrapos_np 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+ by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac someI2_ex 1);
+ by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac someI2_ex 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
+qed "wf_iff_no_infinite_down_chain";
+
--- a/src/HOL/NatArith.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/NatArith.thy Wed Jul 25 17:58:26 2001 +0200
@@ -9,6 +9,11 @@
setup arith_setup
+lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
+apply (simp add: less_eq reflcl_trancl [THEN sym]
+ del: reflcl_trancl)
+by arith
+
(*elimination of `-' on nat*)
lemma nat_diff_split:
"P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
--- a/src/HOL/Ord.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Ord.thy Wed Jul 25 17:58:26 2001 +0200
@@ -173,6 +173,16 @@
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10)
"Least P == THE x. P x & (ALL y. P y --> x <= y)"
+lemma LeastI2:
+ "[| P (x::'a::order);
+ !!y. P y ==> x <= y;
+ !!x. [| P x; \\<forall>y. P y --> x \\<le> y |] ==> Q x |]
+ ==> Q (Least P)";
+apply (unfold Least_def)
+apply (rule theI2)
+ apply (blast intro: order_antisym)+
+done
+
lemma Least_equality:
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
apply (simp add: Least_def)
@@ -180,7 +190,6 @@
apply (auto intro!: order_antisym)
done
-
section "Linear/Total Orders"
axclass linorder < order
--- a/src/HOL/Recdef.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Recdef.thy Wed Jul 25 17:58:26 2001 +0200
@@ -17,9 +17,6 @@
("../TFL/post.ML")
("Tools/recdef_package.ML"):
-lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
- by (blast intro: someI)
-
lemma tfl_eq_True: "(x = True) --> x"
by blast
--- a/src/HOL/Wellfounded_Relations.ML Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.ML Wed Jul 25 17:58:26 2001 +0200
@@ -123,37 +123,6 @@
qed "wf_iff_acyclic_if_finite";
-(*---------------------------------------------------------------------------
- * A relation is wellfounded iff it has no infinite descending chain
- * Cannot go into WF because it needs type nat.
- *---------------------------------------------------------------------------*)
-
-Goalw [wf_eq_minimal RS eq_reflection]
- "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
-by (rtac iffI 1);
- by (rtac notI 1);
- by (etac exE 1);
- by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
- by (Blast_tac 1);
-by (etac contrapos_np 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
- by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- by (rtac allI 1);
- by (Simp_tac 1);
- by (rtac someI2_ex 1);
- by (Blast_tac 1);
- by (Blast_tac 1);
-by (rtac allI 1);
-by (induct_tac "n" 1);
- by (Asm_simp_tac 1);
-by (Simp_tac 1);
-by (rtac someI2_ex 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed "wf_iff_no_infinite_down_chain";
-
(*----------------------------------------------------------------------------
* Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
*---------------------------------------------------------------------------*)
@@ -187,17 +156,10 @@
by Auto_tac;
qed "wf_weak_decr_stable";
-(* special case: <= *)
-
-Goal "(m, n) : pred_nat^* = (m <= n)";
-by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym]
- delsimps [thm"reflcl_trancl"]) 1);
-by (arith_tac 1);
-qed "le_eq";
-
+(* special case of the theorem above: <= *)
Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
-by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1);
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
qed "weak_decr_stable";
@@ -221,37 +183,3 @@
by(Blast_tac 1);
by(blast_tac (claset() addIs prems) 1);
qed "wf_same_fst";
-
-
-
-(* ### see also LEAST and wellorderings in Wellfounded_Recursion.ML *)
-
-Goal "wf r ==> !x y. ((x,y):r^+) = ((y,x)~:r^*) ==> \
-\ P k ==> ? x. P x & (!y. P y --> (m x,m y):r^*)";
-by (dtac (wf_trancl RS (wf_eq_minimal RS iffD1)) 1);
-by (dres_inst_tac [("x","m`Collect P")] spec 1);
-by (Force_tac 1);
-qed "wf_linord_ex_has_least";
-
-(* successor of obsolete nonempty_has_least *)
-Goal "P k ==> ? x. P x & (!y. P y --> m x <= (m y::nat))";
-by (simp_tac (HOL_basic_ss addsimps [le_eq RS sym]) 1);
-by (rtac (wf_pred_nat RS wf_linord_ex_has_least) 1);
-by (simp_tac (simpset() addsimps [less_eq,not_le_iff_less,le_eq]) 1);
-by (atac 1);
-qed "ex_has_least_nat";
-
-Goalw [thm "LeastM_def"]
- "P k ==> P (LeastM m P) & (!y. P y --> m (LeastM m P) <= (m y::nat))";
-by (rtac someI_ex 1);
-by (etac ex_has_least_nat 1);
-qed "LeastM_nat_lemma";
-
-bind_thm ("LeastM_natI", LeastM_nat_lemma RS conjunct1);
-
-Goal "P x ==> m (LeastM m P) <= (m x::nat)";
-by (rtac (LeastM_nat_lemma RS conjunct2 RS spec RS mp) 1);
-by (atac 1);
-by (atac 1);
-qed "LeastM_nat_le";
-
--- a/src/HOL/Wellfounded_Relations.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Wed Jul 25 17:58:26 2001 +0200
@@ -10,7 +10,7 @@
separately.
*)
-Wellfounded_Relations = Finite + Hilbert_Choice +
+Wellfounded_Relations = Finite +
(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
instance unit :: finite (finite_unit)
--- a/src/HOL/subset.thy Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/subset.thy Wed Jul 25 17:58:26 2001 +0200
@@ -9,10 +9,23 @@
theory subset = Set
files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
-(*belongs to theory Ord*)
+(** belongs to theory Ord **)
+
theorems linorder_cases [case_names less equal greater] =
linorder_less_split
+(* Courtesy of Stephan Merz *)
+lemma Least_mono:
+"[| mono (f::'a::order => 'b::order); EX x:S. ALL y:S. x <= y |]
+ ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"
+apply clarify
+apply (erule_tac P = "%x. x : S" in LeastI2)
+apply fast
+apply (rule LeastI2)
+apply (auto elim: monoD intro!: order_antisym)
+done
+
+
(*belongs to theory Set*)
setup Rulify.setup
@@ -22,25 +35,25 @@
constdefs
type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
"type_definition Rep Abs A ==
- (\<forall>x. Rep x \<in> A) \<and>
- (\<forall>x. Abs (Rep x) = x) \<and>
- (\<forall>y \<in> A. Rep (Abs y) = y)"
+ (\\<forall>x. Rep x \\<in> A) \\<and>
+ (\\<forall>x. Abs (Rep x) = x) \\<and>
+ (\\<forall>y \\<in> A. Rep (Abs y) = y)"
-- {* This will be stated as an axiom for each typedef! *}
lemma type_definitionI [intro]:
- "(!!x. Rep x \<in> A) ==>
+ "(!!x. Rep x \\<in> A) ==>
(!!x. Abs (Rep x) = x) ==>
- (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
+ (!!y. y \\<in> A ==> Rep (Abs y) = y) ==>
type_definition Rep Abs A"
by (unfold type_definition_def) blast
-theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
+theorem Rep: "type_definition Rep Abs A ==> Rep x \\<in> A"
by (unfold type_definition_def) blast
theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
by (unfold type_definition_def) blast
-theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
+theorem Abs_inverse: "type_definition Rep Abs A ==> y \\<in> A ==> Rep (Abs y) = y"
by (unfold type_definition_def) blast
theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
@@ -58,10 +71,10 @@
qed
theorem Abs_inject:
- "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
+ "type_definition Rep Abs A ==> x \\<in> A ==> y \\<in> A ==> (Abs x = Abs y) = (x = y)"
proof -
assume tydef: "type_definition Rep Abs A"
- assume x: "x \<in> A" and y: "y \<in> A"
+ assume x: "x \\<in> A" and y: "y \\<in> A"
show ?thesis
proof
assume "Abs x = Abs y"
@@ -76,10 +89,10 @@
qed
theorem Rep_cases:
- "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
+ "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. y = Rep x ==> P) ==> P"
proof -
assume tydef: "type_definition Rep Abs A"
- assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
+ assume y: "y \\<in> A" and r: "(!!x. y = Rep x ==> P)"
show P
proof (rule r)
from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
@@ -88,33 +101,33 @@
qed
theorem Abs_cases:
- "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
+ "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \\<in> A ==> P) ==> P"
proof -
assume tydef: "type_definition Rep Abs A"
- assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
+ assume r: "!!y. x = Abs y ==> y \\<in> A ==> P"
show P
proof (rule r)
have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
thus "x = Abs (Rep x)" ..
- show "Rep x \<in> A" by (rule Rep [OF tydef])
+ show "Rep x \\<in> A" by (rule Rep [OF tydef])
qed
qed
theorem Rep_induct:
- "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
+ "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. P (Rep x)) ==> P y"
proof -
assume tydef: "type_definition Rep Abs A"
assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
- moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
+ moreover assume "y \\<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
ultimately show "P y" by (simp only:)
qed
theorem Abs_induct:
- "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
+ "type_definition Rep Abs A ==> (!!y. y \\<in> A ==> P (Abs y)) ==> P x"
proof -
assume tydef: "type_definition Rep Abs A"
- assume r: "!!y. y \<in> A ==> P (Abs y)"
- have "Rep x \<in> A" by (rule Rep [OF tydef])
+ assume r: "!!y. y \\<in> A ==> P (Abs y)"
+ have "Rep x \\<in> A" by (rule Rep [OF tydef])
hence "P (Abs (Rep x))" by (rule r)
moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
ultimately show "P x" by (simp only:)