src/HOL/Wellfounded.thy
changeset 27823 52971512d1a2
parent 26976 cf147f69b3df
child 28260 703046c93ffe
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Aug 10 12:38:26 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 11 14:49:53 2008 +0200
     1.3 @@ -45,10 +45,6 @@
     1.4  abbreviation acyclicP :: "('a => 'a => bool) => bool" where
     1.5    "acyclicP r == acyclic {(x, y). r x y}"
     1.6  
     1.7 -class wellorder = linorder +
     1.8 -  assumes wf: "wf {(x, y). x < y}"
     1.9 -
    1.10 -
    1.11  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    1.12    by (simp add: wfP_def)
    1.13  
    1.14 @@ -90,6 +86,18 @@
    1.15  (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    1.16  lemmas wf_irrefl = wf_not_refl [elim_format]
    1.17  
    1.18 +lemma wf_wellorderI:
    1.19 +  assumes wf: "wf {(x::'a::ord, y). x < y}"
    1.20 +  assumes lin: "OFCLASS('a::ord, linorder_class)"
    1.21 +  shows "OFCLASS('a::ord, wellorder_class)"
    1.22 +using lin by (rule wellorder_class.intro)
    1.23 +  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
    1.24 +
    1.25 +lemma (in wellorder) wf:
    1.26 +  "wf {(x, y). x < y}"
    1.27 +unfolding wf_def by (blast intro: less_induct)
    1.28 +
    1.29 +
    1.30  subsection {* Basic Results *}
    1.31  
    1.32  text{*transitive closure of a well-founded relation is well-founded! *}
    1.33 @@ -460,43 +468,6 @@
    1.34  *}
    1.35  
    1.36  
    1.37 -subsection {*LEAST and wellorderings*}
    1.38 -
    1.39 -text{* See also @{text wf_linord_ex_has_least} and its consequences in
    1.40 - @{text Wellfounded_Relations.ML}*}
    1.41 -
    1.42 -lemma wellorder_Least_lemma [rule_format]:
    1.43 -     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
    1.44 -apply (rule_tac a = k in wf [THEN wf_induct])
    1.45 -apply (rule impI)
    1.46 -apply (rule classical)
    1.47 -apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
    1.48 -apply (auto simp add: linorder_not_less [symmetric])
    1.49 -done
    1.50 -
    1.51 -lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
    1.52 -lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
    1.53 -
    1.54 --- "The following 3 lemmas are due to Brian Huffman"
    1.55 -lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
    1.56 -apply (erule exE)
    1.57 -apply (erule LeastI)
    1.58 -done
    1.59 -
    1.60 -lemma LeastI2:
    1.61 -  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
    1.62 -by (blast intro: LeastI)
    1.63 -
    1.64 -lemma LeastI2_ex:
    1.65 -  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
    1.66 -by (blast intro: LeastI_ex)
    1.67 -
    1.68 -lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
    1.69 -apply (simp (no_asm_use) add: linorder_not_le [symmetric])
    1.70 -apply (erule contrapos_nn)
    1.71 -apply (erule Least_le)
    1.72 -done
    1.73 -
    1.74  subsection {* @{typ nat} is well-founded *}
    1.75  
    1.76  lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
    1.77 @@ -550,52 +521,6 @@
    1.78  lemma wf_less: "wf {(x, y::nat). x < y}"
    1.79    using wf_less_than by (simp add: less_than_def less_eq [symmetric])
    1.80  
    1.81 -text {* Type @{typ nat} is a wellfounded order *}
    1.82 -
    1.83 -instance nat :: wellorder
    1.84 -  by intro_classes
    1.85 -    (assumption |
    1.86 -      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
    1.87 -
    1.88 -text {* @{text LEAST} theorems for type @{typ nat}*}
    1.89 -
    1.90 -lemma Least_Suc:
    1.91 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.92 -  apply (case_tac "n", auto)
    1.93 -  apply (frule LeastI)
    1.94 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
    1.95 -  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    1.96 -  apply (erule_tac [2] Least_le)
    1.97 -  apply (case_tac "LEAST x. P x", auto)
    1.98 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
    1.99 -  apply (blast intro: order_antisym)
   1.100 -  done
   1.101 -
   1.102 -lemma Least_Suc2:
   1.103 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   1.104 -  apply (erule (1) Least_Suc [THEN ssubst])
   1.105 -  apply simp
   1.106 -  done
   1.107 -
   1.108 -lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
   1.109 -  apply (cases n)
   1.110 -   apply blast
   1.111 -  apply (rule_tac x="LEAST k. P(k)" in exI)
   1.112 -  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   1.113 -  done
   1.114 -
   1.115 -lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
   1.116 -  apply (cases n)
   1.117 -   apply blast
   1.118 -  apply (frule (1) ex_least_nat_le)
   1.119 -  apply (erule exE)
   1.120 -  apply (case_tac k)
   1.121 -   apply simp
   1.122 -  apply (rename_tac k1)
   1.123 -  apply (rule_tac x=k1 in exI)
   1.124 -  apply fastsimp
   1.125 -  done
   1.126 -
   1.127  
   1.128  subsection {* Accessible Part *}
   1.129  
   1.130 @@ -914,8 +839,12 @@
   1.131  
   1.132  setup Size.setup
   1.133  
   1.134 +lemma size_bool [code func]:
   1.135 +  "size (b\<Colon>bool) = 0" by (cases b) auto
   1.136 +
   1.137  lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   1.138    by (induct n) simp_all
   1.139  
   1.140 +declare "prod.size" [noatp]
   1.141  
   1.142  end