Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
authorpaulson
Wed Jul 25 17:58:26 2001 +0200 (2001-07-25)
changeset 114547514e5e21cb8
parent 11453 1b15f655da2c
child 11455 e07927b980ec
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
src/HOL/Hilbert_Choice.thy
src/HOL/Hilbert_Choice_lemmas.ML
src/HOL/NatArith.thy
src/HOL/Ord.thy
src/HOL/Recdef.thy
src/HOL/Wellfounded_Relations.ML
src/HOL/Wellfounded_Relations.thy
src/HOL/subset.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 25 13:44:32 2001 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 25 17:58:26 2001 +0200
     1.3 @@ -29,6 +29,11 @@
     1.4    someI:        "P (x::'a) ==> P (SOME x. P x)"
     1.5  
     1.6  
     1.7 +(*used in TFL*)
     1.8 +lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
     1.9 +  by (blast intro: someI)
    1.10 +
    1.11 +
    1.12  constdefs  
    1.13    inv :: "('a => 'b) => ('b => 'a)"
    1.14      "inv(f::'a=>'b) == % y. @x. f(x)=y"
    1.15 @@ -71,6 +76,38 @@
    1.16  apply (blast intro!: order_antisym) 
    1.17  done
    1.18  
    1.19 +lemma wf_linord_ex_has_least:
    1.20 +     "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
    1.21 +\     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
    1.22 +apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    1.23 +apply (drule_tac x = "m`Collect P" in spec)
    1.24 +apply force
    1.25 +done
    1.26 +
    1.27 +(* successor of obsolete nonempty_has_least *)
    1.28 +lemma ex_has_least_nat:
    1.29 +     "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
    1.30 +apply (simp only: pred_nat_trancl_eq_le [symmetric])
    1.31 +apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    1.32 +apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
    1.33 +apply assumption
    1.34 +done
    1.35 +
    1.36 +lemma LeastM_nat_lemma: 
    1.37 +  "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
    1.38 +apply (unfold LeastM_def)
    1.39 +apply (rule someI_ex)
    1.40 +apply (erule ex_has_least_nat)
    1.41 +done
    1.42 +
    1.43 +lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
    1.44 +
    1.45 +lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
    1.46 +apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
    1.47 +apply assumption
    1.48 +apply assumption
    1.49 +done
    1.50 +
    1.51  
    1.52  (** Greatest value operator **)
    1.53  
     2.1 --- a/src/HOL/Hilbert_Choice_lemmas.ML	Wed Jul 25 13:44:32 2001 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice_lemmas.ML	Wed Jul 25 17:58:26 2001 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  (*  Title:      HOL/Hilbert_Choice_lemmas
     2.5 -    ID:         $Id$
     2.6 +    ID: $Id$
     2.7      Author:     Lawrence C Paulson
     2.8      Copyright   2001  University of Cambridge
     2.9  
    2.10 @@ -263,3 +263,36 @@
    2.11  by (Blast_tac 1);
    2.12  qed "Eps_split_eq";
    2.13  Addsimps [Eps_split_eq];
    2.14 +
    2.15 +
    2.16 +(*---------------------------------------------------------------------------
    2.17 + * A relation is wellfounded iff it has no infinite descending chain
    2.18 + * Cannot go into WF because it needs type nat.
    2.19 + *---------------------------------------------------------------------------*)
    2.20 +
    2.21 +Goalw [wf_eq_minimal RS eq_reflection]
    2.22 +  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
    2.23 +by (rtac iffI 1);
    2.24 + by (rtac notI 1);
    2.25 + by (etac exE 1);
    2.26 + by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
    2.27 + by (Blast_tac 1);
    2.28 +by (etac contrapos_np 1);
    2.29 +by (Asm_full_simp_tac 1);
    2.30 +by (Clarify_tac 1);
    2.31 +by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
    2.32 + by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
    2.33 + by (rtac allI 1);
    2.34 + by (Simp_tac 1);
    2.35 + by (rtac someI2_ex 1);
    2.36 +  by (Blast_tac 1);
    2.37 + by (Blast_tac 1);
    2.38 +by (rtac allI 1);
    2.39 +by (induct_tac "n" 1);
    2.40 + by (Asm_simp_tac 1);
    2.41 +by (Simp_tac 1);
    2.42 +by (rtac someI2_ex 1);
    2.43 + by (Blast_tac 1);
    2.44 +by (Blast_tac 1);
    2.45 +qed "wf_iff_no_infinite_down_chain";
    2.46 +
     3.1 --- a/src/HOL/NatArith.thy	Wed Jul 25 13:44:32 2001 +0200
     3.2 +++ b/src/HOL/NatArith.thy	Wed Jul 25 17:58:26 2001 +0200
     3.3 @@ -9,6 +9,11 @@
     3.4  
     3.5  setup arith_setup
     3.6  
     3.7 +lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
     3.8 +apply (simp add: less_eq reflcl_trancl [THEN sym] 
     3.9 +            del: reflcl_trancl)
    3.10 +by arith
    3.11 +
    3.12  (*elimination of `-' on nat*)
    3.13  lemma nat_diff_split:
    3.14      "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
     4.1 --- a/src/HOL/Ord.thy	Wed Jul 25 13:44:32 2001 +0200
     4.2 +++ b/src/HOL/Ord.thy	Wed Jul 25 17:58:26 2001 +0200
     4.3 @@ -173,6 +173,16 @@
     4.4    Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
     4.5      "Least P == THE x. P x & (ALL y. P y --> x <= y)"
     4.6  
     4.7 +lemma LeastI2:
     4.8 +  "[| P (x::'a::order); 
     4.9 +      !!y. P y ==> x <= y;
    4.10 +      !!x. [| P x; \\<forall>y. P y --> x \\<le> y |] ==> Q x |]
    4.11 +   ==> Q (Least P)";
    4.12 +apply (unfold Least_def)
    4.13 +apply (rule theI2)
    4.14 +  apply (blast intro: order_antisym)+
    4.15 +done
    4.16 +
    4.17  lemma Least_equality:
    4.18    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
    4.19  apply (simp add: Least_def)
    4.20 @@ -180,7 +190,6 @@
    4.21  apply (auto intro!: order_antisym) 
    4.22  done
    4.23  
    4.24 -
    4.25  section "Linear/Total Orders"
    4.26  
    4.27  axclass linorder < order
     5.1 --- a/src/HOL/Recdef.thy	Wed Jul 25 13:44:32 2001 +0200
     5.2 +++ b/src/HOL/Recdef.thy	Wed Jul 25 17:58:26 2001 +0200
     5.3 @@ -17,9 +17,6 @@
     5.4    ("../TFL/post.ML")
     5.5    ("Tools/recdef_package.ML"):
     5.6  
     5.7 -lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
     5.8 -  by (blast intro: someI)
     5.9 -
    5.10  lemma tfl_eq_True: "(x = True) --> x"
    5.11    by blast
    5.12  
     6.1 --- a/src/HOL/Wellfounded_Relations.ML	Wed Jul 25 13:44:32 2001 +0200
     6.2 +++ b/src/HOL/Wellfounded_Relations.ML	Wed Jul 25 17:58:26 2001 +0200
     6.3 @@ -123,37 +123,6 @@
     6.4  qed "wf_iff_acyclic_if_finite";
     6.5  
     6.6  
     6.7 -(*---------------------------------------------------------------------------
     6.8 - * A relation is wellfounded iff it has no infinite descending chain
     6.9 - * Cannot go into WF because it needs type nat.
    6.10 - *---------------------------------------------------------------------------*)
    6.11 -
    6.12 -Goalw [wf_eq_minimal RS eq_reflection]
    6.13 -  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
    6.14 -by (rtac iffI 1);
    6.15 - by (rtac notI 1);
    6.16 - by (etac exE 1);
    6.17 - by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
    6.18 - by (Blast_tac 1);
    6.19 -by (etac contrapos_np 1);
    6.20 -by (Asm_full_simp_tac 1);
    6.21 -by (Clarify_tac 1);
    6.22 -by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
    6.23 - by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
    6.24 - by (rtac allI 1);
    6.25 - by (Simp_tac 1);
    6.26 - by (rtac someI2_ex 1);
    6.27 -  by (Blast_tac 1);
    6.28 - by (Blast_tac 1);
    6.29 -by (rtac allI 1);
    6.30 -by (induct_tac "n" 1);
    6.31 - by (Asm_simp_tac 1);
    6.32 -by (Simp_tac 1);
    6.33 -by (rtac someI2_ex 1);
    6.34 - by (Blast_tac 1);
    6.35 -by (Blast_tac 1);
    6.36 -qed "wf_iff_no_infinite_down_chain";
    6.37 -
    6.38  (*----------------------------------------------------------------------------
    6.39   * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
    6.40   *---------------------------------------------------------------------------*)
    6.41 @@ -187,17 +156,10 @@
    6.42  by Auto_tac;
    6.43  qed "wf_weak_decr_stable";
    6.44  
    6.45 -(* special case: <= *)
    6.46 -
    6.47 -Goal "(m, n) : pred_nat^* = (m <= n)";
    6.48 -by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym] 
    6.49 -                        delsimps [thm"reflcl_trancl"]) 1);
    6.50 -by (arith_tac 1);
    6.51 -qed "le_eq";
    6.52 -
    6.53 +(* special case of the theorem above: <= *)
    6.54  Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
    6.55  by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
    6.56 -by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
    6.57 +by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1);
    6.58  by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
    6.59  qed "weak_decr_stable";
    6.60  
    6.61 @@ -221,37 +183,3 @@
    6.62   by(Blast_tac 1);
    6.63  by(blast_tac (claset() addIs prems) 1);
    6.64  qed "wf_same_fst";
    6.65 -
    6.66 -
    6.67 -
    6.68 -(* ### see also LEAST and wellorderings in Wellfounded_Recursion.ML *)
    6.69 -
    6.70 -Goal "wf r ==> !x y. ((x,y):r^+) = ((y,x)~:r^*) ==> \
    6.71 -\ P k ==> ? x. P x & (!y. P y --> (m x,m y):r^*)";
    6.72 -by (dtac (wf_trancl RS (wf_eq_minimal RS iffD1)) 1);
    6.73 -by (dres_inst_tac [("x","m`Collect P")] spec 1);
    6.74 -by (Force_tac 1);
    6.75 -qed "wf_linord_ex_has_least";
    6.76 -
    6.77 -(* successor of obsolete nonempty_has_least *)
    6.78 -Goal "P k ==> ? x. P x & (!y. P y --> m x <= (m y::nat))";
    6.79 -by (simp_tac (HOL_basic_ss addsimps [le_eq RS sym]) 1);
    6.80 -by (rtac (wf_pred_nat RS wf_linord_ex_has_least) 1);
    6.81 -by (simp_tac (simpset() addsimps [less_eq,not_le_iff_less,le_eq]) 1);
    6.82 -by (atac 1);
    6.83 -qed "ex_has_least_nat";
    6.84 -
    6.85 -Goalw [thm "LeastM_def"] 
    6.86 -  "P k ==> P (LeastM m P) & (!y. P y --> m (LeastM m P) <= (m y::nat))";
    6.87 -by (rtac someI_ex 1);
    6.88 -by (etac ex_has_least_nat 1);
    6.89 -qed "LeastM_nat_lemma";
    6.90 -
    6.91 -bind_thm ("LeastM_natI", LeastM_nat_lemma RS conjunct1);
    6.92 -
    6.93 -Goal "P x ==> m (LeastM m P) <= (m x::nat)";
    6.94 -by (rtac (LeastM_nat_lemma RS conjunct2 RS spec RS mp) 1);
    6.95 -by (atac 1);
    6.96 -by (atac 1);
    6.97 -qed "LeastM_nat_le";
    6.98 -
     7.1 --- a/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:44:32 2001 +0200
     7.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 17:58:26 2001 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  separately.
     7.5  *)
     7.6  
     7.7 -Wellfounded_Relations = Finite + Hilbert_Choice + 
     7.8 +Wellfounded_Relations = Finite + 
     7.9  
    7.10  (* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
    7.11  instance unit :: finite                  (finite_unit)
     8.1 --- a/src/HOL/subset.thy	Wed Jul 25 13:44:32 2001 +0200
     8.2 +++ b/src/HOL/subset.thy	Wed Jul 25 17:58:26 2001 +0200
     8.3 @@ -9,10 +9,23 @@
     8.4  theory subset = Set
     8.5  files "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
     8.6  
     8.7 -(*belongs to theory Ord*)
     8.8 +(** belongs to theory Ord **)
     8.9 +  
    8.10  theorems linorder_cases [case_names less equal greater] =
    8.11    linorder_less_split
    8.12  
    8.13 +(* Courtesy of Stephan Merz *)
    8.14 +lemma Least_mono: 
    8.15 +"[| mono (f::'a::order => 'b::order); EX x:S. ALL y:S. x <= y |]  
    8.16 +   ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"
    8.17 +apply clarify
    8.18 +apply (erule_tac P = "%x. x : S" in LeastI2)
    8.19 +apply  fast
    8.20 +apply (rule LeastI2)
    8.21 +apply (auto elim: monoD intro!: order_antisym)
    8.22 +done
    8.23 +
    8.24 +
    8.25  (*belongs to theory Set*)
    8.26  setup Rulify.setup
    8.27  
    8.28 @@ -22,25 +35,25 @@
    8.29  constdefs
    8.30    type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    8.31    "type_definition Rep Abs A ==
    8.32 -    (\<forall>x. Rep x \<in> A) \<and>
    8.33 -    (\<forall>x. Abs (Rep x) = x) \<and>
    8.34 -    (\<forall>y \<in> A. Rep (Abs y) = y)"
    8.35 +    (\\<forall>x. Rep x \\<in> A) \\<and>
    8.36 +    (\\<forall>x. Abs (Rep x) = x) \\<and>
    8.37 +    (\\<forall>y \\<in> A. Rep (Abs y) = y)"
    8.38    -- {* This will be stated as an axiom for each typedef! *}
    8.39  
    8.40  lemma type_definitionI [intro]:
    8.41 -  "(!!x. Rep x \<in> A) ==>
    8.42 +  "(!!x. Rep x \\<in> A) ==>
    8.43      (!!x. Abs (Rep x) = x) ==>
    8.44 -    (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    8.45 +    (!!y. y \\<in> A ==> Rep (Abs y) = y) ==>
    8.46      type_definition Rep Abs A"
    8.47    by (unfold type_definition_def) blast
    8.48  
    8.49 -theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    8.50 +theorem Rep: "type_definition Rep Abs A ==> Rep x \\<in> A"
    8.51    by (unfold type_definition_def) blast
    8.52  
    8.53  theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    8.54    by (unfold type_definition_def) blast
    8.55  
    8.56 -theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    8.57 +theorem Abs_inverse: "type_definition Rep Abs A ==> y \\<in> A ==> Rep (Abs y) = y"
    8.58    by (unfold type_definition_def) blast
    8.59  
    8.60  theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    8.61 @@ -58,10 +71,10 @@
    8.62  qed
    8.63  
    8.64  theorem Abs_inject:
    8.65 -  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    8.66 +  "type_definition Rep Abs A ==> x \\<in> A ==> y \\<in> A ==> (Abs x = Abs y) = (x = y)"
    8.67  proof -
    8.68    assume tydef: "type_definition Rep Abs A"
    8.69 -  assume x: "x \<in> A" and y: "y \<in> A"
    8.70 +  assume x: "x \\<in> A" and y: "y \\<in> A"
    8.71    show ?thesis
    8.72    proof
    8.73      assume "Abs x = Abs y"
    8.74 @@ -76,10 +89,10 @@
    8.75  qed
    8.76  
    8.77  theorem Rep_cases:
    8.78 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    8.79 +  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    8.80  proof -
    8.81    assume tydef: "type_definition Rep Abs A"
    8.82 -  assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
    8.83 +  assume y: "y \\<in> A" and r: "(!!x. y = Rep x ==> P)"
    8.84    show P
    8.85    proof (rule r)
    8.86      from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    8.87 @@ -88,33 +101,33 @@
    8.88  qed
    8.89  
    8.90  theorem Abs_cases:
    8.91 -  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
    8.92 +  "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \\<in> A ==> P) ==> P"
    8.93  proof -
    8.94    assume tydef: "type_definition Rep Abs A"
    8.95 -  assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
    8.96 +  assume r: "!!y. x = Abs y ==> y \\<in> A ==> P"
    8.97    show P
    8.98    proof (rule r)
    8.99      have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   8.100      thus "x = Abs (Rep x)" ..
   8.101 -    show "Rep x \<in> A" by (rule Rep [OF tydef])
   8.102 +    show "Rep x \\<in> A" by (rule Rep [OF tydef])
   8.103    qed
   8.104  qed
   8.105  
   8.106  theorem Rep_induct:
   8.107 -  "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   8.108 +  "type_definition Rep Abs A ==> y \\<in> A ==> (!!x. P (Rep x)) ==> P y"
   8.109  proof -
   8.110    assume tydef: "type_definition Rep Abs A"
   8.111    assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   8.112 -  moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   8.113 +  moreover assume "y \\<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   8.114    ultimately show "P y" by (simp only:)
   8.115  qed
   8.116  
   8.117  theorem Abs_induct:
   8.118 -  "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   8.119 +  "type_definition Rep Abs A ==> (!!y. y \\<in> A ==> P (Abs y)) ==> P x"
   8.120  proof -
   8.121    assume tydef: "type_definition Rep Abs A"
   8.122 -  assume r: "!!y. y \<in> A ==> P (Abs y)"
   8.123 -  have "Rep x \<in> A" by (rule Rep [OF tydef])
   8.124 +  assume r: "!!y. y \\<in> A ==> P (Abs y)"
   8.125 +  have "Rep x \\<in> A" by (rule Rep [OF tydef])
   8.126    hence "P (Abs (Rep x))" by (rule r)
   8.127    moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   8.128    ultimately show "P x" by (simp only:)