Merged theories about wellfoundedness into one: Wellfounded.thy
authorkrauss
Fri Apr 25 15:30:33 2008 +0200 (2008-04-25)
changeset 267484d51ddd6aa5c
parent 26747 f32fa5f5bdd1
child 26749 397a1aeede7d
Merged theories about wellfoundedness into one: Wellfounded.thy
NEWS
src/HOL/Accessible_Part.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/FunDef.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Int.thy
src/HOL/IsaMakefile
src/HOL/Lambda/ROOT.ML
src/HOL/Nat.thy
src/HOL/Recdef.thy
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Wellfounded.thy
src/HOL/Wellfounded_Recursion.thy
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/NEWS	Thu Apr 24 16:53:04 2008 +0200
     1.2 +++ b/NEWS	Fri Apr 25 15:30:33 2008 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations
     1.8 +  to "Wellfounded.thy"
     1.9 +
    1.10  * Explicit class "eq" for executable equality.  INCOMPATIBILITY.
    1.11  
    1.12  * Class finite no longer treats UNIV as class parameter.  Use class enum from
     2.1 --- a/src/HOL/Accessible_Part.thy	Thu Apr 24 16:53:04 2008 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,167 +0,0 @@
     2.4 -(*  Title:      HOL/Accessible_Part.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1994  University of Cambridge
     2.8 -*)
     2.9 -
    2.10 -header {* The accessible part of a relation *}
    2.11 -
    2.12 -theory Accessible_Part
    2.13 -imports Wellfounded_Recursion
    2.14 -begin
    2.15 -
    2.16 -subsection {* Inductive definition *}
    2.17 -
    2.18 -text {*
    2.19 - Inductive definition of the accessible part @{term "acc r"} of a
    2.20 - relation; see also \cite{paulin-tlca}.
    2.21 -*}
    2.22 -
    2.23 -inductive_set
    2.24 -  acc :: "('a * 'a) set => 'a set"
    2.25 -  for r :: "('a * 'a) set"
    2.26 -  where
    2.27 -    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
    2.28 -
    2.29 -abbreviation
    2.30 -  termip :: "('a => 'a => bool) => 'a => bool" where
    2.31 -  "termip r == accp (r\<inverse>\<inverse>)"
    2.32 -
    2.33 -abbreviation
    2.34 -  termi :: "('a * 'a) set => 'a set" where
    2.35 -  "termi r == acc (r\<inverse>)"
    2.36 -
    2.37 -lemmas accpI = accp.accI
    2.38 -
    2.39 -subsection {* Induction rules *}
    2.40 -
    2.41 -theorem accp_induct:
    2.42 -  assumes major: "accp r a"
    2.43 -  assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
    2.44 -  shows "P a"
    2.45 -  apply (rule major [THEN accp.induct])
    2.46 -  apply (rule hyp)
    2.47 -   apply (rule accp.accI)
    2.48 -   apply fast
    2.49 -  apply fast
    2.50 -  done
    2.51 -
    2.52 -theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
    2.53 -
    2.54 -theorem accp_downward: "accp r b ==> r a b ==> accp r a"
    2.55 -  apply (erule accp.cases)
    2.56 -  apply fast
    2.57 -  done
    2.58 -
    2.59 -lemma not_accp_down:
    2.60 -  assumes na: "\<not> accp R x"
    2.61 -  obtains z where "R z x" and "\<not> accp R z"
    2.62 -proof -
    2.63 -  assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
    2.64 -
    2.65 -  show thesis
    2.66 -  proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
    2.67 -    case True
    2.68 -    hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
    2.69 -    hence "accp R x"
    2.70 -      by (rule accp.accI)
    2.71 -    with na show thesis ..
    2.72 -  next
    2.73 -    case False then obtain z where "R z x" and "\<not> accp R z"
    2.74 -      by auto
    2.75 -    with a show thesis .
    2.76 -  qed
    2.77 -qed
    2.78 -
    2.79 -lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
    2.80 -  apply (erule rtranclp_induct)
    2.81 -   apply blast
    2.82 -  apply (blast dest: accp_downward)
    2.83 -  done
    2.84 -
    2.85 -theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
    2.86 -  apply (blast dest: accp_downwards_aux)
    2.87 -  done
    2.88 -
    2.89 -theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
    2.90 -  apply (rule wfPUNIVI)
    2.91 -  apply (induct_tac P x rule: accp_induct)
    2.92 -   apply blast
    2.93 -  apply blast
    2.94 -  done
    2.95 -
    2.96 -theorem accp_wfPD: "wfP r ==> accp r x"
    2.97 -  apply (erule wfP_induct_rule)
    2.98 -  apply (rule accp.accI)
    2.99 -  apply blast
   2.100 -  done
   2.101 -
   2.102 -theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   2.103 -  apply (blast intro: accp_wfPI dest: accp_wfPD)
   2.104 -  done
   2.105 -
   2.106 -
   2.107 -text {* Smaller relations have bigger accessible parts: *}
   2.108 -
   2.109 -lemma accp_subset:
   2.110 -  assumes sub: "R1 \<le> R2"
   2.111 -  shows "accp R2 \<le> accp R1"
   2.112 -proof
   2.113 -  fix x assume "accp R2 x"
   2.114 -  then show "accp R1 x"
   2.115 -  proof (induct x)
   2.116 -    fix x
   2.117 -    assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   2.118 -    with sub show "accp R1 x"
   2.119 -      by (blast intro: accp.accI)
   2.120 -  qed
   2.121 -qed
   2.122 -
   2.123 -
   2.124 -text {* This is a generalized induction theorem that works on
   2.125 -  subsets of the accessible part. *}
   2.126 -
   2.127 -lemma accp_subset_induct:
   2.128 -  assumes subset: "D \<le> accp R"
   2.129 -    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   2.130 -    and "D x"
   2.131 -    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   2.132 -  shows "P x"
   2.133 -proof -
   2.134 -  from subset and `D x`
   2.135 -  have "accp R x" ..
   2.136 -  then show "P x" using `D x`
   2.137 -  proof (induct x)
   2.138 -    fix x
   2.139 -    assume "D x"
   2.140 -      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   2.141 -    with dcl and istep show "P x" by blast
   2.142 -  qed
   2.143 -qed
   2.144 -
   2.145 -
   2.146 -text {* Set versions of the above theorems *}
   2.147 -
   2.148 -lemmas acc_induct = accp_induct [to_set]
   2.149 -
   2.150 -lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   2.151 -
   2.152 -lemmas acc_downward = accp_downward [to_set]
   2.153 -
   2.154 -lemmas not_acc_down = not_accp_down [to_set]
   2.155 -
   2.156 -lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   2.157 -
   2.158 -lemmas acc_downwards = accp_downwards [to_set]
   2.159 -
   2.160 -lemmas acc_wfI = accp_wfPI [to_set]
   2.161 -
   2.162 -lemmas acc_wfD = accp_wfPD [to_set]
   2.163 -
   2.164 -lemmas wf_acc_iff = wfP_accp_iff [to_set]
   2.165 -
   2.166 -lemmas acc_subset = accp_subset [to_set]
   2.167 -
   2.168 -lemmas acc_subset_induct = accp_subset_induct [to_set]
   2.169 -
   2.170 -end
     3.1 --- a/src/HOL/Datatype.thy	Thu Apr 24 16:53:04 2008 +0200
     3.2 +++ b/src/HOL/Datatype.thy	Fri Apr 25 15:30:33 2008 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     3.5  
     3.6  theory Datatype
     3.7 -imports Finite_Set
     3.8 +imports Finite_Set Wellfounded
     3.9  begin
    3.10  
    3.11  lemma size_bool [code func]:
     4.1 --- a/src/HOL/Divides.thy	Thu Apr 24 16:53:04 2008 +0200
     4.2 +++ b/src/HOL/Divides.thy	Fri Apr 25 15:30:33 2008 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  header {* The division operators div,  mod and the divides relation dvd *}
     4.5  
     4.6  theory Divides
     4.7 -imports Nat Power Product_Type Wellfounded_Recursion
     4.8 +imports Nat Power Product_Type
     4.9  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    4.10  begin
    4.11  
     5.1 --- a/src/HOL/Finite_Set.thy	Thu Apr 24 16:53:04 2008 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Fri Apr 25 15:30:33 2008 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Finite sets *}
     5.5  
     5.6  theory Finite_Set
     5.7 -imports Divides
     5.8 +imports Divides Transitive_Closure
     5.9  begin
    5.10  
    5.11  subsection {* Definition and basic properties *}
    5.12 @@ -2639,6 +2639,35 @@
    5.13      by (simp add: Max fold1_antimono [folded dual_max])
    5.14  qed
    5.15  
    5.16 +lemma finite_linorder_induct[consumes 1, case_names empty insert]:
    5.17 + "finite A \<Longrightarrow> P {} \<Longrightarrow>
    5.18 +  (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
    5.19 +  \<Longrightarrow> P A"
    5.20 +proof (induct A rule: measure_induct_rule[where f=card])
    5.21 +  fix A :: "'a set"
    5.22 +  assume IH: "!! B. card B < card A \<Longrightarrow> finite B \<Longrightarrow> P {} \<Longrightarrow>
    5.23 +                 (!!A b. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A))
    5.24 +                  \<Longrightarrow> P B"
    5.25 +  and "finite A" and "P {}"
    5.26 +  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
    5.27 +  show "P A"
    5.28 +  proof cases
    5.29 +    assume "A = {}" thus "P A" using `P {}` by simp
    5.30 +  next
    5.31 +    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
    5.32 +    assume "A \<noteq> {}"
    5.33 +    with `finite A` have "Max A : A" by auto
    5.34 +    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
    5.35 +    note card_Diff1_less[OF `finite A` `Max A : A`]
    5.36 +    moreover have "finite ?B" using `finite A` by simp
    5.37 +    ultimately have "P ?B" using `P {}` step IH by blast
    5.38 +    moreover have "\<forall>a\<in>?B. a < Max A"
    5.39 +      using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
    5.40 +    ultimately show "P A"
    5.41 +      using A insert_Diff_single step[OF `finite ?B`] by fastsimp
    5.42 +  qed
    5.43 +qed
    5.44 +
    5.45  end
    5.46  
    5.47  context ordered_ab_semigroup_add
     6.1 --- a/src/HOL/FunDef.thy	Thu Apr 24 16:53:04 2008 +0200
     6.2 +++ b/src/HOL/FunDef.thy	Fri Apr 25 15:30:33 2008 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* General recursive function definitions *}
     6.5  
     6.6  theory FunDef
     6.7 -imports Accessible_Part
     6.8 +imports Wellfounded
     6.9  uses
    6.10    ("Tools/function_package/fundef_lib.ML")
    6.11    ("Tools/function_package/fundef_common.ML")
    6.12 @@ -19,6 +19,8 @@
    6.13    ("Tools/function_package/fundef_package.ML")
    6.14    ("Tools/function_package/auto_term.ML")
    6.15    ("Tools/function_package/induction_scheme.ML")
    6.16 +  ("Tools/function_package/lexicographic_order.ML")
    6.17 +  ("Tools/function_package/fundef_datatype.ML")
    6.18  begin
    6.19  
    6.20  text {* Definitions with default value. *}
    6.21 @@ -106,10 +108,14 @@
    6.22  use "Tools/function_package/auto_term.ML"
    6.23  use "Tools/function_package/fundef_package.ML"
    6.24  use "Tools/function_package/induction_scheme.ML"
    6.25 +use "Tools/function_package/lexicographic_order.ML"
    6.26 +use "Tools/function_package/fundef_datatype.ML"
    6.27  
    6.28  setup {* 
    6.29    FundefPackage.setup 
    6.30    #> InductionScheme.setup
    6.31 +  #> LexicographicOrder.setup 
    6.32 +  #> FundefDatatype.setup
    6.33  *}
    6.34  
    6.35  lemma let_cong [fundef_cong]:
     7.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Apr 24 16:53:04 2008 +0200
     7.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Apr 25 15:30:33 2008 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     7.5  
     7.6  theory Hilbert_Choice
     7.7 -imports Nat Wellfounded_Recursion
     7.8 +imports Nat Wellfounded
     7.9  uses ("Tools/meson.ML") ("Tools/specification_package.ML")
    7.10  begin
    7.11  
     8.1 --- a/src/HOL/Int.thy	Thu Apr 24 16:53:04 2008 +0200
     8.2 +++ b/src/HOL/Int.thy	Fri Apr 25 15:30:33 2008 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     8.5  
     8.6  theory Int
     8.7 -imports Equiv_Relations Nat Wellfounded_Relations
     8.8 +imports Equiv_Relations Nat Wellfounded
     8.9  uses
    8.10    ("Tools/numeral.ML")
    8.11    ("Tools/numeral_syntax.ML")
     9.1 --- a/src/HOL/IsaMakefile	Thu Apr 24 16:53:04 2008 +0200
     9.2 +++ b/src/HOL/IsaMakefile	Fri Apr 25 15:30:33 2008 +0200
     9.3 @@ -92,7 +92,7 @@
     9.4    $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML	\
     9.5    $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
     9.6    $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
     9.7 -  Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
     9.8 +  Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
     9.9    Divides.thy Equiv_Relations.thy Extraction.thy	\
    9.10    Finite_Set.thy Fun.thy FunDef.thy HOL.thy		\
    9.11    Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy	\
    9.12 @@ -142,8 +142,8 @@
    9.13    Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML	\
    9.14    Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML	\
    9.15    Tools/typedef_codegen.ML Tools/typedef_package.ML			\
    9.16 -  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
    9.17 -  Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML	\
    9.18 +  Transitive_Closure.thy Typedef.thy Wellfounded.thy		\
    9.19 +  arith_data.ML document/root.tex hologic.ML	\
    9.20    int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
    9.21  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    9.22  
    10.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Apr 24 16:53:04 2008 +0200
    10.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Apr 25 15:30:33 2008 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  Syntax.ambiguity_level := 100;
    10.5  Proofterm.proofs := 2;
    10.6  
    10.7 -no_document use_thys ["Accessible_Part", "Code_Integer"];
    10.8 +no_document use_thys ["Code_Integer"];
    10.9  use_thys ["Eta", "StrongNorm", "Standardization"];
   10.10  if HOL_proofs < 2 then
   10.11    warning "HOL proof terms required for running theory WeakNorm"
    11.1 --- a/src/HOL/Nat.thy	Thu Apr 24 16:53:04 2008 +0200
    11.2 +++ b/src/HOL/Nat.thy	Fri Apr 25 15:30:33 2008 +0200
    11.3 @@ -734,7 +734,55 @@
    11.4  by simp
    11.5  
    11.6  
    11.7 -subsubsection {* Additional theorems about "less than" *}
    11.8 +subsubsection {* Additional theorems about @{term "op \<le>"} *}
    11.9 +
   11.10 +text {* Complete induction, aka course-of-values induction *}
   11.11 +
   11.12 +lemma less_induct [case_names less]:
   11.13 +  fixes P :: "nat \<Rightarrow> bool"
   11.14 +  assumes step: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   11.15 +  shows "P a"
   11.16 +proof - 
   11.17 +  have "\<And>z. z\<le>a \<Longrightarrow> P z"
   11.18 +  proof (induct a)
   11.19 +    case (0 z)
   11.20 +    have "P 0" by (rule step) auto
   11.21 +    thus ?case using 0 by auto
   11.22 +  next
   11.23 +    case (Suc x z)
   11.24 +    then have "z \<le> x \<or> z = Suc x" by (simp add: le_Suc_eq)
   11.25 +    thus ?case
   11.26 +    proof
   11.27 +      assume "z \<le> x" thus "P z" by (rule Suc(1))
   11.28 +    next
   11.29 +      assume z: "z = Suc x"
   11.30 +      show "P z"
   11.31 +        by (rule step) (rule Suc(1), simp add: z le_simps)
   11.32 +    qed
   11.33 +  qed
   11.34 +  thus ?thesis by auto
   11.35 +qed
   11.36 +
   11.37 +lemma nat_less_induct:
   11.38 +  assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   11.39 +  using assms less_induct by blast
   11.40 +
   11.41 +lemma measure_induct_rule [case_names less]:
   11.42 +  fixes f :: "'a \<Rightarrow> nat"
   11.43 +  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
   11.44 +  shows "P a"
   11.45 +by (induct m\<equiv>"f a" arbitrary: a rule: less_induct) (auto intro: step)
   11.46 +
   11.47 +text {* old style induction rules: *}
   11.48 +lemma measure_induct:
   11.49 +  fixes f :: "'a \<Rightarrow> nat"
   11.50 +  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   11.51 +  by (rule measure_induct_rule [of f P a]) iprover
   11.52 +
   11.53 +lemma full_nat_induct:
   11.54 +  assumes step: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
   11.55 +  shows "P n"
   11.56 +  by (rule less_induct) (auto intro: step simp:le_simps)
   11.57  
   11.58  text{*An induction rule for estabilishing binary relations*}
   11.59  lemma less_Suc_induct:
   11.60 @@ -755,6 +803,73 @@
   11.61    thus "P i j" by (simp add: j)
   11.62  qed
   11.63  
   11.64 +lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   11.65 +  apply (rule nat_less_induct)
   11.66 +  apply (case_tac n)
   11.67 +  apply (case_tac [2] nat)
   11.68 +  apply (blast intro: less_trans)+
   11.69 +  done
   11.70 +
   11.71 +text {* The method of infinite descent, frequently used in number theory.
   11.72 +Provided by Roelof Oosterhuis.
   11.73 +$P(n)$ is true for all $n\in\mathbb{N}$ if
   11.74 +\begin{itemize}
   11.75 +  \item case ``0'': given $n=0$ prove $P(n)$,
   11.76 +  \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
   11.77 +        a smaller integer $m$ such that $\neg P(m)$.
   11.78 +\end{itemize} *}
   11.79 +
   11.80 +text{* A compact version without explicit base case: *}
   11.81 +lemma infinite_descent:
   11.82 +  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   11.83 +by (induct n rule: less_induct, auto)
   11.84 +
   11.85 +lemma infinite_descent0[case_names 0 smaller]: 
   11.86 +  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   11.87 +by (rule infinite_descent) (case_tac "n>0", auto)
   11.88 +
   11.89 +text {*
   11.90 +Infinite descent using a mapping to $\mathbb{N}$:
   11.91 +$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
   11.92 +\begin{itemize}
   11.93 +\item case ``0'': given $V(x)=0$ prove $P(x)$,
   11.94 +\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
   11.95 +\end{itemize}
   11.96 +NB: the proof also shows how to use the previous lemma. *}
   11.97 +
   11.98 +corollary infinite_descent0_measure [case_names 0 smaller]:
   11.99 +  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
  11.100 +    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
  11.101 +  shows "P x"
  11.102 +proof -
  11.103 +  obtain n where "n = V x" by auto
  11.104 +  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  11.105 +  proof (induct n rule: infinite_descent0)
  11.106 +    case 0 -- "i.e. $V(x) = 0$"
  11.107 +    with A0 show "P x" by auto
  11.108 +  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  11.109 +    case (smaller n)
  11.110 +    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  11.111 +    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  11.112 +    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  11.113 +    then show ?case by auto
  11.114 +  qed
  11.115 +  ultimately show "P x" by auto
  11.116 +qed
  11.117 +
  11.118 +text{* Again, without explicit base case: *}
  11.119 +lemma infinite_descent_measure:
  11.120 +assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  11.121 +proof -
  11.122 +  from assms obtain n where "n = V x" by auto
  11.123 +  moreover have "!!x. V x = n \<Longrightarrow> P x"
  11.124 +  proof (induct n rule: infinite_descent, auto)
  11.125 +    fix x assume "\<not> P x"
  11.126 +    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  11.127 +  qed
  11.128 +  ultimately show "P x" by auto
  11.129 +qed
  11.130 +
  11.131  text {* A [clumsy] way of lifting @{text "<"}
  11.132    monotonicity to @{text "\<le>"} monotonicity *}
  11.133  lemma less_mono_imp_le_mono:
  11.134 @@ -809,7 +924,7 @@
  11.135  done
  11.136  
  11.137  lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
  11.138 -by (simp add: add_commute not_add_less1)
  11.139 +by (simp add: add_commute)
  11.140  
  11.141  lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
  11.142  apply (rule order_trans [of _ "m+k"])
  11.143 @@ -841,7 +956,7 @@
  11.144  by (simp add: add_diff_inverse linorder_not_less)
  11.145  
  11.146  lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
  11.147 -by (simp add: le_add_diff_inverse add_commute)
  11.148 +by (simp add: add_commute)
  11.149  
  11.150  lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
  11.151  by (induct m n rule: diff_induct) simp_all
  11.152 @@ -1328,6 +1443,6 @@
  11.153  subsection {* size of a datatype value *}
  11.154  
  11.155  class size = type +
  11.156 -  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded_Recursion} *}
  11.157 +  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
  11.158  
  11.159  end
    12.1 --- a/src/HOL/Recdef.thy	Thu Apr 24 16:53:04 2008 +0200
    12.2 +++ b/src/HOL/Recdef.thy	Fri Apr 25 15:30:33 2008 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  header {* TFL: recursive function definitions *}
    12.5  
    12.6  theory Recdef
    12.7 -imports Wellfounded_Relations FunDef
    12.8 +imports FunDef
    12.9  uses
   12.10    ("Tools/TFL/casesplit.ML")
   12.11    ("Tools/TFL/utils.ML")
   12.12 @@ -20,6 +20,30 @@
   12.13    ("Tools/recdef_package.ML")
   12.14  begin
   12.15  
   12.16 +text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
   12.17 +lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
   12.18 +apply auto
   12.19 +apply (blast intro: wfrec)
   12.20 +done
   12.21 +
   12.22 +
   12.23 +lemma tfl_wf_induct: "ALL R. wf R -->  
   12.24 +       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
   12.25 +apply clarify
   12.26 +apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
   12.27 +done
   12.28 +
   12.29 +lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
   12.30 +apply clarify
   12.31 +apply (rule cut_apply, assumption)
   12.32 +done
   12.33 +
   12.34 +lemma tfl_wfrec:
   12.35 +     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
   12.36 +apply clarify
   12.37 +apply (erule wfrec)
   12.38 +done
   12.39 +
   12.40  lemma tfl_eq_True: "(x = True) --> x"
   12.41    by blast
   12.42  
    13.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 24 16:53:04 2008 +0200
    13.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 25 15:30:33 2008 +0200
    13.3 @@ -17,7 +17,7 @@
    13.4  fun PROFILE msg = if !profile then timeap_msg msg else I
    13.5  
    13.6  
    13.7 -val acc_const_name = "Accessible_Part.accp"
    13.8 +val acc_const_name = @{const_name "accp"}
    13.9  fun mk_acc domT R =
   13.10      Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
   13.11  
    14.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Apr 24 16:53:04 2008 +0200
    14.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Apr 25 15:30:33 2008 +0200
    14.3 @@ -95,17 +95,17 @@
    14.4  (* Theory dependencies. *)
    14.5  val Pair_inject = @{thm Product_Type.Pair_inject};
    14.6  
    14.7 -val acc_induct_rule = @{thm Accessible_Part.accp_induct_rule};
    14.8 +val acc_induct_rule = @{thm accp_induct_rule};
    14.9  
   14.10  val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
   14.11  val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
   14.12  val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
   14.13  
   14.14 -val acc_downward = @{thm Accessible_Part.accp_downward};
   14.15 -val accI = @{thm Accessible_Part.accp.accI};
   14.16 +val acc_downward = @{thm accp_downward};
   14.17 +val accI = @{thm accp.accI};
   14.18  val case_split = @{thm HOL.case_split_thm};
   14.19  val fundef_default_value = @{thm FunDef.fundef_default_value};
   14.20 -val not_acc_down = @{thm Accessible_Part.not_accp_down};
   14.21 +val not_acc_down = @{thm not_accp_down};
   14.22  
   14.23  
   14.24  
   14.25 @@ -575,7 +575,7 @@
   14.26  (** Induction rule **)
   14.27  
   14.28  
   14.29 -val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
   14.30 +val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
   14.31  
   14.32  
   14.33  fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
   14.34 @@ -710,7 +710,7 @@
   14.35  
   14.36  (** Termination rule **)
   14.37  
   14.38 -val wf_induct_rule = @{thm Wellfounded_Recursion.wfP_induct_rule};
   14.39 +val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
   14.40  val wf_in_rel = @{thm FunDef.wf_in_rel};
   14.41  val in_rel_def = @{thm FunDef.in_rel_def};
   14.42  
   14.43 @@ -770,7 +770,7 @@
   14.44        val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
   14.45        val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   14.46                      
   14.47 -      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   14.48 +      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   14.49                            
   14.50        (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   14.51        val ihyp = all domT $ Abs ("z", domT, 
    15.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 24 16:53:04 2008 +0200
    15.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 25 15:30:33 2008 +0200
    15.3 @@ -50,7 +50,7 @@
    15.4          val mlexT = (domT --> HOLogic.natT) --> relT --> relT
    15.5          fun mk_ms [] = Const (@{const_name "{}"}, relT)
    15.6            | mk_ms (f::fs) = 
    15.7 -            Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs
    15.8 +            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
    15.9      in
   15.10          mk_ms mfuns
   15.11      end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Wellfounded.thy	Fri Apr 25 15:30:33 2008 +0200
    16.3 @@ -0,0 +1,919 @@
    16.4 +(*  ID:         $Id$
    16.5 +    Author:     Tobias Nipkow
    16.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 +    Author:     Konrad Slind, Alexander Krauss
    16.8 +    Copyright   1992-2008  University of Cambridge and TU Muenchen
    16.9 +*)
   16.10 +
   16.11 +header {*Well-founded Recursion*}
   16.12 +
   16.13 +theory Wellfounded
   16.14 +imports Finite_Set Nat
   16.15 +uses ("Tools/function_package/size.ML")
   16.16 +begin
   16.17 +
   16.18 +inductive
   16.19 +  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
   16.20 +  for R :: "('a * 'a) set"
   16.21 +  and F :: "('a => 'b) => 'a => 'b"
   16.22 +where
   16.23 +  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
   16.24 +            wfrec_rel R F x (F g x)"
   16.25 +
   16.26 +constdefs
   16.27 +  wf         :: "('a * 'a)set => bool"
   16.28 +  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
   16.29 +
   16.30 +  wfP :: "('a => 'a => bool) => bool"
   16.31 +  "wfP r == wf {(x, y). r x y}"
   16.32 +
   16.33 +  acyclic :: "('a*'a)set => bool"
   16.34 +  "acyclic r == !x. (x,x) ~: r^+"
   16.35 +
   16.36 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
   16.37 +  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
   16.38 +
   16.39 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
   16.40 +  "adm_wf R F == ALL f g x.
   16.41 +     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   16.42 +
   16.43 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
   16.44 +  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   16.45 +
   16.46 +abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   16.47 +  "acyclicP r == acyclic {(x, y). r x y}"
   16.48 +
   16.49 +class wellorder = linorder +
   16.50 +  assumes wf: "wf {(x, y). x < y}"
   16.51 +
   16.52 +
   16.53 +lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   16.54 +  by (simp add: wfP_def)
   16.55 +
   16.56 +lemma wfUNIVI: 
   16.57 +   "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
   16.58 +  unfolding wf_def by blast
   16.59 +
   16.60 +lemmas wfPUNIVI = wfUNIVI [to_pred]
   16.61 +
   16.62 +text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
   16.63 +    well-founded over their intersection, then @{term "wf r"}*}
   16.64 +lemma wfI: 
   16.65 + "[| r \<subseteq> A <*> B; 
   16.66 +     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   16.67 +  ==>  wf r"
   16.68 +  unfolding wf_def by blast
   16.69 +
   16.70 +lemma wf_induct: 
   16.71 +    "[| wf(r);           
   16.72 +        !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
   16.73 +     |]  ==>  P(a)"
   16.74 +  unfolding wf_def by blast
   16.75 +
   16.76 +lemmas wfP_induct = wf_induct [to_pred]
   16.77 +
   16.78 +lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
   16.79 +
   16.80 +lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
   16.81 +
   16.82 +lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
   16.83 +  by (induct a arbitrary: x set: wf) blast
   16.84 +
   16.85 +(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
   16.86 +lemmas wf_asym = wf_not_sym [elim_format]
   16.87 +
   16.88 +lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
   16.89 +  by (blast elim: wf_asym)
   16.90 +
   16.91 +(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
   16.92 +lemmas wf_irrefl = wf_not_refl [elim_format]
   16.93 +
   16.94 +text{*transitive closure of a well-founded relation is well-founded! *}
   16.95 +lemma wf_trancl:
   16.96 +  assumes "wf r"
   16.97 +  shows "wf (r^+)"
   16.98 +proof -
   16.99 +  {
  16.100 +    fix P and x
  16.101 +    assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
  16.102 +    have "P x"
  16.103 +    proof (rule induct_step)
  16.104 +      fix y assume "(y, x) : r^+"
  16.105 +      with `wf r` show "P y"
  16.106 +      proof (induct x arbitrary: y)
  16.107 +	case (less x)
  16.108 +	note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
  16.109 +	from `(y, x) : r^+` show "P y"
  16.110 +	proof cases
  16.111 +	  case base
  16.112 +	  show "P y"
  16.113 +	  proof (rule induct_step)
  16.114 +	    fix y' assume "(y', y) : r^+"
  16.115 +	    with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
  16.116 +	  qed
  16.117 +	next
  16.118 +	  case step
  16.119 +	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
  16.120 +	  then show "P y" by (rule hyp [of x' y])
  16.121 +	qed
  16.122 +      qed
  16.123 +    qed
  16.124 +  } then show ?thesis unfolding wf_def by blast
  16.125 +qed
  16.126 +
  16.127 +lemmas wfP_trancl = wf_trancl [to_pred]
  16.128 +
  16.129 +lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
  16.130 +  apply (subst trancl_converse [symmetric])
  16.131 +  apply (erule wf_trancl)
  16.132 +  done
  16.133 +
  16.134 +
  16.135 +subsubsection {* Other simple well-foundedness results *}
  16.136 +
  16.137 +text{*Minimal-element characterization of well-foundedness*}
  16.138 +lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
  16.139 +proof (intro iffI strip)
  16.140 +  fix Q :: "'a set" and x
  16.141 +  assume "wf r" and "x \<in> Q"
  16.142 +  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
  16.143 +    unfolding wf_def
  16.144 +    by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
  16.145 +next
  16.146 +  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
  16.147 +  show "wf r"
  16.148 +  proof (rule wfUNIVI)
  16.149 +    fix P :: "'a \<Rightarrow> bool" and x
  16.150 +    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
  16.151 +    let ?Q = "{x. \<not> P x}"
  16.152 +    have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
  16.153 +      by (rule 1 [THEN spec, THEN spec])
  16.154 +    then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
  16.155 +    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
  16.156 +    then show "P x" by simp
  16.157 +  qed
  16.158 +qed
  16.159 +
  16.160 +lemma wfE_min: 
  16.161 +  assumes "wf R" "x \<in> Q"
  16.162 +  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
  16.163 +  using assms unfolding wf_eq_minimal by blast
  16.164 +
  16.165 +lemma wfI_min:
  16.166 +  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
  16.167 +  \<Longrightarrow> wf R"
  16.168 +  unfolding wf_eq_minimal by blast
  16.169 +
  16.170 +lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
  16.171 +
  16.172 +text {* Well-foundedness of subsets *}
  16.173 +lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
  16.174 +  apply (simp (no_asm_use) add: wf_eq_minimal)
  16.175 +  apply fast
  16.176 +  done
  16.177 +
  16.178 +lemmas wfP_subset = wf_subset [to_pred]
  16.179 +
  16.180 +text {* Well-foundedness of the empty relation *}
  16.181 +lemma wf_empty [iff]: "wf({})"
  16.182 +  by (simp add: wf_def)
  16.183 +
  16.184 +lemmas wfP_empty [iff] =
  16.185 +  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
  16.186 +
  16.187 +lemma wf_Int1: "wf r ==> wf (r Int r')"
  16.188 +  apply (erule wf_subset)
  16.189 +  apply (rule Int_lower1)
  16.190 +  done
  16.191 +
  16.192 +lemma wf_Int2: "wf r ==> wf (r' Int r)"
  16.193 +  apply (erule wf_subset)
  16.194 +  apply (rule Int_lower2)
  16.195 +  done  
  16.196 +
  16.197 +text{*Well-foundedness of insert*}
  16.198 +lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
  16.199 +apply (rule iffI)
  16.200 + apply (blast elim: wf_trancl [THEN wf_irrefl]
  16.201 +              intro: rtrancl_into_trancl1 wf_subset 
  16.202 +                     rtrancl_mono [THEN [2] rev_subsetD])
  16.203 +apply (simp add: wf_eq_minimal, safe)
  16.204 +apply (rule allE, assumption, erule impE, blast) 
  16.205 +apply (erule bexE)
  16.206 +apply (rename_tac "a", case_tac "a = x")
  16.207 + prefer 2
  16.208 +apply blast 
  16.209 +apply (case_tac "y:Q")
  16.210 + prefer 2 apply blast
  16.211 +apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
  16.212 + apply assumption
  16.213 +apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
  16.214 +  --{*essential for speed*}
  16.215 +txt{*Blast with new substOccur fails*}
  16.216 +apply (fast intro: converse_rtrancl_into_rtrancl)
  16.217 +done
  16.218 +
  16.219 +text{*Well-foundedness of image*}
  16.220 +lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
  16.221 +apply (simp only: wf_eq_minimal, clarify)
  16.222 +apply (case_tac "EX p. f p : Q")
  16.223 +apply (erule_tac x = "{p. f p : Q}" in allE)
  16.224 +apply (fast dest: inj_onD, blast)
  16.225 +done
  16.226 +
  16.227 +
  16.228 +subsubsection {* Well-Foundedness Results for Unions *}
  16.229 +
  16.230 +lemma wf_union_compatible:
  16.231 +  assumes "wf R" "wf S"
  16.232 +  assumes "S O R \<subseteq> R"
  16.233 +  shows "wf (R \<union> S)"
  16.234 +proof (rule wfI_min)
  16.235 +  fix x :: 'a and Q 
  16.236 +  let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
  16.237 +  assume "x \<in> Q"
  16.238 +  obtain a where "a \<in> ?Q'"
  16.239 +    by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
  16.240 +  with `wf S`
  16.241 +  obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
  16.242 +  { 
  16.243 +    fix y assume "(y, z) \<in> S"
  16.244 +    then have "y \<notin> ?Q'" by (rule zmin)
  16.245 +
  16.246 +    have "y \<notin> Q"
  16.247 +    proof 
  16.248 +      assume "y \<in> Q"
  16.249 +      with `y \<notin> ?Q'` 
  16.250 +      obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
  16.251 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
  16.252 +      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
  16.253 +      with `z \<in> ?Q'` have "w \<notin> Q" by blast 
  16.254 +      with `w \<in> Q` show False by contradiction
  16.255 +    qed
  16.256 +  }
  16.257 +  with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
  16.258 +qed
  16.259 +
  16.260 +
  16.261 +text {* Well-foundedness of indexed union with disjoint domains and ranges *}
  16.262 +
  16.263 +lemma wf_UN: "[| ALL i:I. wf(r i);  
  16.264 +         ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
  16.265 +      |] ==> wf(UN i:I. r i)"
  16.266 +apply (simp only: wf_eq_minimal, clarify)
  16.267 +apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
  16.268 + prefer 2
  16.269 + apply force 
  16.270 +apply clarify
  16.271 +apply (drule bspec, assumption)  
  16.272 +apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
  16.273 +apply (blast elim!: allE)  
  16.274 +done
  16.275 +
  16.276 +lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
  16.277 +  to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]
  16.278 +
  16.279 +lemma wf_Union: 
  16.280 + "[| ALL r:R. wf r;  
  16.281 +     ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
  16.282 +  |] ==> wf(Union R)"
  16.283 +apply (simp add: Union_def)
  16.284 +apply (blast intro: wf_UN)
  16.285 +done
  16.286 +
  16.287 +(*Intuition: we find an (R u S)-min element of a nonempty subset A
  16.288 +             by case distinction.
  16.289 +  1. There is a step a -R-> b with a,b : A.
  16.290 +     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
  16.291 +     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
  16.292 +     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
  16.293 +     have an S-successor and is thus S-min in A as well.
  16.294 +  2. There is no such step.
  16.295 +     Pick an S-min element of A. In this case it must be an R-min
  16.296 +     element of A as well.
  16.297 +
  16.298 +*)
  16.299 +lemma wf_Un:
  16.300 +     "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
  16.301 +  using wf_union_compatible[of s r] 
  16.302 +  by (auto simp: Un_ac)
  16.303 +
  16.304 +lemma wf_union_merge: 
  16.305 +  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
  16.306 +proof
  16.307 +  assume "wf ?A"
  16.308 +  with wf_trancl have wfT: "wf (?A^+)" .
  16.309 +  moreover have "?B \<subseteq> ?A^+"
  16.310 +    by (subst trancl_unfold, subst trancl_unfold) blast
  16.311 +  ultimately show "wf ?B" by (rule wf_subset)
  16.312 +next
  16.313 +  assume "wf ?B"
  16.314 +
  16.315 +  show "wf ?A"
  16.316 +  proof (rule wfI_min)
  16.317 +    fix Q :: "'a set" and x 
  16.318 +    assume "x \<in> Q"
  16.319 +
  16.320 +    with `wf ?B`
  16.321 +    obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
  16.322 +      by (erule wfE_min)
  16.323 +    then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
  16.324 +      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
  16.325 +      and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
  16.326 +      by auto
  16.327 +    
  16.328 +    show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
  16.329 +    proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
  16.330 +      case True
  16.331 +      with `z \<in> Q` A3 show ?thesis by blast
  16.332 +    next
  16.333 +      case False 
  16.334 +      then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
  16.335 +
  16.336 +      have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
  16.337 +      proof (intro allI impI)
  16.338 +        fix y assume "(y, z') \<in> ?A"
  16.339 +        then show "y \<notin> Q"
  16.340 +        proof
  16.341 +          assume "(y, z') \<in> R" 
  16.342 +          then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
  16.343 +          with A1 show "y \<notin> Q" .
  16.344 +        next
  16.345 +          assume "(y, z') \<in> S" 
  16.346 +          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
  16.347 +          with A2 show "y \<notin> Q" .
  16.348 +        qed
  16.349 +      qed
  16.350 +      with `z' \<in> Q` show ?thesis ..
  16.351 +    qed
  16.352 +  qed
  16.353 +qed
  16.354 +
  16.355 +lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
  16.356 +  by (rule wf_union_merge [where S = "{}", simplified])
  16.357 +
  16.358 +
  16.359 +subsubsection {* acyclic *}
  16.360 +
  16.361 +lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
  16.362 +  by (simp add: acyclic_def)
  16.363 +
  16.364 +lemma wf_acyclic: "wf r ==> acyclic r"
  16.365 +apply (simp add: acyclic_def)
  16.366 +apply (blast elim: wf_trancl [THEN wf_irrefl])
  16.367 +done
  16.368 +
  16.369 +lemmas wfP_acyclicP = wf_acyclic [to_pred]
  16.370 +
  16.371 +lemma acyclic_insert [iff]:
  16.372 +     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
  16.373 +apply (simp add: acyclic_def trancl_insert)
  16.374 +apply (blast intro: rtrancl_trans)
  16.375 +done
  16.376 +
  16.377 +lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
  16.378 +by (simp add: acyclic_def trancl_converse)
  16.379 +
  16.380 +lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
  16.381 +
  16.382 +lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
  16.383 +apply (simp add: acyclic_def antisym_def)
  16.384 +apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
  16.385 +done
  16.386 +
  16.387 +(* Other direction:
  16.388 +acyclic = no loops
  16.389 +antisym = only self loops
  16.390 +Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
  16.391 +==> antisym( r^* ) = acyclic(r - Id)";
  16.392 +*)
  16.393 +
  16.394 +lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
  16.395 +apply (simp add: acyclic_def)
  16.396 +apply (blast intro: trancl_mono)
  16.397 +done
  16.398 +
  16.399 +text{* Wellfoundedness of finite acyclic relations*}
  16.400 +
  16.401 +lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
  16.402 +apply (erule finite_induct, blast)
  16.403 +apply (simp (no_asm_simp) only: split_tupled_all)
  16.404 +apply simp
  16.405 +done
  16.406 +
  16.407 +lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
  16.408 +apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
  16.409 +apply (erule acyclic_converse [THEN iffD2])
  16.410 +done
  16.411 +
  16.412 +lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
  16.413 +by (blast intro: finite_acyclic_wf wf_acyclic)
  16.414 +
  16.415 +
  16.416 +subsection{*Well-Founded Recursion*}
  16.417 +
  16.418 +text{*cut*}
  16.419 +
  16.420 +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
  16.421 +by (simp add: expand_fun_eq cut_def)
  16.422 +
  16.423 +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
  16.424 +by (simp add: cut_def)
  16.425 +
  16.426 +text{*Inductive characterization of wfrec combinator; for details see:  
  16.427 +John Harrison, "Inductive definitions: automation and application"*}
  16.428 +
  16.429 +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
  16.430 +apply (simp add: adm_wf_def)
  16.431 +apply (erule_tac a=x in wf_induct) 
  16.432 +apply (rule ex1I)
  16.433 +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
  16.434 +apply (fast dest!: theI')
  16.435 +apply (erule wfrec_rel.cases, simp)
  16.436 +apply (erule allE, erule allE, erule allE, erule mp)
  16.437 +apply (fast intro: the_equality [symmetric])
  16.438 +done
  16.439 +
  16.440 +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
  16.441 +apply (simp add: adm_wf_def)
  16.442 +apply (intro strip)
  16.443 +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
  16.444 +apply (rule refl)
  16.445 +done
  16.446 +
  16.447 +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
  16.448 +apply (simp add: wfrec_def)
  16.449 +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
  16.450 +apply (rule wfrec_rel.wfrecI)
  16.451 +apply (intro strip)
  16.452 +apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
  16.453 +done
  16.454 +
  16.455 +subsection {* Code generator setup *}
  16.456 +
  16.457 +consts_code
  16.458 +  "wfrec"   ("\<module>wfrec?")
  16.459 +attach {*
  16.460 +fun wfrec f x = f (wfrec f) x;
  16.461 +*}
  16.462 +
  16.463 +
  16.464 +subsection {*LEAST and wellorderings*}
  16.465 +
  16.466 +text{* See also @{text wf_linord_ex_has_least} and its consequences in
  16.467 + @{text Wellfounded_Relations.ML}*}
  16.468 +
  16.469 +lemma wellorder_Least_lemma [rule_format]:
  16.470 +     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
  16.471 +apply (rule_tac a = k in wf [THEN wf_induct])
  16.472 +apply (rule impI)
  16.473 +apply (rule classical)
  16.474 +apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
  16.475 +apply (auto simp add: linorder_not_less [symmetric])
  16.476 +done
  16.477 +
  16.478 +lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
  16.479 +lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
  16.480 +
  16.481 +-- "The following 3 lemmas are due to Brian Huffman"
  16.482 +lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
  16.483 +apply (erule exE)
  16.484 +apply (erule LeastI)
  16.485 +done
  16.486 +
  16.487 +lemma LeastI2:
  16.488 +  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
  16.489 +by (blast intro: LeastI)
  16.490 +
  16.491 +lemma LeastI2_ex:
  16.492 +  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
  16.493 +by (blast intro: LeastI_ex)
  16.494 +
  16.495 +lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
  16.496 +apply (simp (no_asm_use) add: linorder_not_le [symmetric])
  16.497 +apply (erule contrapos_nn)
  16.498 +apply (erule Least_le)
  16.499 +done
  16.500 +
  16.501 +subsection {* @{typ nat} is well-founded *}
  16.502 +
  16.503 +lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
  16.504 +proof (rule ext, rule ext, rule iffI)
  16.505 +  fix n m :: nat
  16.506 +  assume "m < n"
  16.507 +  then show "(\<lambda>m n. n = Suc m)^++ m n"
  16.508 +  proof (induct n)
  16.509 +    case 0 then show ?case by auto
  16.510 +  next
  16.511 +    case (Suc n) then show ?case
  16.512 +      by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
  16.513 +  qed
  16.514 +next
  16.515 +  fix n m :: nat
  16.516 +  assume "(\<lambda>m n. n = Suc m)^++ m n"
  16.517 +  then show "m < n"
  16.518 +    by (induct n)
  16.519 +      (simp_all add: less_Suc_eq_le reflexive le_less)
  16.520 +qed
  16.521 +
  16.522 +definition
  16.523 +  pred_nat :: "(nat * nat) set" where
  16.524 +  "pred_nat = {(m, n). n = Suc m}"
  16.525 +
  16.526 +definition
  16.527 +  less_than :: "(nat * nat) set" where
  16.528 +  "less_than = pred_nat^+"
  16.529 +
  16.530 +lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
  16.531 +  unfolding less_nat_rel pred_nat_def trancl_def by simp
  16.532 +
  16.533 +lemma pred_nat_trancl_eq_le:
  16.534 +  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
  16.535 +  unfolding less_eq rtrancl_eq_or_trancl by auto
  16.536 +
  16.537 +lemma wf_pred_nat: "wf pred_nat"
  16.538 +  apply (unfold wf_def pred_nat_def, clarify)
  16.539 +  apply (induct_tac x, blast+)
  16.540 +  done
  16.541 +
  16.542 +lemma wf_less_than [iff]: "wf less_than"
  16.543 +  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
  16.544 +
  16.545 +lemma trans_less_than [iff]: "trans less_than"
  16.546 +  by (simp add: less_than_def trans_trancl)
  16.547 +
  16.548 +lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
  16.549 +  by (simp add: less_than_def less_eq)
  16.550 +
  16.551 +lemma wf_less: "wf {(x, y::nat). x < y}"
  16.552 +  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
  16.553 +
  16.554 +text {* Type @{typ nat} is a wellfounded order *}
  16.555 +
  16.556 +instance nat :: wellorder
  16.557 +  by intro_classes
  16.558 +    (assumption |
  16.559 +      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
  16.560 +
  16.561 +text {* @{text LEAST} theorems for type @{typ nat}*}
  16.562 +
  16.563 +lemma Least_Suc:
  16.564 +     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  16.565 +  apply (case_tac "n", auto)
  16.566 +  apply (frule LeastI)
  16.567 +  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
  16.568 +  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
  16.569 +  apply (erule_tac [2] Least_le)
  16.570 +  apply (case_tac "LEAST x. P x", auto)
  16.571 +  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
  16.572 +  apply (blast intro: order_antisym)
  16.573 +  done
  16.574 +
  16.575 +lemma Least_Suc2:
  16.576 +   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
  16.577 +  apply (erule (1) Least_Suc [THEN ssubst])
  16.578 +  apply simp
  16.579 +  done
  16.580 +
  16.581 +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)"
  16.582 +  apply (cases n)
  16.583 +   apply blast
  16.584 +  apply (rule_tac x="LEAST k. P(k)" in exI)
  16.585 +  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
  16.586 +  done
  16.587 +
  16.588 +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)"
  16.589 +  apply (cases n)
  16.590 +   apply blast
  16.591 +  apply (frule (1) ex_least_nat_le)
  16.592 +  apply (erule exE)
  16.593 +  apply (case_tac k)
  16.594 +   apply simp
  16.595 +  apply (rename_tac k1)
  16.596 +  apply (rule_tac x=k1 in exI)
  16.597 +  apply fastsimp
  16.598 +  done
  16.599 +
  16.600 +
  16.601 +subsection {* Accessible Part *}
  16.602 +
  16.603 +text {*
  16.604 + Inductive definition of the accessible part @{term "acc r"} of a
  16.605 + relation; see also \cite{paulin-tlca}.
  16.606 +*}
  16.607 +
  16.608 +inductive_set
  16.609 +  acc :: "('a * 'a) set => 'a set"
  16.610 +  for r :: "('a * 'a) set"
  16.611 +  where
  16.612 +    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
  16.613 +
  16.614 +abbreviation
  16.615 +  termip :: "('a => 'a => bool) => 'a => bool" where
  16.616 +  "termip r == accp (r\<inverse>\<inverse>)"
  16.617 +
  16.618 +abbreviation
  16.619 +  termi :: "('a * 'a) set => 'a set" where
  16.620 +  "termi r == acc (r\<inverse>)"
  16.621 +
  16.622 +lemmas accpI = accp.accI
  16.623 +
  16.624 +text {* Induction rules *}
  16.625 +
  16.626 +theorem accp_induct:
  16.627 +  assumes major: "accp r a"
  16.628 +  assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
  16.629 +  shows "P a"
  16.630 +  apply (rule major [THEN accp.induct])
  16.631 +  apply (rule hyp)
  16.632 +   apply (rule accp.accI)
  16.633 +   apply fast
  16.634 +  apply fast
  16.635 +  done
  16.636 +
  16.637 +theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
  16.638 +
  16.639 +theorem accp_downward: "accp r b ==> r a b ==> accp r a"
  16.640 +  apply (erule accp.cases)
  16.641 +  apply fast
  16.642 +  done
  16.643 +
  16.644 +lemma not_accp_down:
  16.645 +  assumes na: "\<not> accp R x"
  16.646 +  obtains z where "R z x" and "\<not> accp R z"
  16.647 +proof -
  16.648 +  assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
  16.649 +
  16.650 +  show thesis
  16.651 +  proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
  16.652 +    case True
  16.653 +    hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
  16.654 +    hence "accp R x"
  16.655 +      by (rule accp.accI)
  16.656 +    with na show thesis ..
  16.657 +  next
  16.658 +    case False then obtain z where "R z x" and "\<not> accp R z"
  16.659 +      by auto
  16.660 +    with a show thesis .
  16.661 +  qed
  16.662 +qed
  16.663 +
  16.664 +lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
  16.665 +  apply (erule rtranclp_induct)
  16.666 +   apply blast
  16.667 +  apply (blast dest: accp_downward)
  16.668 +  done
  16.669 +
  16.670 +theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
  16.671 +  apply (blast dest: accp_downwards_aux)
  16.672 +  done
  16.673 +
  16.674 +theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
  16.675 +  apply (rule wfPUNIVI)
  16.676 +  apply (induct_tac P x rule: accp_induct)
  16.677 +   apply blast
  16.678 +  apply blast
  16.679 +  done
  16.680 +
  16.681 +theorem accp_wfPD: "wfP r ==> accp r x"
  16.682 +  apply (erule wfP_induct_rule)
  16.683 +  apply (rule accp.accI)
  16.684 +  apply blast
  16.685 +  done
  16.686 +
  16.687 +theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
  16.688 +  apply (blast intro: accp_wfPI dest: accp_wfPD)
  16.689 +  done
  16.690 +
  16.691 +
  16.692 +text {* Smaller relations have bigger accessible parts: *}
  16.693 +
  16.694 +lemma accp_subset:
  16.695 +  assumes sub: "R1 \<le> R2"
  16.696 +  shows "accp R2 \<le> accp R1"
  16.697 +proof
  16.698 +  fix x assume "accp R2 x"
  16.699 +  then show "accp R1 x"
  16.700 +  proof (induct x)
  16.701 +    fix x
  16.702 +    assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
  16.703 +    with sub show "accp R1 x"
  16.704 +      by (blast intro: accp.accI)
  16.705 +  qed
  16.706 +qed
  16.707 +
  16.708 +
  16.709 +text {* This is a generalized induction theorem that works on
  16.710 +  subsets of the accessible part. *}
  16.711 +
  16.712 +lemma accp_subset_induct:
  16.713 +  assumes subset: "D \<le> accp R"
  16.714 +    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
  16.715 +    and "D x"
  16.716 +    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
  16.717 +  shows "P x"
  16.718 +proof -
  16.719 +  from subset and `D x`
  16.720 +  have "accp R x" ..
  16.721 +  then show "P x" using `D x`
  16.722 +  proof (induct x)
  16.723 +    fix x
  16.724 +    assume "D x"
  16.725 +      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
  16.726 +    with dcl and istep show "P x" by blast
  16.727 +  qed
  16.728 +qed
  16.729 +
  16.730 +
  16.731 +text {* Set versions of the above theorems *}
  16.732 +
  16.733 +lemmas acc_induct = accp_induct [to_set]
  16.734 +
  16.735 +lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
  16.736 +
  16.737 +lemmas acc_downward = accp_downward [to_set]
  16.738 +
  16.739 +lemmas not_acc_down = not_accp_down [to_set]
  16.740 +
  16.741 +lemmas acc_downwards_aux = accp_downwards_aux [to_set]
  16.742 +
  16.743 +lemmas acc_downwards = accp_downwards [to_set]
  16.744 +
  16.745 +lemmas acc_wfI = accp_wfPI [to_set]
  16.746 +
  16.747 +lemmas acc_wfD = accp_wfPD [to_set]
  16.748 +
  16.749 +lemmas wf_acc_iff = wfP_accp_iff [to_set]
  16.750 +
  16.751 +lemmas acc_subset = accp_subset [to_set]
  16.752 +
  16.753 +lemmas acc_subset_induct = accp_subset_induct [to_set]
  16.754 +
  16.755 +
  16.756 +subsection {* Tools for building wellfounded relations *}
  16.757 +
  16.758 +text {* Inverse Image *}
  16.759 +
  16.760 +lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
  16.761 +apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
  16.762 +apply clarify
  16.763 +apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
  16.764 +prefer 2 apply (blast del: allE)
  16.765 +apply (erule allE)
  16.766 +apply (erule (1) notE impE)
  16.767 +apply blast
  16.768 +done
  16.769 +
  16.770 +lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
  16.771 +  by (auto simp:inv_image_def)
  16.772 +
  16.773 +text {* Measure functions into @{typ nat} *}
  16.774 +
  16.775 +definition measure :: "('a => nat) => ('a * 'a)set"
  16.776 +where "measure == inv_image less_than"
  16.777 +
  16.778 +lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
  16.779 +  by (simp add:measure_def)
  16.780 +
  16.781 +lemma wf_measure [iff]: "wf (measure f)"
  16.782 +apply (unfold measure_def)
  16.783 +apply (rule wf_less_than [THEN wf_inv_image])
  16.784 +done
  16.785 +
  16.786 +text{* Lexicographic combinations *}
  16.787 +
  16.788 +definition
  16.789 + lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
  16.790 +               (infixr "<*lex*>" 80)
  16.791 +where
  16.792 +    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
  16.793 +
  16.794 +lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
  16.795 +apply (unfold wf_def lex_prod_def) 
  16.796 +apply (rule allI, rule impI)
  16.797 +apply (simp (no_asm_use) only: split_paired_All)
  16.798 +apply (drule spec, erule mp) 
  16.799 +apply (rule allI, rule impI)
  16.800 +apply (drule spec, erule mp, blast) 
  16.801 +done
  16.802 +
  16.803 +lemma in_lex_prod[simp]: 
  16.804 +  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
  16.805 +  by (auto simp:lex_prod_def)
  16.806 +
  16.807 +text{* @{term "op <*lex*>"} preserves transitivity *}
  16.808 +
  16.809 +lemma trans_lex_prod [intro!]: 
  16.810 +    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
  16.811 +by (unfold trans_def lex_prod_def, blast) 
  16.812 +
  16.813 +text {* lexicographic combinations with measure functions *}
  16.814 +
  16.815 +definition 
  16.816 +  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
  16.817 +where
  16.818 +  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
  16.819 +
  16.820 +lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
  16.821 +unfolding mlex_prod_def
  16.822 +by auto
  16.823 +
  16.824 +lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
  16.825 +unfolding mlex_prod_def by simp
  16.826 +
  16.827 +lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
  16.828 +unfolding mlex_prod_def by auto
  16.829 +
  16.830 +text {* proper subset relation on finite sets *}
  16.831 +
  16.832 +definition finite_psubset  :: "('a set * 'a set) set"
  16.833 +where "finite_psubset == {(A,B). A < B & finite B}"
  16.834 +
  16.835 +lemma wf_finite_psubset: "wf(finite_psubset)"
  16.836 +apply (unfold finite_psubset_def)
  16.837 +apply (rule wf_measure [THEN wf_subset])
  16.838 +apply (simp add: measure_def inv_image_def less_than_def less_eq)
  16.839 +apply (fast elim!: psubset_card_mono)
  16.840 +done
  16.841 +
  16.842 +lemma trans_finite_psubset: "trans finite_psubset"
  16.843 +by (simp add: finite_psubset_def psubset_def trans_def, blast)
  16.844 +
  16.845 +
  16.846 +
  16.847 +
  16.848 +text {*Wellfoundedness of @{text same_fst}*}
  16.849 +
  16.850 +definition
  16.851 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
  16.852 +where
  16.853 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
  16.854 +   --{*For @{text rec_def} declarations where the first n parameters
  16.855 +       stay unchanged in the recursive call. 
  16.856 +       See @{text "Library/While_Combinator.thy"} for an application.*}
  16.857 +
  16.858 +lemma same_fstI [intro!]:
  16.859 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
  16.860 +by (simp add: same_fst_def)
  16.861 +
  16.862 +lemma wf_same_fst:
  16.863 +  assumes prem: "(!!x. P x ==> wf(R x))"
  16.864 +  shows "wf(same_fst P R)"
  16.865 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
  16.866 +apply (intro strip)
  16.867 +apply (rename_tac a b)
  16.868 +apply (case_tac "wf (R a)")
  16.869 + apply (erule_tac a = b in wf_induct, blast)
  16.870 +apply (blast intro: prem)
  16.871 +done
  16.872 +
  16.873 +
  16.874 +subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
  16.875 +   stabilize.*}
  16.876 +
  16.877 +text{*This material does not appear to be used any longer.*}
  16.878 +
  16.879 +lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
  16.880 +apply (induct_tac "k", simp_all)
  16.881 +apply (blast intro: rtrancl_trans)
  16.882 +done
  16.883 +
  16.884 +lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
  16.885 +      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
  16.886 +apply (erule wf_induct, clarify)
  16.887 +apply (case_tac "EX j. (f (m+j), f m) : r^+")
  16.888 + apply clarify
  16.889 + apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
  16.890 +  apply clarify
  16.891 +  apply (rule_tac x = "j+i" in exI)
  16.892 +  apply (simp add: add_ac, blast)
  16.893 +apply (rule_tac x = 0 in exI, clarsimp)
  16.894 +apply (drule_tac i = m and k = k in lemma1)
  16.895 +apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
  16.896 +done
  16.897 +
  16.898 +lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
  16.899 +      ==> EX i. ALL k. f (i+k) = f i"
  16.900 +apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
  16.901 +done
  16.902 +
  16.903 +(* special case of the theorem above: <= *)
  16.904 +lemma weak_decr_stable:
  16.905 +     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
  16.906 +apply (rule_tac r = pred_nat in wf_weak_decr_stable)
  16.907 +apply (simp add: pred_nat_trancl_eq_le)
  16.908 +apply (intro wf_trancl wf_pred_nat)
  16.909 +done
  16.910 +
  16.911 +
  16.912 +subsection {* size of a datatype value *}
  16.913 +
  16.914 +use "Tools/function_package/size.ML"
  16.915 +
  16.916 +setup Size.setup
  16.917 +
  16.918 +lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  16.919 +  by (induct n) simp_all
  16.920 +
  16.921 +
  16.922 +end
    17.1 --- a/src/HOL/Wellfounded_Recursion.thy	Thu Apr 24 16:53:04 2008 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,693 +0,0 @@
    17.4 -(*  ID:         $Id$
    17.5 -    Author:     Tobias Nipkow
    17.6 -    Copyright   1992  University of Cambridge
    17.7 -*)
    17.8 -
    17.9 -header {*Well-founded Recursion*}
   17.10 -
   17.11 -theory Wellfounded_Recursion
   17.12 -imports Transitive_Closure Nat
   17.13 -uses ("Tools/function_package/size.ML")
   17.14 -begin
   17.15 -
   17.16 -inductive
   17.17 -  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
   17.18 -  for R :: "('a * 'a) set"
   17.19 -  and F :: "('a => 'b) => 'a => 'b"
   17.20 -where
   17.21 -  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
   17.22 -            wfrec_rel R F x (F g x)"
   17.23 -
   17.24 -constdefs
   17.25 -  wf         :: "('a * 'a)set => bool"
   17.26 -  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
   17.27 -
   17.28 -  wfP :: "('a => 'a => bool) => bool"
   17.29 -  "wfP r == wf {(x, y). r x y}"
   17.30 -
   17.31 -  acyclic :: "('a*'a)set => bool"
   17.32 -  "acyclic r == !x. (x,x) ~: r^+"
   17.33 -
   17.34 -  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
   17.35 -  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
   17.36 -
   17.37 -  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
   17.38 -  "adm_wf R F == ALL f g x.
   17.39 -     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
   17.40 -
   17.41 -  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
   17.42 -  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   17.43 -
   17.44 -abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   17.45 -  "acyclicP r == acyclic {(x, y). r x y}"
   17.46 -
   17.47 -class wellorder = linorder +
   17.48 -  assumes wf: "wf {(x, y). x < y}"
   17.49 -
   17.50 -
   17.51 -lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   17.52 -  by (simp add: wfP_def)
   17.53 -
   17.54 -lemma wfUNIVI: 
   17.55 -   "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
   17.56 -  unfolding wf_def by blast
   17.57 -
   17.58 -lemmas wfPUNIVI = wfUNIVI [to_pred]
   17.59 -
   17.60 -text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
   17.61 -    well-founded over their intersection, then @{term "wf r"}*}
   17.62 -lemma wfI: 
   17.63 - "[| r \<subseteq> A <*> B; 
   17.64 -     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
   17.65 -  ==>  wf r"
   17.66 -  unfolding wf_def by blast
   17.67 -
   17.68 -lemma wf_induct: 
   17.69 -    "[| wf(r);           
   17.70 -        !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
   17.71 -     |]  ==>  P(a)"
   17.72 -  unfolding wf_def by blast
   17.73 -
   17.74 -lemmas wfP_induct = wf_induct [to_pred]
   17.75 -
   17.76 -lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
   17.77 -
   17.78 -lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
   17.79 -
   17.80 -lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
   17.81 -  by (induct a arbitrary: x set: wf) blast
   17.82 -
   17.83 -(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
   17.84 -lemmas wf_asym = wf_not_sym [elim_format]
   17.85 -
   17.86 -lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
   17.87 -  by (blast elim: wf_asym)
   17.88 -
   17.89 -(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
   17.90 -lemmas wf_irrefl = wf_not_refl [elim_format]
   17.91 -
   17.92 -text{*transitive closure of a well-founded relation is well-founded! *}
   17.93 -lemma wf_trancl:
   17.94 -  assumes "wf r"
   17.95 -  shows "wf (r^+)"
   17.96 -proof -
   17.97 -  {
   17.98 -    fix P and x
   17.99 -    assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
  17.100 -    have "P x"
  17.101 -    proof (rule induct_step)
  17.102 -      fix y assume "(y, x) : r^+"
  17.103 -      with `wf r` show "P y"
  17.104 -      proof (induct x arbitrary: y)
  17.105 -	case (less x)
  17.106 -	note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
  17.107 -	from `(y, x) : r^+` show "P y"
  17.108 -	proof cases
  17.109 -	  case base
  17.110 -	  show "P y"
  17.111 -	  proof (rule induct_step)
  17.112 -	    fix y' assume "(y', y) : r^+"
  17.113 -	    with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
  17.114 -	  qed
  17.115 -	next
  17.116 -	  case step
  17.117 -	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
  17.118 -	  then show "P y" by (rule hyp [of x' y])
  17.119 -	qed
  17.120 -      qed
  17.121 -    qed
  17.122 -  } then show ?thesis unfolding wf_def by blast
  17.123 -qed
  17.124 -
  17.125 -lemmas wfP_trancl = wf_trancl [to_pred]
  17.126 -
  17.127 -lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
  17.128 -  apply (subst trancl_converse [symmetric])
  17.129 -  apply (erule wf_trancl)
  17.130 -  done
  17.131 -
  17.132 -
  17.133 -subsubsection {* Other simple well-foundedness results *}
  17.134 -
  17.135 -text{*Minimal-element characterization of well-foundedness*}
  17.136 -lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
  17.137 -proof (intro iffI strip)
  17.138 -  fix Q :: "'a set" and x
  17.139 -  assume "wf r" and "x \<in> Q"
  17.140 -  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
  17.141 -    unfolding wf_def
  17.142 -    by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
  17.143 -next
  17.144 -  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
  17.145 -  show "wf r"
  17.146 -  proof (rule wfUNIVI)
  17.147 -    fix P :: "'a \<Rightarrow> bool" and x
  17.148 -    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
  17.149 -    let ?Q = "{x. \<not> P x}"
  17.150 -    have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
  17.151 -      by (rule 1 [THEN spec, THEN spec])
  17.152 -    then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
  17.153 -    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
  17.154 -    then show "P x" by simp
  17.155 -  qed
  17.156 -qed
  17.157 -
  17.158 -lemma wfE_min: 
  17.159 -  assumes "wf R" "x \<in> Q"
  17.160 -  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
  17.161 -  using assms unfolding wf_eq_minimal by blast
  17.162 -
  17.163 -lemma wfI_min:
  17.164 -  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
  17.165 -  \<Longrightarrow> wf R"
  17.166 -  unfolding wf_eq_minimal by blast
  17.167 -
  17.168 -lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
  17.169 -
  17.170 -text {* Well-foundedness of subsets *}
  17.171 -lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
  17.172 -  apply (simp (no_asm_use) add: wf_eq_minimal)
  17.173 -  apply fast
  17.174 -  done
  17.175 -
  17.176 -lemmas wfP_subset = wf_subset [to_pred]
  17.177 -
  17.178 -text {* Well-foundedness of the empty relation *}
  17.179 -lemma wf_empty [iff]: "wf({})"
  17.180 -  by (simp add: wf_def)
  17.181 -
  17.182 -lemmas wfP_empty [iff] =
  17.183 -  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
  17.184 -
  17.185 -lemma wf_Int1: "wf r ==> wf (r Int r')"
  17.186 -  apply (erule wf_subset)
  17.187 -  apply (rule Int_lower1)
  17.188 -  done
  17.189 -
  17.190 -lemma wf_Int2: "wf r ==> wf (r' Int r)"
  17.191 -  apply (erule wf_subset)
  17.192 -  apply (rule Int_lower2)
  17.193 -  done  
  17.194 -
  17.195 -text{*Well-foundedness of insert*}
  17.196 -lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
  17.197 -apply (rule iffI)
  17.198 - apply (blast elim: wf_trancl [THEN wf_irrefl]
  17.199 -              intro: rtrancl_into_trancl1 wf_subset 
  17.200 -                     rtrancl_mono [THEN [2] rev_subsetD])
  17.201 -apply (simp add: wf_eq_minimal, safe)
  17.202 -apply (rule allE, assumption, erule impE, blast) 
  17.203 -apply (erule bexE)
  17.204 -apply (rename_tac "a", case_tac "a = x")
  17.205 - prefer 2
  17.206 -apply blast 
  17.207 -apply (case_tac "y:Q")
  17.208 - prefer 2 apply blast
  17.209 -apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
  17.210 - apply assumption
  17.211 -apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
  17.212 -  --{*essential for speed*}
  17.213 -txt{*Blast with new substOccur fails*}
  17.214 -apply (fast intro: converse_rtrancl_into_rtrancl)
  17.215 -done
  17.216 -
  17.217 -text{*Well-foundedness of image*}
  17.218 -lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
  17.219 -apply (simp only: wf_eq_minimal, clarify)
  17.220 -apply (case_tac "EX p. f p : Q")
  17.221 -apply (erule_tac x = "{p. f p : Q}" in allE)
  17.222 -apply (fast dest: inj_onD, blast)
  17.223 -done
  17.224 -
  17.225 -
  17.226 -subsubsection {* Well-Foundedness Results for Unions *}
  17.227 -
  17.228 -lemma wf_union_compatible:
  17.229 -  assumes "wf R" "wf S"
  17.230 -  assumes "S O R \<subseteq> R"
  17.231 -  shows "wf (R \<union> S)"
  17.232 -proof (rule wfI_min)
  17.233 -  fix x :: 'a and Q 
  17.234 -  let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
  17.235 -  assume "x \<in> Q"
  17.236 -  obtain a where "a \<in> ?Q'"
  17.237 -    by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
  17.238 -  with `wf S`
  17.239 -  obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
  17.240 -  { 
  17.241 -    fix y assume "(y, z) \<in> S"
  17.242 -    then have "y \<notin> ?Q'" by (rule zmin)
  17.243 -
  17.244 -    have "y \<notin> Q"
  17.245 -    proof 
  17.246 -      assume "y \<in> Q"
  17.247 -      with `y \<notin> ?Q'` 
  17.248 -      obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
  17.249 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
  17.250 -      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
  17.251 -      with `z \<in> ?Q'` have "w \<notin> Q" by blast 
  17.252 -      with `w \<in> Q` show False by contradiction
  17.253 -    qed
  17.254 -  }
  17.255 -  with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
  17.256 -qed
  17.257 -
  17.258 -
  17.259 -text {* Well-foundedness of indexed union with disjoint domains and ranges *}
  17.260 -
  17.261 -lemma wf_UN: "[| ALL i:I. wf(r i);  
  17.262 -         ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
  17.263 -      |] ==> wf(UN i:I. r i)"
  17.264 -apply (simp only: wf_eq_minimal, clarify)
  17.265 -apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
  17.266 - prefer 2
  17.267 - apply force 
  17.268 -apply clarify
  17.269 -apply (drule bspec, assumption)  
  17.270 -apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
  17.271 -apply (blast elim!: allE)  
  17.272 -done
  17.273 -
  17.274 -lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
  17.275 -  to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]
  17.276 -
  17.277 -lemma wf_Union: 
  17.278 - "[| ALL r:R. wf r;  
  17.279 -     ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
  17.280 -  |] ==> wf(Union R)"
  17.281 -apply (simp add: Union_def)
  17.282 -apply (blast intro: wf_UN)
  17.283 -done
  17.284 -
  17.285 -(*Intuition: we find an (R u S)-min element of a nonempty subset A
  17.286 -             by case distinction.
  17.287 -  1. There is a step a -R-> b with a,b : A.
  17.288 -     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
  17.289 -     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
  17.290 -     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
  17.291 -     have an S-successor and is thus S-min in A as well.
  17.292 -  2. There is no such step.
  17.293 -     Pick an S-min element of A. In this case it must be an R-min
  17.294 -     element of A as well.
  17.295 -
  17.296 -*)
  17.297 -lemma wf_Un:
  17.298 -     "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
  17.299 -  using wf_union_compatible[of s r] 
  17.300 -  by (auto simp: Un_ac)
  17.301 -
  17.302 -lemma wf_union_merge: 
  17.303 -  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
  17.304 -proof
  17.305 -  assume "wf ?A"
  17.306 -  with wf_trancl have wfT: "wf (?A^+)" .
  17.307 -  moreover have "?B \<subseteq> ?A^+"
  17.308 -    by (subst trancl_unfold, subst trancl_unfold) blast
  17.309 -  ultimately show "wf ?B" by (rule wf_subset)
  17.310 -next
  17.311 -  assume "wf ?B"
  17.312 -
  17.313 -  show "wf ?A"
  17.314 -  proof (rule wfI_min)
  17.315 -    fix Q :: "'a set" and x 
  17.316 -    assume "x \<in> Q"
  17.317 -
  17.318 -    with `wf ?B`
  17.319 -    obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
  17.320 -      by (erule wfE_min)
  17.321 -    then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
  17.322 -      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
  17.323 -      and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
  17.324 -      by auto
  17.325 -    
  17.326 -    show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
  17.327 -    proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
  17.328 -      case True
  17.329 -      with `z \<in> Q` A3 show ?thesis by blast
  17.330 -    next
  17.331 -      case False 
  17.332 -      then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
  17.333 -
  17.334 -      have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
  17.335 -      proof (intro allI impI)
  17.336 -        fix y assume "(y, z') \<in> ?A"
  17.337 -        then show "y \<notin> Q"
  17.338 -        proof
  17.339 -          assume "(y, z') \<in> R" 
  17.340 -          then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
  17.341 -          with A1 show "y \<notin> Q" .
  17.342 -        next
  17.343 -          assume "(y, z') \<in> S" 
  17.344 -          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
  17.345 -          with A2 show "y \<notin> Q" .
  17.346 -        qed
  17.347 -      qed
  17.348 -      with `z' \<in> Q` show ?thesis ..
  17.349 -    qed
  17.350 -  qed
  17.351 -qed
  17.352 -
  17.353 -lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
  17.354 -  by (rule wf_union_merge [where S = "{}", simplified])
  17.355 -
  17.356 -
  17.357 -subsubsection {* acyclic *}
  17.358 -
  17.359 -lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
  17.360 -  by (simp add: acyclic_def)
  17.361 -
  17.362 -lemma wf_acyclic: "wf r ==> acyclic r"
  17.363 -apply (simp add: acyclic_def)
  17.364 -apply (blast elim: wf_trancl [THEN wf_irrefl])
  17.365 -done
  17.366 -
  17.367 -lemmas wfP_acyclicP = wf_acyclic [to_pred]
  17.368 -
  17.369 -lemma acyclic_insert [iff]:
  17.370 -     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
  17.371 -apply (simp add: acyclic_def trancl_insert)
  17.372 -apply (blast intro: rtrancl_trans)
  17.373 -done
  17.374 -
  17.375 -lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
  17.376 -by (simp add: acyclic_def trancl_converse)
  17.377 -
  17.378 -lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
  17.379 -
  17.380 -lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
  17.381 -apply (simp add: acyclic_def antisym_def)
  17.382 -apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
  17.383 -done
  17.384 -
  17.385 -(* Other direction:
  17.386 -acyclic = no loops
  17.387 -antisym = only self loops
  17.388 -Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
  17.389 -==> antisym( r^* ) = acyclic(r - Id)";
  17.390 -*)
  17.391 -
  17.392 -lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
  17.393 -apply (simp add: acyclic_def)
  17.394 -apply (blast intro: trancl_mono)
  17.395 -done
  17.396 -
  17.397 -
  17.398 -subsection{*Well-Founded Recursion*}
  17.399 -
  17.400 -text{*cut*}
  17.401 -
  17.402 -lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
  17.403 -by (simp add: expand_fun_eq cut_def)
  17.404 -
  17.405 -lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
  17.406 -by (simp add: cut_def)
  17.407 -
  17.408 -text{*Inductive characterization of wfrec combinator; for details see:  
  17.409 -John Harrison, "Inductive definitions: automation and application"*}
  17.410 -
  17.411 -lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
  17.412 -apply (simp add: adm_wf_def)
  17.413 -apply (erule_tac a=x in wf_induct) 
  17.414 -apply (rule ex1I)
  17.415 -apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
  17.416 -apply (fast dest!: theI')
  17.417 -apply (erule wfrec_rel.cases, simp)
  17.418 -apply (erule allE, erule allE, erule allE, erule mp)
  17.419 -apply (fast intro: the_equality [symmetric])
  17.420 -done
  17.421 -
  17.422 -lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
  17.423 -apply (simp add: adm_wf_def)
  17.424 -apply (intro strip)
  17.425 -apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
  17.426 -apply (rule refl)
  17.427 -done
  17.428 -
  17.429 -lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
  17.430 -apply (simp add: wfrec_def)
  17.431 -apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
  17.432 -apply (rule wfrec_rel.wfrecI)
  17.433 -apply (intro strip)
  17.434 -apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
  17.435 -done
  17.436 -
  17.437 -
  17.438 -text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
  17.439 -lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
  17.440 -apply auto
  17.441 -apply (blast intro: wfrec)
  17.442 -done
  17.443 -
  17.444 -
  17.445 -subsection {* Code generator setup *}
  17.446 -
  17.447 -consts_code
  17.448 -  "wfrec"   ("\<module>wfrec?")
  17.449 -attach {*
  17.450 -fun wfrec f x = f (wfrec f) x;
  17.451 -*}
  17.452 -
  17.453 -
  17.454 -subsection{*Variants for TFL: the Recdef Package*}
  17.455 -
  17.456 -lemma tfl_wf_induct: "ALL R. wf R -->  
  17.457 -       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
  17.458 -apply clarify
  17.459 -apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
  17.460 -done
  17.461 -
  17.462 -lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
  17.463 -apply clarify
  17.464 -apply (rule cut_apply, assumption)
  17.465 -done
  17.466 -
  17.467 -lemma tfl_wfrec:
  17.468 -     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
  17.469 -apply clarify
  17.470 -apply (erule wfrec)
  17.471 -done
  17.472 -
  17.473 -subsection {*LEAST and wellorderings*}
  17.474 -
  17.475 -text{* See also @{text wf_linord_ex_has_least} and its consequences in
  17.476 - @{text Wellfounded_Relations.ML}*}
  17.477 -
  17.478 -lemma wellorder_Least_lemma [rule_format]:
  17.479 -     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
  17.480 -apply (rule_tac a = k in wf [THEN wf_induct])
  17.481 -apply (rule impI)
  17.482 -apply (rule classical)
  17.483 -apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
  17.484 -apply (auto simp add: linorder_not_less [symmetric])
  17.485 -done
  17.486 -
  17.487 -lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
  17.488 -lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
  17.489 -
  17.490 --- "The following 3 lemmas are due to Brian Huffman"
  17.491 -lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
  17.492 -apply (erule exE)
  17.493 -apply (erule LeastI)
  17.494 -done
  17.495 -
  17.496 -lemma LeastI2:
  17.497 -  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
  17.498 -by (blast intro: LeastI)
  17.499 -
  17.500 -lemma LeastI2_ex:
  17.501 -  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
  17.502 -by (blast intro: LeastI_ex)
  17.503 -
  17.504 -lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
  17.505 -apply (simp (no_asm_use) add: linorder_not_le [symmetric])
  17.506 -apply (erule contrapos_nn)
  17.507 -apply (erule Least_le)
  17.508 -done
  17.509 -
  17.510 -subsection {* @{typ nat} is well-founded *}
  17.511 -
  17.512 -lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
  17.513 -proof (rule ext, rule ext, rule iffI)
  17.514 -  fix n m :: nat
  17.515 -  assume "m < n"
  17.516 -  then show "(\<lambda>m n. n = Suc m)^++ m n"
  17.517 -  proof (induct n)
  17.518 -    case 0 then show ?case by auto
  17.519 -  next
  17.520 -    case (Suc n) then show ?case
  17.521 -      by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
  17.522 -  qed
  17.523 -next
  17.524 -  fix n m :: nat
  17.525 -  assume "(\<lambda>m n. n = Suc m)^++ m n"
  17.526 -  then show "m < n"
  17.527 -    by (induct n)
  17.528 -      (simp_all add: less_Suc_eq_le reflexive le_less)
  17.529 -qed
  17.530 -
  17.531 -definition
  17.532 -  pred_nat :: "(nat * nat) set" where
  17.533 -  "pred_nat = {(m, n). n = Suc m}"
  17.534 -
  17.535 -definition
  17.536 -  less_than :: "(nat * nat) set" where
  17.537 -  "less_than = pred_nat^+"
  17.538 -
  17.539 -lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
  17.540 -  unfolding less_nat_rel pred_nat_def trancl_def by simp
  17.541 -
  17.542 -lemma pred_nat_trancl_eq_le:
  17.543 -  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
  17.544 -  unfolding less_eq rtrancl_eq_or_trancl by auto
  17.545 -
  17.546 -lemma wf_pred_nat: "wf pred_nat"
  17.547 -  apply (unfold wf_def pred_nat_def, clarify)
  17.548 -  apply (induct_tac x, blast+)
  17.549 -  done
  17.550 -
  17.551 -lemma wf_less_than [iff]: "wf less_than"
  17.552 -  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
  17.553 -
  17.554 -lemma trans_less_than [iff]: "trans less_than"
  17.555 -  by (simp add: less_than_def trans_trancl)
  17.556 -
  17.557 -lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
  17.558 -  by (simp add: less_than_def less_eq)
  17.559 -
  17.560 -lemma wf_less: "wf {(x, y::nat). x < y}"
  17.561 -  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
  17.562 -
  17.563 -text {* Complete induction, aka course-of-values induction *}
  17.564 -lemma nat_less_induct:
  17.565 -  assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
  17.566 -  apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
  17.567 -  apply (rule assms)
  17.568 -  apply (unfold less_eq [symmetric], assumption)
  17.569 -  done
  17.570 -
  17.571 -lemmas less_induct = nat_less_induct [rule_format, case_names less]
  17.572 -
  17.573 -text {* Type @{typ nat} is a wellfounded order *}
  17.574 -
  17.575 -instance nat :: wellorder
  17.576 -  by intro_classes
  17.577 -    (assumption |
  17.578 -      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
  17.579 -
  17.580 -lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
  17.581 -  apply (rule nat_less_induct)
  17.582 -  apply (case_tac n)
  17.583 -  apply (case_tac [2] nat)
  17.584 -  apply (blast intro: less_trans)+
  17.585 -  done
  17.586 -
  17.587 -text {* The method of infinite descent, frequently used in number theory.
  17.588 -Provided by Roelof Oosterhuis.
  17.589 -$P(n)$ is true for all $n\in\mathbb{N}$ if
  17.590 -\begin{itemize}
  17.591 -  \item case ``0'': given $n=0$ prove $P(n)$,
  17.592 -  \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
  17.593 -        a smaller integer $m$ such that $\neg P(m)$.
  17.594 -\end{itemize} *}
  17.595 -
  17.596 -lemma infinite_descent0[case_names 0 smaller]: 
  17.597 -  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
  17.598 -by (induct n rule: less_induct, case_tac "n>0", auto)
  17.599 -
  17.600 -text{* A compact version without explicit base case: *}
  17.601 -lemma infinite_descent:
  17.602 -  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
  17.603 -by (induct n rule: less_induct, auto)
  17.604 -
  17.605 -text {*
  17.606 -Infinite descent using a mapping to $\mathbb{N}$:
  17.607 -$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
  17.608 -\begin{itemize}
  17.609 -\item case ``0'': given $V(x)=0$ prove $P(x)$,
  17.610 -\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
  17.611 -\end{itemize}
  17.612 -NB: the proof also shows how to use the previous lemma. *}
  17.613 -
  17.614 -corollary infinite_descent0_measure [case_names 0 smaller]:
  17.615 -  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
  17.616 -    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
  17.617 -  shows "P x"
  17.618 -proof -
  17.619 -  obtain n where "n = V x" by auto
  17.620 -  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  17.621 -  proof (induct n rule: infinite_descent0)
  17.622 -    case 0 -- "i.e. $V(x) = 0$"
  17.623 -    with A0 show "P x" by auto
  17.624 -  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  17.625 -    case (smaller n)
  17.626 -    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  17.627 -    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  17.628 -    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  17.629 -    then show ?case by auto
  17.630 -  qed
  17.631 -  ultimately show "P x" by auto
  17.632 -qed
  17.633 -
  17.634 -text{* Again, without explicit base case: *}
  17.635 -lemma infinite_descent_measure:
  17.636 -assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  17.637 -proof -
  17.638 -  from assms obtain n where "n = V x" by auto
  17.639 -  moreover have "!!x. V x = n \<Longrightarrow> P x"
  17.640 -  proof (induct n rule: infinite_descent, auto)
  17.641 -    fix x assume "\<not> P x"
  17.642 -    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  17.643 -  qed
  17.644 -  ultimately show "P x" by auto
  17.645 -qed
  17.646 -
  17.647 -text {* @{text LEAST} theorems for type @{typ nat}*}
  17.648 -
  17.649 -lemma Least_Suc:
  17.650 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  17.651 -  apply (case_tac "n", auto)
  17.652 -  apply (frule LeastI)
  17.653 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
  17.654 -  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
  17.655 -  apply (erule_tac [2] Least_le)
  17.656 -  apply (case_tac "LEAST x. P x", auto)
  17.657 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
  17.658 -  apply (blast intro: order_antisym)
  17.659 -  done
  17.660 -
  17.661 -lemma Least_Suc2:
  17.662 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
  17.663 -  apply (erule (1) Least_Suc [THEN ssubst])
  17.664 -  apply simp
  17.665 -  done
  17.666 -
  17.667 -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)"
  17.668 -  apply (cases n)
  17.669 -   apply blast
  17.670 -  apply (rule_tac x="LEAST k. P(k)" in exI)
  17.671 -  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
  17.672 -  done
  17.673 -
  17.674 -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)"
  17.675 -  apply (cases n)
  17.676 -   apply blast
  17.677 -  apply (frule (1) ex_least_nat_le)
  17.678 -  apply (erule exE)
  17.679 -  apply (case_tac k)
  17.680 -   apply simp
  17.681 -  apply (rename_tac k1)
  17.682 -  apply (rule_tac x=k1 in exI)
  17.683 -  apply fastsimp
  17.684 -  done
  17.685 -
  17.686 -
  17.687 -subsection {* size of a datatype value *}
  17.688 -
  17.689 -use "Tools/function_package/size.ML"
  17.690 -
  17.691 -setup Size.setup
  17.692 -
  17.693 -lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  17.694 -  by (induct n) simp_all
  17.695 -
  17.696 -end
    18.1 --- a/src/HOL/Wellfounded_Relations.thy	Thu Apr 24 16:53:04 2008 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,269 +0,0 @@
    18.4 -(*  ID:   $Id$
    18.5 -    Author:     Konrad Slind
    18.6 -    Copyright   1995 TU Munich
    18.7 -*)
    18.8 -
    18.9 -header {*Well-founded Relations*}
   18.10 -
   18.11 -theory Wellfounded_Relations
   18.12 -imports Finite_Set FunDef
   18.13 -uses
   18.14 -  ("Tools/function_package/lexicographic_order.ML")
   18.15 -  ("Tools/function_package/fundef_datatype.ML")
   18.16 -begin
   18.17 -
   18.18 -text{*Derived WF relations such as inverse image, lexicographic product and
   18.19 -measure. The simple relational product, in which @{term "(x',y')"} precedes
   18.20 -@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
   18.21 -lexicographic product, and therefore does not need to be defined separately.*}
   18.22 -
   18.23 -constdefs
   18.24 - measure   :: "('a => nat) => ('a * 'a)set"
   18.25 -    "measure == inv_image less_than"
   18.26 -
   18.27 - lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
   18.28 -               (infixr "<*lex*>" 80)
   18.29 -    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
   18.30 -
   18.31 - finite_psubset  :: "('a set * 'a set) set"
   18.32 -   --{* finite proper subset*}
   18.33 -    "finite_psubset == {(A,B). A < B & finite B}"
   18.34 -
   18.35 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   18.36 -    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   18.37 -   --{*For @{text rec_def} declarations where the first n parameters
   18.38 -       stay unchanged in the recursive call. 
   18.39 -       See @{text "Library/While_Combinator.thy"} for an application.*}
   18.40 -
   18.41 -
   18.42 -subsection{*Measure Functions make Wellfounded Relations*}
   18.43 -
   18.44 -subsubsection{*`Less than' on the natural numbers*}
   18.45 -
   18.46 -lemma full_nat_induct:
   18.47 -  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
   18.48 -  shows "P n"
   18.49 -apply (rule wf_less_than [THEN wf_induct])
   18.50 -apply (rule ih, auto)
   18.51 -done
   18.52 -
   18.53 -subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
   18.54 -
   18.55 -lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
   18.56 -apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
   18.57 -apply clarify
   18.58 -apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
   18.59 -prefer 2 apply (blast del: allE)
   18.60 -apply (erule allE)
   18.61 -apply (erule (1) notE impE)
   18.62 -apply blast
   18.63 -done
   18.64 -
   18.65 -lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   18.66 -  by (auto simp:inv_image_def)
   18.67 -
   18.68 -subsubsection{*Finally, All Measures are Wellfounded.*}
   18.69 -
   18.70 -lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   18.71 -  by (simp add:measure_def)
   18.72 -
   18.73 -lemma wf_measure [iff]: "wf (measure f)"
   18.74 -apply (unfold measure_def)
   18.75 -apply (rule wf_less_than [THEN wf_inv_image])
   18.76 -done
   18.77 -
   18.78 -lemma measure_induct_rule [case_names less]:
   18.79 -  fixes f :: "'a \<Rightarrow> nat"
   18.80 -  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
   18.81 -  shows "P a"
   18.82 -proof -
   18.83 -  have "wf (measure f)" ..
   18.84 -  then show ?thesis
   18.85 -  proof induct
   18.86 -    case (less x)
   18.87 -    show ?case
   18.88 -    proof (rule step)
   18.89 -      fix y
   18.90 -      assume "f y < f x"
   18.91 -      hence "(y, x) \<in> measure f" by simp
   18.92 -      thus "P y" by (rule less)
   18.93 -    qed
   18.94 -  qed
   18.95 -qed
   18.96 -
   18.97 -lemma measure_induct:
   18.98 -  fixes f :: "'a \<Rightarrow> nat"
   18.99 -  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
  18.100 -  by (rule measure_induct_rule [of f P a]) iprover
  18.101 -
  18.102 -(* Should go into Finite_Set, but needs measure.
  18.103 -   Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set?
  18.104 -*)
  18.105 -lemma (in linorder)
  18.106 -  finite_linorder_induct[consumes 1, case_names empty insert]:
  18.107 - "finite A \<Longrightarrow> P {} \<Longrightarrow>
  18.108 -  (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
  18.109 -  \<Longrightarrow> P A"
  18.110 -proof (induct A rule: measure_induct[where f=card])
  18.111 -  fix A :: "'a set"
  18.112 -  assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
  18.113 -                 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a<b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
  18.114 -                  \<longrightarrow> P B"
  18.115 -  and "finite A" and "P {}"
  18.116 -  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
  18.117 -  show "P A"
  18.118 -  proof cases
  18.119 -    assume "A = {}" thus "P A" using `P {}` by simp
  18.120 -  next
  18.121 -    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
  18.122 -    assume "A \<noteq> {}"
  18.123 -    with `finite A` have "Max A : A" by auto
  18.124 -    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
  18.125 -    note card_Diff1_less[OF `finite A` `Max A : A`]
  18.126 -    moreover have "finite ?B" using `finite A` by simp
  18.127 -    ultimately have "P ?B" using `P {}` step IH by blast
  18.128 -    moreover have "\<forall>a\<in>?B. a < Max A"
  18.129 -      using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
  18.130 -    ultimately show "P A"
  18.131 -      using A insert_Diff_single step[OF `finite ?B`] by fastsimp
  18.132 -  qed
  18.133 -qed
  18.134 -
  18.135 -
  18.136 -subsection{*Other Ways of Constructing Wellfounded Relations*}
  18.137 -
  18.138 -text{*Wellfoundedness of lexicographic combinations*}
  18.139 -lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
  18.140 -apply (unfold wf_def lex_prod_def) 
  18.141 -apply (rule allI, rule impI)
  18.142 -apply (simp (no_asm_use) only: split_paired_All)
  18.143 -apply (drule spec, erule mp) 
  18.144 -apply (rule allI, rule impI)
  18.145 -apply (drule spec, erule mp, blast) 
  18.146 -done
  18.147 -
  18.148 -lemma in_lex_prod[simp]: 
  18.149 -  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
  18.150 -  by (auto simp:lex_prod_def)
  18.151 -
  18.152 -text {* lexicographic combinations with measure functions *}
  18.153 -
  18.154 -definition 
  18.155 -  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
  18.156 -where
  18.157 -  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
  18.158 -
  18.159 -lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
  18.160 -unfolding mlex_prod_def
  18.161 -by auto
  18.162 -
  18.163 -lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
  18.164 -unfolding mlex_prod_def by simp
  18.165 -
  18.166 -lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
  18.167 -unfolding mlex_prod_def by auto
  18.168 -
  18.169 -
  18.170 -text{*Transitivity of WF combinators.*}
  18.171 -lemma trans_lex_prod [intro!]: 
  18.172 -    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
  18.173 -by (unfold trans_def lex_prod_def, blast) 
  18.174 -
  18.175 -subsubsection{*Wellfoundedness of proper subset on finite sets.*}
  18.176 -lemma wf_finite_psubset: "wf(finite_psubset)"
  18.177 -apply (unfold finite_psubset_def)
  18.178 -apply (rule wf_measure [THEN wf_subset])
  18.179 -apply (simp add: measure_def inv_image_def less_than_def less_eq)
  18.180 -apply (fast elim!: psubset_card_mono)
  18.181 -done
  18.182 -
  18.183 -lemma trans_finite_psubset: "trans finite_psubset"
  18.184 -by (simp add: finite_psubset_def psubset_def trans_def, blast)
  18.185 -
  18.186 -
  18.187 -subsubsection{*Wellfoundedness of finite acyclic relations*}
  18.188 -
  18.189 -text{*This proof belongs in this theory because it needs Finite.*}
  18.190 -
  18.191 -lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
  18.192 -apply (erule finite_induct, blast)
  18.193 -apply (simp (no_asm_simp) only: split_tupled_all)
  18.194 -apply simp
  18.195 -done
  18.196 -
  18.197 -lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
  18.198 -apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
  18.199 -apply (erule acyclic_converse [THEN iffD2])
  18.200 -done
  18.201 -
  18.202 -lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
  18.203 -by (blast intro: finite_acyclic_wf wf_acyclic)
  18.204 -
  18.205 -
  18.206 -subsubsection{*Wellfoundedness of @{term same_fst}*}
  18.207 -
  18.208 -lemma same_fstI [intro!]:
  18.209 -     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
  18.210 -by (simp add: same_fst_def)
  18.211 -
  18.212 -lemma wf_same_fst:
  18.213 -  assumes prem: "(!!x. P x ==> wf(R x))"
  18.214 -  shows "wf(same_fst P R)"
  18.215 -apply (simp cong del: imp_cong add: wf_def same_fst_def)
  18.216 -apply (intro strip)
  18.217 -apply (rename_tac a b)
  18.218 -apply (case_tac "wf (R a)")
  18.219 - apply (erule_tac a = b in wf_induct, blast)
  18.220 -apply (blast intro: prem)
  18.221 -done
  18.222 -
  18.223 -
  18.224 -subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
  18.225 -   stabilize.*}
  18.226 -
  18.227 -text{*This material does not appear to be used any longer.*}
  18.228 -
  18.229 -lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
  18.230 -apply (induct_tac "k", simp_all)
  18.231 -apply (blast intro: rtrancl_trans)
  18.232 -done
  18.233 -
  18.234 -lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
  18.235 -      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
  18.236 -apply (erule wf_induct, clarify)
  18.237 -apply (case_tac "EX j. (f (m+j), f m) : r^+")
  18.238 - apply clarify
  18.239 - apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
  18.240 -  apply clarify
  18.241 -  apply (rule_tac x = "j+i" in exI)
  18.242 -  apply (simp add: add_ac, blast)
  18.243 -apply (rule_tac x = 0 in exI, clarsimp)
  18.244 -apply (drule_tac i = m and k = k in lemma1)
  18.245 -apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
  18.246 -done
  18.247 -
  18.248 -lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
  18.249 -      ==> EX i. ALL k. f (i+k) = f i"
  18.250 -apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
  18.251 -done
  18.252 -
  18.253 -(* special case of the theorem above: <= *)
  18.254 -lemma weak_decr_stable:
  18.255 -     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
  18.256 -apply (rule_tac r = pred_nat in wf_weak_decr_stable)
  18.257 -apply (simp add: pred_nat_trancl_eq_le)
  18.258 -apply (intro wf_trancl wf_pred_nat)
  18.259 -done
  18.260 -
  18.261 -
  18.262 -text {*
  18.263 -  Setup of @{text lexicographic_order} method
  18.264 -  and @{text fun} command
  18.265 -*}
  18.266 -
  18.267 -use "Tools/function_package/lexicographic_order.ML"
  18.268 -use "Tools/function_package/fundef_datatype.ML"
  18.269 -
  18.270 -setup "LexicographicOrder.setup #> FundefDatatype.setup"
  18.271 -
  18.272 -end