# HG changeset patch # User krauss # Date 1209130233 -7200 # Node ID 4d51ddd6aa5c51cae7d94ed4fb3f74b13a464b69 # Parent f32fa5f5bdd12d27b8338112593112bde1fca5e2 Merged theories about wellfoundedness into one: Wellfounded.thy diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c NEWS --- a/NEWS Thu Apr 24 16:53:04 2008 +0200 +++ b/NEWS Fri Apr 25 15:30:33 2008 +0200 @@ -100,6 +100,9 @@ *** HOL *** +* Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations + to "Wellfounded.thy" + * Explicit class "eq" for executable equality. INCOMPATIBILITY. * Class finite no longer treats UNIV as class parameter. Use class enum from diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Accessible_Part.thy --- a/src/HOL/Accessible_Part.thy Thu Apr 24 16:53:04 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,167 +0,0 @@ -(* Title: HOL/Accessible_Part.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge -*) - -header {* The accessible part of a relation *} - -theory Accessible_Part -imports Wellfounded_Recursion -begin - -subsection {* Inductive definition *} - -text {* - Inductive definition of the accessible part @{term "acc r"} of a - relation; see also \cite{paulin-tlca}. -*} - -inductive_set - acc :: "('a * 'a) set => 'a set" - for r :: "('a * 'a) set" - where - accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" - -abbreviation - termip :: "('a => 'a => bool) => 'a => bool" where - "termip r == accp (r\\)" - -abbreviation - termi :: "('a * 'a) set => 'a set" where - "termi r == acc (r\)" - -lemmas accpI = accp.accI - -subsection {* Induction rules *} - -theorem accp_induct: - assumes major: "accp r a" - assumes hyp: "!!x. accp r x ==> \y. r y x --> P y ==> P x" - shows "P a" - apply (rule major [THEN accp.induct]) - apply (rule hyp) - apply (rule accp.accI) - apply fast - apply fast - done - -theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] - -theorem accp_downward: "accp r b ==> r a b ==> accp r a" - apply (erule accp.cases) - apply fast - done - -lemma not_accp_down: - assumes na: "\ accp R x" - obtains z where "R z x" and "\ accp R z" -proof - - assume a: "\z. \R z x; \ accp R z\ \ thesis" - - show thesis - proof (cases "\z. R z x \ accp R z") - case True - hence "\z. R z x \ accp R z" by auto - hence "accp R x" - by (rule accp.accI) - with na show thesis .. - next - case False then obtain z where "R z x" and "\ accp R z" - by auto - with a show thesis . - qed -qed - -lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b" - apply (erule rtranclp_induct) - apply blast - apply (blast dest: accp_downward) - done - -theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b" - apply (blast dest: accp_downwards_aux) - done - -theorem accp_wfPI: "\x. accp r x ==> wfP r" - apply (rule wfPUNIVI) - apply (induct_tac P x rule: accp_induct) - apply blast - apply blast - done - -theorem accp_wfPD: "wfP r ==> accp r x" - apply (erule wfP_induct_rule) - apply (rule accp.accI) - apply blast - done - -theorem wfP_accp_iff: "wfP r = (\x. accp r x)" - apply (blast intro: accp_wfPI dest: accp_wfPD) - done - - -text {* Smaller relations have bigger accessible parts: *} - -lemma accp_subset: - assumes sub: "R1 \ R2" - shows "accp R2 \ accp R1" -proof - fix x assume "accp R2 x" - then show "accp R1 x" - proof (induct x) - fix x - assume ih: "\y. R2 y x \ accp R1 y" - with sub show "accp R1 x" - by (blast intro: accp.accI) - qed -qed - - -text {* This is a generalized induction theorem that works on - subsets of the accessible part. *} - -lemma accp_subset_induct: - assumes subset: "D \ accp R" - and dcl: "\x z. \D x; R z x\ \ D z" - and "D x" - and istep: "\x. \D x; (\z. R z x \ P z)\ \ P x" - shows "P x" -proof - - from subset and `D x` - have "accp R x" .. - then show "P x" using `D x` - proof (induct x) - fix x - assume "D x" - and "\y. R y x \ D y \ P y" - with dcl and istep show "P x" by blast - qed -qed - - -text {* Set versions of the above theorems *} - -lemmas acc_induct = accp_induct [to_set] - -lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] - -lemmas acc_downward = accp_downward [to_set] - -lemmas not_acc_down = not_accp_down [to_set] - -lemmas acc_downwards_aux = accp_downwards_aux [to_set] - -lemmas acc_downwards = accp_downwards [to_set] - -lemmas acc_wfI = accp_wfPI [to_set] - -lemmas acc_wfD = accp_wfPD [to_set] - -lemmas wf_acc_iff = wfP_accp_iff [to_set] - -lemmas acc_subset = accp_subset [to_set] - -lemmas acc_subset_induct = accp_subset_induct [to_set] - -end diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Datatype.thy Fri Apr 25 15:30:33 2008 +0200 @@ -9,7 +9,7 @@ header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} theory Datatype -imports Finite_Set +imports Finite_Set Wellfounded begin lemma size_bool [code func]: diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Divides.thy Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ header {* The division operators div, mod and the divides relation dvd *} theory Divides -imports Nat Power Product_Type Wellfounded_Recursion +imports Nat Power Product_Type uses "~~/src/Provers/Arith/cancel_div_mod.ML" begin diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Finite_Set.thy Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ header {* Finite sets *} theory Finite_Set -imports Divides +imports Divides Transitive_Closure begin subsection {* Definition and basic properties *} @@ -2639,6 +2639,35 @@ by (simp add: Max fold1_antimono [folded dual_max]) qed +lemma finite_linorder_induct[consumes 1, case_names empty insert]: + "finite A \ P {} \ + (!!A b. finite A \ ALL a:A. a < b \ P A \ P(insert b A)) + \ P A" +proof (induct A rule: measure_induct_rule[where f=card]) + fix A :: "'a set" + assume IH: "!! B. card B < card A \ finite B \ P {} \ + (!!A b. finite A \ (\a\A. a P A \ P (insert b A)) + \ P B" + and "finite A" and "P {}" + and step: "!!A b. \finite A; \a\A. a < b; P A\ \ P (insert b A)" + show "P A" + proof cases + assume "A = {}" thus "P A" using `P {}` by simp + next + let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B" + assume "A \ {}" + with `finite A` have "Max A : A" by auto + hence A: "?A = A" using insert_Diff_single insert_absorb by auto + note card_Diff1_less[OF `finite A` `Max A : A`] + moreover have "finite ?B" using `finite A` by simp + ultimately have "P ?B" using `P {}` step IH by blast + moreover have "\a\?B. a < Max A" + using Max_ge[OF `finite A` `A \ {}`] by fastsimp + ultimately show "P A" + using A insert_Diff_single step[OF `finite ?B`] by fastsimp + qed +qed + end context ordered_ab_semigroup_add diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/FunDef.thy Fri Apr 25 15:30:33 2008 +0200 @@ -6,7 +6,7 @@ header {* General recursive function definitions *} theory FunDef -imports Accessible_Part +imports Wellfounded uses ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/fundef_common.ML") @@ -19,6 +19,8 @@ ("Tools/function_package/fundef_package.ML") ("Tools/function_package/auto_term.ML") ("Tools/function_package/induction_scheme.ML") + ("Tools/function_package/lexicographic_order.ML") + ("Tools/function_package/fundef_datatype.ML") begin text {* Definitions with default value. *} @@ -106,10 +108,14 @@ use "Tools/function_package/auto_term.ML" use "Tools/function_package/fundef_package.ML" use "Tools/function_package/induction_scheme.ML" +use "Tools/function_package/lexicographic_order.ML" +use "Tools/function_package/fundef_datatype.ML" setup {* FundefPackage.setup #> InductionScheme.setup + #> LexicographicOrder.setup + #> FundefDatatype.setup *} lemma let_cong [fundef_cong]: diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} theory Hilbert_Choice -imports Nat Wellfounded_Recursion +imports Nat Wellfounded uses ("Tools/meson.ML") ("Tools/specification_package.ML") begin diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Int.thy --- a/src/HOL/Int.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Int.thy Fri Apr 25 15:30:33 2008 +0200 @@ -9,7 +9,7 @@ header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} theory Int -imports Equiv_Relations Nat Wellfounded_Relations +imports Equiv_Relations Nat Wellfounded uses ("Tools/numeral.ML") ("Tools/numeral_syntax.ML") diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/IsaMakefile Fri Apr 25 15:30:33 2008 +0200 @@ -92,7 +92,7 @@ $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML \ $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \ $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ - Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy \ + Arith_Tools.thy Code_Setup.thy Datatype.thy \ Divides.thy Equiv_Relations.thy Extraction.thy \ Finite_Set.thy Fun.thy FunDef.thy HOL.thy \ Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \ @@ -142,8 +142,8 @@ Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML \ Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML \ Tools/typedef_codegen.ML Tools/typedef_package.ML \ - Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \ - Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \ + Transitive_Closure.thy Typedef.thy Wellfounded.thy \ + arith_data.ML document/root.tex hologic.ML \ int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Lambda/ROOT.ML --- a/src/HOL/Lambda/ROOT.ML Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Lambda/ROOT.ML Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ Syntax.ambiguity_level := 100; Proofterm.proofs := 2; -no_document use_thys ["Accessible_Part", "Code_Integer"]; +no_document use_thys ["Code_Integer"]; use_thys ["Eta", "StrongNorm", "Standardization"]; if HOL_proofs < 2 then warning "HOL proof terms required for running theory WeakNorm" diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Nat.thy Fri Apr 25 15:30:33 2008 +0200 @@ -734,7 +734,55 @@ by simp -subsubsection {* Additional theorems about "less than" *} +subsubsection {* Additional theorems about @{term "op \"} *} + +text {* Complete induction, aka course-of-values induction *} + +lemma less_induct [case_names less]: + fixes P :: "nat \ bool" + assumes step: "\x. (\y. y < x \ P y) \ P x" + shows "P a" +proof - + have "\z. z\a \ P z" + proof (induct a) + case (0 z) + have "P 0" by (rule step) auto + thus ?case using 0 by auto + next + case (Suc x z) + then have "z \ x \ z = Suc x" by (simp add: le_Suc_eq) + thus ?case + proof + assume "z \ x" thus "P z" by (rule Suc(1)) + next + assume z: "z = Suc x" + show "P z" + by (rule step) (rule Suc(1), simp add: z le_simps) + qed + qed + thus ?thesis by auto +qed + +lemma nat_less_induct: + assumes "!!n. \m::nat. m < n --> P m ==> P n" shows "P n" + using assms less_induct by blast + +lemma measure_induct_rule [case_names less]: + fixes f :: "'a \ nat" + assumes step: "\x. (\y. f y < f x \ P y) \ P x" + shows "P a" +by (induct m\"f a" arbitrary: a rule: less_induct) (auto intro: step) + +text {* old style induction rules: *} +lemma measure_induct: + fixes f :: "'a \ nat" + shows "(\x. \y. f y < f x \ P y \ P x) \ P a" + by (rule measure_induct_rule [of f P a]) iprover + +lemma full_nat_induct: + assumes step: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)" + shows "P n" + by (rule less_induct) (auto intro: step simp:le_simps) text{*An induction rule for estabilishing binary relations*} lemma less_Suc_induct: @@ -755,6 +803,73 @@ thus "P i j" by (simp add: j) qed +lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n" + apply (rule nat_less_induct) + apply (case_tac n) + apply (case_tac [2] nat) + apply (blast intro: less_trans)+ + done + +text {* The method of infinite descent, frequently used in number theory. +Provided by Roelof Oosterhuis. +$P(n)$ is true for all $n\in\mathbb{N}$ if +\begin{itemize} + \item case ``0'': given $n=0$ prove $P(n)$, + \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists + a smaller integer $m$ such that $\neg P(m)$. +\end{itemize} *} + +text{* A compact version without explicit base case: *} +lemma infinite_descent: + "\ !!n::nat. \ P n \ \m P m \ \ P n" +by (induct n rule: less_induct, auto) + +lemma infinite_descent0[case_names 0 smaller]: + "\ P 0; !!n. n>0 \ \ P n \ (\m::nat. m < n \ \P m) \ \ P n" +by (rule infinite_descent) (case_tac "n>0", auto) + +text {* +Infinite descent using a mapping to $\mathbb{N}$: +$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and +\begin{itemize} +\item case ``0'': given $V(x)=0$ prove $P(x)$, +\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y) P x" + and A1: "!!x. V x > 0 \ \P x \ (\y. V y < V x \ \P y)" + shows "P x" +proof - + obtain n where "n = V x" by auto + moreover have "\x. V x = n \ P x" + proof (induct n rule: infinite_descent0) + case 0 -- "i.e. $V(x) = 0$" + with A0 show "P x" by auto + next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" + case (smaller n) + then obtain x where vxn: "V x = n " and "V x > 0 \ \ P x" by auto + with A1 obtain y where "V y < V x \ \ P y" by auto + with vxn obtain m where "m = V y \ m \ P y" by auto + then show ?case by auto + qed + ultimately show "P x" by auto +qed + +text{* Again, without explicit base case: *} +lemma infinite_descent_measure: +assumes "!!x. \ P x \ \y. (V::'a\nat) y < V x \ \ P y" shows "P x" +proof - + from assms obtain n where "n = V x" by auto + moreover have "!!x. V x = n \ P x" + proof (induct n rule: infinite_descent, auto) + fix x assume "\ P x" + with assms show "\m < V x. \y. V y = m \ \ P y" by auto + qed + ultimately show "P x" by auto +qed + text {* A [clumsy] way of lifting @{text "<"} monotonicity to @{text "\"} monotonicity *} lemma less_mono_imp_le_mono: @@ -809,7 +924,7 @@ done lemma not_add_less2 [iff]: "~ (j + i < (i::nat))" -by (simp add: add_commute not_add_less1) +by (simp add: add_commute) lemma add_leD1: "m + k \ n ==> m \ (n::nat)" apply (rule order_trans [of _ "m+k"]) @@ -841,7 +956,7 @@ by (simp add: add_diff_inverse linorder_not_less) lemma le_add_diff_inverse2 [simp]: "n \ m ==> (m - n) + n = (m::nat)" -by (simp add: le_add_diff_inverse add_commute) +by (simp add: add_commute) lemma Suc_diff_le: "n \ m ==> Suc m - n = Suc (m - n)" by (induct m n rule: diff_induct) simp_all @@ -1328,6 +1443,6 @@ subsection {* size of a datatype value *} class size = type + - fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded_Recursion} *} + fixes size :: "'a \ nat" -- {* see further theory @{text Wellfounded} *} end diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Recdef.thy Fri Apr 25 15:30:33 2008 +0200 @@ -6,7 +6,7 @@ header {* TFL: recursive function definitions *} theory Recdef -imports Wellfounded_Relations FunDef +imports FunDef uses ("Tools/TFL/casesplit.ML") ("Tools/TFL/utils.ML") @@ -20,6 +20,30 @@ ("Tools/recdef_package.ML") begin +text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} +lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" +apply auto +apply (blast intro: wfrec) +done + + +lemma tfl_wf_induct: "ALL R. wf R --> + (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" +apply clarify +apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) +done + +lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" +apply clarify +apply (rule cut_apply, assumption) +done + +lemma tfl_wfrec: + "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" +apply clarify +apply (erule wfrec) +done + lemma tfl_eq_True: "(x = True) --> x" by blast diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 25 15:30:33 2008 +0200 @@ -17,7 +17,7 @@ fun PROFILE msg = if !profile then timeap_msg msg else I -val acc_const_name = "Accessible_Part.accp" +val acc_const_name = @{const_name "accp"} fun mk_acc domT R = Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Fri Apr 25 15:30:33 2008 +0200 @@ -95,17 +95,17 @@ (* Theory dependencies. *) val Pair_inject = @{thm Product_Type.Pair_inject}; -val acc_induct_rule = @{thm Accessible_Part.accp_induct_rule}; +val acc_induct_rule = @{thm accp_induct_rule}; val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}; val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}; val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}; -val acc_downward = @{thm Accessible_Part.accp_downward}; -val accI = @{thm Accessible_Part.accp.accI}; +val acc_downward = @{thm accp_downward}; +val accI = @{thm accp.accI}; val case_split = @{thm HOL.case_split_thm}; val fundef_default_value = @{thm FunDef.fundef_default_value}; -val not_acc_down = @{thm Accessible_Part.not_accp_down}; +val not_acc_down = @{thm not_accp_down}; @@ -575,7 +575,7 @@ (** Induction rule **) -val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct} +val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct} fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt); @@ -710,7 +710,7 @@ (** Termination rule **) -val wf_induct_rule = @{thm Wellfounded_Recursion.wfP_induct_rule}; +val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}; val wf_in_rel = @{thm FunDef.wf_in_rel}; val in_rel_def = @{thm FunDef.in_rel_def}; @@ -770,7 +770,7 @@ val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel - val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) + val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = all domT $ Abs ("z", domT, diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Apr 25 15:30:33 2008 +0200 @@ -50,7 +50,7 @@ val mlexT = (domT --> HOLogic.natT) --> relT --> relT fun mk_ms [] = Const (@{const_name "{}"}, relT) | mk_ms (f::fs) = - Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs + Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs in mk_ms mfuns end diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Wellfounded.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Wellfounded.thy Fri Apr 25 15:30:33 2008 +0200 @@ -0,0 +1,919 @@ +(* ID: $Id$ + Author: Tobias Nipkow + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Konrad Slind, Alexander Krauss + Copyright 1992-2008 University of Cambridge and TU Muenchen +*) + +header {*Well-founded Recursion*} + +theory Wellfounded +imports Finite_Set Nat +uses ("Tools/function_package/size.ML") +begin + +inductive + wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" + for R :: "('a * 'a) set" + and F :: "('a => 'b) => 'a => 'b" +where + wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> + wfrec_rel R F x (F g x)" + +constdefs + wf :: "('a * 'a)set => bool" + "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" + + wfP :: "('a => 'a => bool) => bool" + "wfP r == wf {(x, y). r x y}" + + acyclic :: "('a*'a)set => bool" + "acyclic r == !x. (x,x) ~: r^+" + + cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" + "cut f r x == (%y. if (y,x):r then f y else arbitrary)" + + adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" + "adm_wf R F == ALL f g x. + (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" + + wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" + [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" + +abbreviation acyclicP :: "('a => 'a => bool) => bool" where + "acyclicP r == acyclic {(x, y). r x y}" + +class wellorder = linorder + + assumes wf: "wf {(x, y). x < y}" + + +lemma wfP_wf_eq [pred_set_conv]: "wfP (\x y. (x, y) \ r) = wf r" + by (simp add: wfP_def) + +lemma wfUNIVI: + "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)" + unfolding wf_def by blast + +lemmas wfPUNIVI = wfUNIVI [to_pred] + +text{*Restriction to domain @{term A} and range @{term B}. If @{term r} is + well-founded over their intersection, then @{term "wf r"}*} +lemma wfI: + "[| r \ A <*> B; + !!x P. [|\x. (\y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] + ==> wf r" + unfolding wf_def by blast + +lemma wf_induct: + "[| wf(r); + !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) + |] ==> P(a)" + unfolding wf_def by blast + +lemmas wfP_induct = wf_induct [to_pred] + +lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] + +lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] + +lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r" + by (induct a arbitrary: x set: wf) blast + +(* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) +lemmas wf_asym = wf_not_sym [elim_format] + +lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r" + by (blast elim: wf_asym) + +(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *) +lemmas wf_irrefl = wf_not_refl [elim_format] + +text{*transitive closure of a well-founded relation is well-founded! *} +lemma wf_trancl: + assumes "wf r" + shows "wf (r^+)" +proof - + { + fix P and x + assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x" + have "P x" + proof (rule induct_step) + fix y assume "(y, x) : r^+" + with `wf r` show "P y" + proof (induct x arbitrary: y) + case (less x) + note hyp = `\x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'` + from `(y, x) : r^+` show "P y" + proof cases + case base + show "P y" + proof (rule induct_step) + fix y' assume "(y', y) : r^+" + with `(y, x) : r` show "P y'" by (rule hyp [of y y']) + qed + next + case step + then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp + then show "P y" by (rule hyp [of x' y]) + qed + qed + qed + } then show ?thesis unfolding wf_def by blast +qed + +lemmas wfP_trancl = wf_trancl [to_pred] + +lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)" + apply (subst trancl_converse [symmetric]) + apply (erule wf_trancl) + done + + +subsubsection {* Other simple well-foundedness results *} + +text{*Minimal-element characterization of well-foundedness*} +lemma wf_eq_minimal: "wf r = (\Q x. x\Q --> (\z\Q. \y. (y,z)\r --> y\Q))" +proof (intro iffI strip) + fix Q :: "'a set" and x + assume "wf r" and "x \ Q" + then show "\z\Q. \y. (y, z) \ r \ y \ Q" + unfolding wf_def + by (blast dest: spec [of _ "%x. x\Q \ (\z\Q. \y. (y,z) \ r \ y\Q)"]) +next + assume 1: "\Q x. x \ Q \ (\z\Q. \y. (y, z) \ r \ y \ Q)" + show "wf r" + proof (rule wfUNIVI) + fix P :: "'a \ bool" and x + assume 2: "\x. (\y. (y, x) \ r \ P y) \ P x" + let ?Q = "{x. \ P x}" + have "x \ ?Q \ (\z \ ?Q. \y. (y, z) \ r \ y \ ?Q)" + by (rule 1 [THEN spec, THEN spec]) + then have "\ P x \ (\z. \ P z \ (\y. (y, z) \ r \ P y))" by simp + with 2 have "\ P x \ (\z. \ P z \ P z)" by fast + then show "P x" by simp + qed +qed + +lemma wfE_min: + assumes "wf R" "x \ Q" + obtains z where "z \ Q" "\y. (y, z) \ R \ y \ Q" + using assms unfolding wf_eq_minimal by blast + +lemma wfI_min: + "(\x Q. x \ Q \ \z\Q. \y. (y, z) \ R \ y \ Q) + \ wf R" + unfolding wf_eq_minimal by blast + +lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] + +text {* Well-foundedness of subsets *} +lemma wf_subset: "[| wf(r); p<=r |] ==> wf(p)" + apply (simp (no_asm_use) add: wf_eq_minimal) + apply fast + done + +lemmas wfP_subset = wf_subset [to_pred] + +text {* Well-foundedness of the empty relation *} +lemma wf_empty [iff]: "wf({})" + by (simp add: wf_def) + +lemmas wfP_empty [iff] = + wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq] + +lemma wf_Int1: "wf r ==> wf (r Int r')" + apply (erule wf_subset) + apply (rule Int_lower1) + done + +lemma wf_Int2: "wf r ==> wf (r' Int r)" + apply (erule wf_subset) + apply (rule Int_lower2) + done + +text{*Well-foundedness of insert*} +lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)" +apply (rule iffI) + apply (blast elim: wf_trancl [THEN wf_irrefl] + intro: rtrancl_into_trancl1 wf_subset + rtrancl_mono [THEN [2] rev_subsetD]) +apply (simp add: wf_eq_minimal, safe) +apply (rule allE, assumption, erule impE, blast) +apply (erule bexE) +apply (rename_tac "a", case_tac "a = x") + prefer 2 +apply blast +apply (case_tac "y:Q") + prefer 2 apply blast +apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) + apply assumption +apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) + --{*essential for speed*} +txt{*Blast with new substOccur fails*} +apply (fast intro: converse_rtrancl_into_rtrancl) +done + +text{*Well-foundedness of image*} +lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)" +apply (simp only: wf_eq_minimal, clarify) +apply (case_tac "EX p. f p : Q") +apply (erule_tac x = "{p. f p : Q}" in allE) +apply (fast dest: inj_onD, blast) +done + + +subsubsection {* Well-Foundedness Results for Unions *} + +lemma wf_union_compatible: + assumes "wf R" "wf S" + assumes "S O R \ R" + shows "wf (R \ S)" +proof (rule wfI_min) + fix x :: 'a and Q + let ?Q' = "{x \ Q. \y. (y, x) \ R \ y \ Q}" + assume "x \ Q" + obtain a where "a \ ?Q'" + by (rule wfE_min [OF `wf R` `x \ Q`]) blast + with `wf S` + obtain z where "z \ ?Q'" and zmin: "\y. (y, z) \ S \ y \ ?Q'" by (erule wfE_min) + { + fix y assume "(y, z) \ S" + then have "y \ ?Q'" by (rule zmin) + + have "y \ Q" + proof + assume "y \ Q" + with `y \ ?Q'` + obtain w where "(w, y) \ R" and "w \ Q" by auto + from `(w, y) \ R` `(y, z) \ S` have "(w, z) \ S O R" by (rule rel_compI) + with `S O R \ R` have "(w, z) \ R" .. + with `z \ ?Q'` have "w \ Q" by blast + with `w \ Q` show False by contradiction + qed + } + with `z \ ?Q'` show "\z\Q. \y. (y, z) \ R \ S \ y \ Q" by blast +qed + + +text {* Well-foundedness of indexed union with disjoint domains and ranges *} + +lemma wf_UN: "[| ALL i:I. wf(r i); + ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} + |] ==> wf(UN i:I. r i)" +apply (simp only: wf_eq_minimal, clarify) +apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i") + prefer 2 + apply force +apply clarify +apply (drule bspec, assumption) +apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE) +apply (blast elim!: allE) +done + +lemmas wfP_SUP = wf_UN [where I=UNIV and r="\i. {(x, y). r i x y}", + to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard] + +lemma wf_Union: + "[| ALL r:R. wf r; + ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} + |] ==> wf(Union R)" +apply (simp add: Union_def) +apply (blast intro: wf_UN) +done + +(*Intuition: we find an (R u S)-min element of a nonempty subset A + by case distinction. + 1. There is a step a -R-> b with a,b : A. + Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. + By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the + subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot + have an S-successor and is thus S-min in A as well. + 2. There is no such step. + Pick an S-min element of A. In this case it must be an R-min + element of A as well. + +*) +lemma wf_Un: + "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)" + using wf_union_compatible[of s r] + by (auto simp: Un_ac) + +lemma wf_union_merge: + "wf (R \ S) = wf (R O R \ R O S \ S)" (is "wf ?A = wf ?B") +proof + assume "wf ?A" + with wf_trancl have wfT: "wf (?A^+)" . + moreover have "?B \ ?A^+" + by (subst trancl_unfold, subst trancl_unfold) blast + ultimately show "wf ?B" by (rule wf_subset) +next + assume "wf ?B" + + show "wf ?A" + proof (rule wfI_min) + fix Q :: "'a set" and x + assume "x \ Q" + + with `wf ?B` + obtain z where "z \ Q" and "\y. (y, z) \ ?B \ y \ Q" + by (erule wfE_min) + then have A1: "\y. (y, z) \ R O R \ y \ Q" + and A2: "\y. (y, z) \ R O S \ y \ Q" + and A3: "\y. (y, z) \ S \ y \ Q" + by auto + + show "\z\Q. \y. (y, z) \ ?A \ y \ Q" + proof (cases "\y. (y, z) \ R \ y \ Q") + case True + with `z \ Q` A3 show ?thesis by blast + next + case False + then obtain z' where "z'\Q" "(z', z) \ R" by blast + + have "\y. (y, z') \ ?A \ y \ Q" + proof (intro allI impI) + fix y assume "(y, z') \ ?A" + then show "y \ Q" + proof + assume "(y, z') \ R" + then have "(y, z) \ R O R" using `(z', z) \ R` .. + with A1 show "y \ Q" . + next + assume "(y, z') \ S" + then have "(y, z) \ R O S" using `(z', z) \ R` .. + with A2 show "y \ Q" . + qed + qed + with `z' \ Q` show ?thesis .. + qed + qed +qed + +lemma wf_comp_self: "wf R = wf (R O R)" -- {* special case *} + by (rule wf_union_merge [where S = "{}", simplified]) + + +subsubsection {* acyclic *} + +lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" + by (simp add: acyclic_def) + +lemma wf_acyclic: "wf r ==> acyclic r" +apply (simp add: acyclic_def) +apply (blast elim: wf_trancl [THEN wf_irrefl]) +done + +lemmas wfP_acyclicP = wf_acyclic [to_pred] + +lemma acyclic_insert [iff]: + "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" +apply (simp add: acyclic_def trancl_insert) +apply (blast intro: rtrancl_trans) +done + +lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r" +by (simp add: acyclic_def trancl_converse) + +lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] + +lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" +apply (simp add: acyclic_def antisym_def) +apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) +done + +(* Other direction: +acyclic = no loops +antisym = only self loops +Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id) +==> antisym( r^* ) = acyclic(r - Id)"; +*) + +lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r" +apply (simp add: acyclic_def) +apply (blast intro: trancl_mono) +done + +text{* Wellfoundedness of finite acyclic relations*} + +lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r" +apply (erule finite_induct, blast) +apply (simp (no_asm_simp) only: split_tupled_all) +apply simp +done + +lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)" +apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf]) +apply (erule acyclic_converse [THEN iffD2]) +done + +lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r" +by (blast intro: finite_acyclic_wf wf_acyclic) + + +subsection{*Well-Founded Recursion*} + +text{*cut*} + +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" +by (simp add: expand_fun_eq cut_def) + +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" +by (simp add: cut_def) + +text{*Inductive characterization of wfrec combinator; for details see: +John Harrison, "Inductive definitions: automation and application"*} + +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y" +apply (simp add: adm_wf_def) +apply (erule_tac a=x in wf_induct) +apply (rule ex1I) +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) +apply (fast dest!: theI') +apply (erule wfrec_rel.cases, simp) +apply (erule allE, erule allE, erule allE, erule mp) +apply (fast intro: the_equality [symmetric]) +done + +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" +apply (simp add: adm_wf_def) +apply (intro strip) +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) +apply (rule refl) +done + +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" +apply (simp add: wfrec_def) +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) +apply (rule wfrec_rel.wfrecI) +apply (intro strip) +apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) +done + +subsection {* Code generator setup *} + +consts_code + "wfrec" ("\wfrec?") +attach {* +fun wfrec f x = f (wfrec f) x; +*} + + +subsection {*LEAST and wellorderings*} + +text{* See also @{text wf_linord_ex_has_least} and its consequences in + @{text Wellfounded_Relations.ML}*} + +lemma wellorder_Least_lemma [rule_format]: + "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k" +apply (rule_tac a = k in wf [THEN wf_induct]) +apply (rule impI) +apply (rule classical) +apply (rule_tac s = x in Least_equality [THEN ssubst], auto) +apply (auto simp add: linorder_not_less [symmetric]) +done + +lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard] +lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard] + +-- "The following 3 lemmas are due to Brian Huffman" +lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)" +apply (erule exE) +apply (erule LeastI) +done + +lemma LeastI2: + "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)" +by (blast intro: LeastI) + +lemma LeastI2_ex: + "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)" +by (blast intro: LeastI_ex) + +lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)" +apply (simp (no_asm_use) add: linorder_not_le [symmetric]) +apply (erule contrapos_nn) +apply (erule Least_le) +done + +subsection {* @{typ nat} is well-founded *} + +lemma less_nat_rel: "op < = (\m n. n = Suc m)^++" +proof (rule ext, rule ext, rule iffI) + fix n m :: nat + assume "m < n" + then show "(\m n. n = Suc m)^++ m n" + proof (induct n) + case 0 then show ?case by auto + next + case (Suc n) then show ?case + by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) + qed +next + fix n m :: nat + assume "(\m n. n = Suc m)^++ m n" + then show "m < n" + by (induct n) + (simp_all add: less_Suc_eq_le reflexive le_less) +qed + +definition + pred_nat :: "(nat * nat) set" where + "pred_nat = {(m, n). n = Suc m}" + +definition + less_than :: "(nat * nat) set" where + "less_than = pred_nat^+" + +lemma less_eq: "(m, n) \ pred_nat^+ \ m < n" + unfolding less_nat_rel pred_nat_def trancl_def by simp + +lemma pred_nat_trancl_eq_le: + "(m, n) \ pred_nat^* \ m \ n" + unfolding less_eq rtrancl_eq_or_trancl by auto + +lemma wf_pred_nat: "wf pred_nat" + apply (unfold wf_def pred_nat_def, clarify) + apply (induct_tac x, blast+) + done + +lemma wf_less_than [iff]: "wf less_than" + by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) + +lemma trans_less_than [iff]: "trans less_than" + by (simp add: less_than_def trans_trancl) + +lemma less_than_iff [iff]: "((x,y): less_than) = (x (LEAST n. P n) = Suc (LEAST m. P(Suc m))" + apply (case_tac "n", auto) + apply (frule LeastI) + apply (drule_tac P = "%x. P (Suc x) " in LeastI) + apply (subgoal_tac " (LEAST x. P x) \ Suc (LEAST x. P (Suc x))") + apply (erule_tac [2] Least_le) + apply (case_tac "LEAST x. P x", auto) + apply (drule_tac P = "%x. P (Suc x) " in Least_le) + apply (blast intro: order_antisym) + done + +lemma Least_Suc2: + "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)" + apply (erule (1) Least_Suc [THEN ssubst]) + apply simp + done + +lemma ex_least_nat_le: "\P(0) \ P(n::nat) \ \k\n. (\iP i) & P(k)" + apply (cases n) + apply blast + apply (rule_tac x="LEAST k. P(k)" in exI) + apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) + done + +lemma ex_least_nat_less: "\P(0) \ P(n::nat) \ \ki\k. \P i) & P(k+1)" + apply (cases n) + apply blast + apply (frule (1) ex_least_nat_le) + apply (erule exE) + apply (case_tac k) + apply simp + apply (rename_tac k1) + apply (rule_tac x=k1 in exI) + apply fastsimp + done + + +subsection {* Accessible Part *} + +text {* + Inductive definition of the accessible part @{term "acc r"} of a + relation; see also \cite{paulin-tlca}. +*} + +inductive_set + acc :: "('a * 'a) set => 'a set" + for r :: "('a * 'a) set" + where + accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r" + +abbreviation + termip :: "('a => 'a => bool) => 'a => bool" where + "termip r == accp (r\\)" + +abbreviation + termi :: "('a * 'a) set => 'a set" where + "termi r == acc (r\)" + +lemmas accpI = accp.accI + +text {* Induction rules *} + +theorem accp_induct: + assumes major: "accp r a" + assumes hyp: "!!x. accp r x ==> \y. r y x --> P y ==> P x" + shows "P a" + apply (rule major [THEN accp.induct]) + apply (rule hyp) + apply (rule accp.accI) + apply fast + apply fast + done + +theorems accp_induct_rule = accp_induct [rule_format, induct set: accp] + +theorem accp_downward: "accp r b ==> r a b ==> accp r a" + apply (erule accp.cases) + apply fast + done + +lemma not_accp_down: + assumes na: "\ accp R x" + obtains z where "R z x" and "\ accp R z" +proof - + assume a: "\z. \R z x; \ accp R z\ \ thesis" + + show thesis + proof (cases "\z. R z x \ accp R z") + case True + hence "\z. R z x \ accp R z" by auto + hence "accp R x" + by (rule accp.accI) + with na show thesis .. + next + case False then obtain z where "R z x" and "\ accp R z" + by auto + with a show thesis . + qed +qed + +lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b" + apply (erule rtranclp_induct) + apply blast + apply (blast dest: accp_downward) + done + +theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b" + apply (blast dest: accp_downwards_aux) + done + +theorem accp_wfPI: "\x. accp r x ==> wfP r" + apply (rule wfPUNIVI) + apply (induct_tac P x rule: accp_induct) + apply blast + apply blast + done + +theorem accp_wfPD: "wfP r ==> accp r x" + apply (erule wfP_induct_rule) + apply (rule accp.accI) + apply blast + done + +theorem wfP_accp_iff: "wfP r = (\x. accp r x)" + apply (blast intro: accp_wfPI dest: accp_wfPD) + done + + +text {* Smaller relations have bigger accessible parts: *} + +lemma accp_subset: + assumes sub: "R1 \ R2" + shows "accp R2 \ accp R1" +proof + fix x assume "accp R2 x" + then show "accp R1 x" + proof (induct x) + fix x + assume ih: "\y. R2 y x \ accp R1 y" + with sub show "accp R1 x" + by (blast intro: accp.accI) + qed +qed + + +text {* This is a generalized induction theorem that works on + subsets of the accessible part. *} + +lemma accp_subset_induct: + assumes subset: "D \ accp R" + and dcl: "\x z. \D x; R z x\ \ D z" + and "D x" + and istep: "\x. \D x; (\z. R z x \ P z)\ \ P x" + shows "P x" +proof - + from subset and `D x` + have "accp R x" .. + then show "P x" using `D x` + proof (induct x) + fix x + assume "D x" + and "\y. R y x \ D y \ P y" + with dcl and istep show "P x" by blast + qed +qed + + +text {* Set versions of the above theorems *} + +lemmas acc_induct = accp_induct [to_set] + +lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] + +lemmas acc_downward = accp_downward [to_set] + +lemmas not_acc_down = not_accp_down [to_set] + +lemmas acc_downwards_aux = accp_downwards_aux [to_set] + +lemmas acc_downwards = accp_downwards [to_set] + +lemmas acc_wfI = accp_wfPI [to_set] + +lemmas acc_wfD = accp_wfPD [to_set] + +lemmas wf_acc_iff = wfP_accp_iff [to_set] + +lemmas acc_subset = accp_subset [to_set] + +lemmas acc_subset_induct = accp_subset_induct [to_set] + + +subsection {* Tools for building wellfounded relations *} + +text {* Inverse Image *} + +lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))" +apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) +apply clarify +apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }") +prefer 2 apply (blast del: allE) +apply (erule allE) +apply (erule (1) notE impE) +apply blast +done + +lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" + by (auto simp:inv_image_def) + +text {* Measure functions into @{typ nat} *} + +definition measure :: "('a => nat) => ('a * 'a)set" +where "measure == inv_image less_than" + +lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)" + by (simp add:measure_def) + +lemma wf_measure [iff]: "wf (measure f)" +apply (unfold measure_def) +apply (rule wf_less_than [THEN wf_inv_image]) +done + +text{* Lexicographic combinations *} + +definition + lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" + (infixr "<*lex*>" 80) +where + "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" + +lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)" +apply (unfold wf_def lex_prod_def) +apply (rule allI, rule impI) +apply (simp (no_asm_use) only: split_paired_All) +apply (drule spec, erule mp) +apply (rule allI, rule impI) +apply (drule spec, erule mp, blast) +done + +lemma in_lex_prod[simp]: + "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \ (a = a' \ (b, b') : s))" + by (auto simp:lex_prod_def) + +text{* @{term "op <*lex*>"} preserves transitivity *} + +lemma trans_lex_prod [intro!]: + "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)" +by (unfold trans_def lex_prod_def, blast) + +text {* lexicographic combinations with measure functions *} + +definition + mlex_prod :: "('a \ nat) \ ('a \ 'a) set \ ('a \ 'a) set" (infixr "<*mlex*>" 80) +where + "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))" + +lemma wf_mlex: "wf R \ wf (f <*mlex*> R)" +unfolding mlex_prod_def +by auto + +lemma mlex_less: "f x < f y \ (x, y) \ f <*mlex*> R" +unfolding mlex_prod_def by simp + +lemma mlex_leq: "f x \ f y \ (x, y) \ R \ (x, y) \ f <*mlex*> R" +unfolding mlex_prod_def by auto + +text {* proper subset relation on finite sets *} + +definition finite_psubset :: "('a set * 'a set) set" +where "finite_psubset == {(A,B). A < B & finite B}" + +lemma wf_finite_psubset: "wf(finite_psubset)" +apply (unfold finite_psubset_def) +apply (rule wf_measure [THEN wf_subset]) +apply (simp add: measure_def inv_image_def less_than_def less_eq) +apply (fast elim!: psubset_card_mono) +done + +lemma trans_finite_psubset: "trans finite_psubset" +by (simp add: finite_psubset_def psubset_def trans_def, blast) + + + + +text {*Wellfoundedness of @{text same_fst}*} + +definition + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" +where + "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" + --{*For @{text rec_def} declarations where the first n parameters + stay unchanged in the recursive call. + See @{text "Library/While_Combinator.thy"} for an application.*} + +lemma same_fstI [intro!]: + "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R" +by (simp add: same_fst_def) + +lemma wf_same_fst: + assumes prem: "(!!x. P x ==> wf(R x))" + shows "wf(same_fst P R)" +apply (simp cong del: imp_cong add: wf_def same_fst_def) +apply (intro strip) +apply (rename_tac a b) +apply (case_tac "wf (R a)") + apply (erule_tac a = b in wf_induct, blast) +apply (blast intro: prem) +done + + +subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) + stabilize.*} + +text{*This material does not appear to be used any longer.*} + +lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*" +apply (induct_tac "k", simp_all) +apply (blast intro: rtrancl_trans) +done + +lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] + ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))" +apply (erule wf_induct, clarify) +apply (case_tac "EX j. (f (m+j), f m) : r^+") + apply clarify + apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ") + apply clarify + apply (rule_tac x = "j+i" in exI) + apply (simp add: add_ac, blast) +apply (rule_tac x = 0 in exI, clarsimp) +apply (drule_tac i = m and k = k in lemma1) +apply (blast elim: rtranclE dest: rtrancl_into_trancl1) +done + +lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] + ==> EX i. ALL k. f (i+k) = f i" +apply (drule_tac x = 0 in lemma2 [THEN spec], auto) +done + +(* special case of the theorem above: <= *) +lemma weak_decr_stable: + "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i" +apply (rule_tac r = pred_nat in wf_weak_decr_stable) +apply (simp add: pred_nat_trancl_eq_le) +apply (intro wf_trancl wf_pred_nat) +done + + +subsection {* size of a datatype value *} + +use "Tools/function_package/size.ML" + +setup Size.setup + +lemma nat_size [simp, code func]: "size (n\nat) = n" + by (induct n) simp_all + + +end diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Wellfounded_Recursion.thy --- a/src/HOL/Wellfounded_Recursion.thy Thu Apr 24 16:53:04 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,693 +0,0 @@ -(* ID: $Id$ - Author: Tobias Nipkow - Copyright 1992 University of Cambridge -*) - -header {*Well-founded Recursion*} - -theory Wellfounded_Recursion -imports Transitive_Closure Nat -uses ("Tools/function_package/size.ML") -begin - -inductive - wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" - for R :: "('a * 'a) set" - and F :: "('a => 'b) => 'a => 'b" -where - wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> - wfrec_rel R F x (F g x)" - -constdefs - wf :: "('a * 'a)set => bool" - "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" - - wfP :: "('a => 'a => bool) => bool" - "wfP r == wf {(x, y). r x y}" - - acyclic :: "('a*'a)set => bool" - "acyclic r == !x. (x,x) ~: r^+" - - cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" - "cut f r x == (%y. if (y,x):r then f y else arbitrary)" - - adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" - "adm_wf R F == ALL f g x. - (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" - - wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" - [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" - -abbreviation acyclicP :: "('a => 'a => bool) => bool" where - "acyclicP r == acyclic {(x, y). r x y}" - -class wellorder = linorder + - assumes wf: "wf {(x, y). x < y}" - - -lemma wfP_wf_eq [pred_set_conv]: "wfP (\x y. (x, y) \ r) = wf r" - by (simp add: wfP_def) - -lemma wfUNIVI: - "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)" - unfolding wf_def by blast - -lemmas wfPUNIVI = wfUNIVI [to_pred] - -text{*Restriction to domain @{term A} and range @{term B}. If @{term r} is - well-founded over their intersection, then @{term "wf r"}*} -lemma wfI: - "[| r \ A <*> B; - !!x P. [|\x. (\y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] - ==> wf r" - unfolding wf_def by blast - -lemma wf_induct: - "[| wf(r); - !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) - |] ==> P(a)" - unfolding wf_def by blast - -lemmas wfP_induct = wf_induct [to_pred] - -lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] - -lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] - -lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r" - by (induct a arbitrary: x set: wf) blast - -(* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) -lemmas wf_asym = wf_not_sym [elim_format] - -lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r" - by (blast elim: wf_asym) - -(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *) -lemmas wf_irrefl = wf_not_refl [elim_format] - -text{*transitive closure of a well-founded relation is well-founded! *} -lemma wf_trancl: - assumes "wf r" - shows "wf (r^+)" -proof - - { - fix P and x - assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x" - have "P x" - proof (rule induct_step) - fix y assume "(y, x) : r^+" - with `wf r` show "P y" - proof (induct x arbitrary: y) - case (less x) - note hyp = `\x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'` - from `(y, x) : r^+` show "P y" - proof cases - case base - show "P y" - proof (rule induct_step) - fix y' assume "(y', y) : r^+" - with `(y, x) : r` show "P y'" by (rule hyp [of y y']) - qed - next - case step - then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp - then show "P y" by (rule hyp [of x' y]) - qed - qed - qed - } then show ?thesis unfolding wf_def by blast -qed - -lemmas wfP_trancl = wf_trancl [to_pred] - -lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)" - apply (subst trancl_converse [symmetric]) - apply (erule wf_trancl) - done - - -subsubsection {* Other simple well-foundedness results *} - -text{*Minimal-element characterization of well-foundedness*} -lemma wf_eq_minimal: "wf r = (\Q x. x\Q --> (\z\Q. \y. (y,z)\r --> y\Q))" -proof (intro iffI strip) - fix Q :: "'a set" and x - assume "wf r" and "x \ Q" - then show "\z\Q. \y. (y, z) \