# HG changeset patch # User paulson # Date 1101828464 -3600 # Node ID ac272926fb771a1477e39d47444bfedfde8416a3 # Parent 3a5c538644ed42bec86b1ea213ca426e5462b7e7 converted Wellfounded_Relations to Isar script diff -r 3a5c538644ed -r ac272926fb77 TODO --- a/TODO Tue Nov 30 13:29:36 2004 +0100 +++ b/TODO Tue Nov 30 16:27:44 2004 +0100 @@ -21,7 +21,5 @@ NatArith.ML Relation_Power.ML Sum_Type.ML - Wellfounded_Recursion.ML - Wellfounded_Relations.ML - remove this file (Tobias) diff -r 3a5c538644ed -r ac272926fb77 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Nov 30 13:29:36 2004 +0100 +++ b/src/HOL/IsaMakefile Tue Nov 30 16:27:44 2004 +0100 @@ -112,8 +112,7 @@ Tools/specification_package.ML \ Tools/split_rule.ML Tools/typedef_package.ML \ Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ - Wellfounded_Recursion.thy Wellfounded_Relations.ML \ - Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ + Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ blastdata.ML cladata.ML \ document/root.tex hologic.ML simpdata.ML thy_syntax.ML @$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL diff -r 3a5c538644ed -r ac272926fb77 src/HOL/Wellfounded_Relations.ML --- a/src/HOL/Wellfounded_Relations.ML Tue Nov 30 13:29:36 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,185 +0,0 @@ -(* Title: HOL/Wellfounded_Relations - ID: $Id$ - Author: Konrad Slind - Copyright 1996 TU Munich - -Derived WF relations: inverse image, lexicographic product, measure, ... -*) - - -section "`Less than' on the natural numbers"; - -Goalw [less_than_def] "wf less_than"; -by (rtac (wf_pred_nat RS wf_trancl) 1); -qed "wf_less_than"; -AddIffs [wf_less_than]; - -Goalw [less_than_def] "trans less_than"; -by (rtac trans_trancl 1); -qed "trans_less_than"; -AddIffs [trans_less_than]; - -Goalw [less_than_def, less_def] "((x,y): less_than) = (x P m) ==> P n) ==> P n"; -by (rtac (wf_less_than RS wf_induct) 1); -by (resolve_tac (premises()) 1); -by Auto_tac; -qed_spec_mp "full_nat_induct"; - -(*---------------------------------------------------------------------------- - * The inverse image into a wellfounded relation is wellfounded. - *---------------------------------------------------------------------------*) - -Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; -by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1); -by (Clarify_tac 1); -by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1); -by (blast_tac (claset() delrules [allE]) 2); -by (etac allE 1); -by (mp_tac 1); -by (Blast_tac 1); -qed "wf_inv_image"; -Addsimps [wf_inv_image]; -AddSIs [wf_inv_image]; - - -(*---------------------------------------------------------------------------- - * All measures are wellfounded. - *---------------------------------------------------------------------------*) - -Goalw [measure_def] "wf (measure f)"; -by (rtac (wf_less_than RS wf_inv_image) 1); -qed "wf_measure"; -AddIffs [wf_measure]; - -val measure_induct = standard - (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def]) - (wf_measure RS wf_induct)); -bind_thm ("measure_induct", measure_induct); - -(*---------------------------------------------------------------------------- - * Wellfoundedness of lexicographic combinations - *---------------------------------------------------------------------------*) - -val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def] - "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"; -by (EVERY1 [rtac allI,rtac impI]); -by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); -by (rtac (wfa RS spec RS mp) 1); -by (EVERY1 [rtac allI,rtac impI]); -by (rtac (wfb RS spec RS mp) 1); -by (Blast_tac 1); -qed "wf_lex_prod"; -AddSIs [wf_lex_prod]; - -(*--------------------------------------------------------------------------- - * Transitivity of WF combinators. - *---------------------------------------------------------------------------*) -Goalw [trans_def, lex_prod_def] - "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "trans_lex_prod"; -AddSIs [trans_lex_prod]; - - -(*--------------------------------------------------------------------------- - * Wellfoundedness of proper subset on finite sets. - *---------------------------------------------------------------------------*) -Goalw [finite_psubset_def] "wf(finite_psubset)"; -by (rtac (wf_measure RS wf_subset) 1); -by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def, - symmetric less_def])1); -by (fast_tac (claset() addSEs [psubset_card_mono]) 1); -qed "wf_finite_psubset"; - -Goalw [finite_psubset_def, trans_def] "trans finite_psubset"; -by (simp_tac (simpset() addsimps [psubset_def]) 1); -by (Blast_tac 1); -qed "trans_finite_psubset"; - -(*--------------------------------------------------------------------------- - * Wellfoundedness of finite acyclic relations - * Cannot go into WF because it needs Finite. - *---------------------------------------------------------------------------*) - -Goal "finite r ==> acyclic r --> wf r"; -by (etac finite_induct 1); - by (Blast_tac 1); -by (split_all_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "finite_acyclic_wf"; - -Goal "[|finite r; acyclic r|] ==> wf (r^-1)"; -by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1); -by (etac (acyclic_converse RS iffD2) 1); -qed "finite_acyclic_wf_converse"; - -Goal "finite r ==> wf r = acyclic r"; -by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1); -qed "wf_iff_acyclic_if_finite"; - - -(*---------------------------------------------------------------------------- - * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize. - *---------------------------------------------------------------------------*) - -Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"; -by (induct_tac "k" 1); - by (ALLGOALS Simp_tac); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -val lemma = result(); - -Goal "[| 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))"; -by (etac wf_induct 1); -by (Clarify_tac 1); -by (case_tac "EX j. (f (m+j), f m) : r^+" 1); - by (Clarify_tac 1); - by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1); - by (Clarify_tac 1); - by (res_inst_tac [("x","j+i")] exI 1); - by (asm_full_simp_tac (simpset() addsimps add_ac) 1); - by (Blast_tac 1); -by (res_inst_tac [("x","0")] exI 1); -by (Clarsimp_tac 1); -by (dres_inst_tac [("i","m"), ("k","k")] lemma 1); -by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1); -val lemma = result(); - -Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \ -\ ==> EX i. ALL k. f (i+k) = f i"; -by (dres_inst_tac [("x","0")] (lemma RS spec) 1); -by Auto_tac; -qed "wf_weak_decr_stable"; - -(* special case of the theorem above: <= *) -Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"; -by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1); -by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1); -by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1)); -qed "weak_decr_stable"; - -(*---------------------------------------------------------------------------- - * Wellfoundedness of same_fst - *---------------------------------------------------------------------------*) - -Goalw[same_fst_def] "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"; -by (Asm_simp_tac 1); -qed "same_fstI"; -AddSIs[same_fstI]; - -val prems = goalw thy [same_fst_def] - "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)"; -by (full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1); -by (strip_tac 1); -by (rename_tac "a b" 1); -by (case_tac "wf(R a)" 1); - by (eres_inst_tac [("a","b")] wf_induct 1); - by (Blast_tac 1); -by (blast_tac (claset() addIs prems) 1); -qed "wf_same_fst"; diff -r 3a5c538644ed -r ac272926fb77 src/HOL/Wellfounded_Relations.thy --- a/src/HOL/Wellfounded_Relations.thy Tue Nov 30 13:29:36 2004 +0100 +++ b/src/HOL/Wellfounded_Relations.thy Tue Nov 30 16:27:44 2004 +0100 @@ -1,36 +1,220 @@ -(* Title: HOL/Wellfounded_Relations - ID: $Id$ +(* ID: $Id$ Author: Konrad Slind Copyright 1995 TU Munich - -Derived WF relations: inverse image, lexicographic product, measure, ... - -The simple relational product, in which (x',y')<(x,y) iff x' nat) => ('a * 'a)set" -"measure == inv_image less_than" + "measure == inv_image less_than" lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixr "<*lex*>" 80) -"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" + "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" + + finite_psubset :: "('a set * 'a set) set" + --{* finite proper subset*} + "finite_psubset == {(A,B). A < B & finite B}" + + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" + "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.*} + + + + +subsection{*Measure Functions make Wellfounded Relations*} + +subsubsection{*`Less than' on the natural numbers*} + +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 P m) ==> P n)" + shows "P n" +apply (rule wf_less_than [THEN wf_induct]) +apply (rule ih, auto) +done + +subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*} + +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 - (* finite proper subset*) - finite_psubset :: "('a set * 'a set) set" -"finite_psubset == {(A,B). A < B & finite B}" + +subsubsection{*Finally, All Measures are Wellfounded.*} + +lemma wf_measure [iff]: "wf (measure f)" +apply (unfold measure_def) +apply (rule wf_less_than [THEN wf_inv_image]) +done + +lemmas measure_induct = + wf_measure [THEN wf_induct, unfolded measure_def inv_image_def, + simplified, standard] + + +subsection{*Other Ways of Constructing Wellfounded Relations*} + +text{*Wellfoundedness of lexicographic combinations*} +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 + + +text{*Transitivity of WF combinators.*} +lemma trans_lex_prod [intro!]: + "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)" +by (unfold trans_def lex_prod_def, blast) + + +subsubsection{*Wellfoundedness of proper subset on finite sets.*} +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_def [symmetric]) +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) + + +subsubsection{*Wellfoundedness of finite acyclic relations*} + +text{*This proof belongs in this theory because it needs Finite.*} -(* For rec_defs where the first n parameters stay unchanged in the recursive - call. See Library/While_Combinator.thy for an application. -*) - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" -"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" +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) + + +subsubsection{*Wellfoundedness of same_fst*} + +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 + + +ML +{* +val less_than_def = thm "less_than_def"; +val measure_def = thm "measure_def"; +val lex_prod_def = thm "lex_prod_def"; +val finite_psubset_def = thm "finite_psubset_def"; + +val wf_less_than = thm "wf_less_than"; +val trans_less_than = thm "trans_less_than"; +val less_than_iff = thm "less_than_iff"; +val full_nat_induct = thm "full_nat_induct"; +val wf_inv_image = thm "wf_inv_image"; +val wf_measure = thm "wf_measure"; +val measure_induct = thm "measure_induct"; +val wf_lex_prod = thm "wf_lex_prod"; +val trans_lex_prod = thm "trans_lex_prod"; +val wf_finite_psubset = thm "wf_finite_psubset"; +val trans_finite_psubset = thm "trans_finite_psubset"; +val finite_acyclic_wf = thm "finite_acyclic_wf"; +val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse"; +val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite"; +val wf_weak_decr_stable = thm "wf_weak_decr_stable"; +val weak_decr_stable = thm "weak_decr_stable"; +val same_fstI = thm "same_fstI"; +val wf_same_fst = thm "wf_same_fst"; +*} + end