--- 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)
--- 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
--- 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<y)";
-by (Simp_tac 1);
-qed "less_than_iff";
-AddIffs [less_than_iff];
-
-Goal "(!!n. (ALL m. Suc m <= n --> 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";
--- 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'<x and y'<y, is a
-subset of the lexicographic product, and therefore does not need to be defined
-separately.
*)
-Wellfounded_Relations = Finite_Set +
+header {*Well-founded Relations*}
+
+theory Wellfounded_Relations
+imports Finite_Set
+begin
+
+text{*Derived WF relations such as inverse image, lexicographic product and
+measure. The simple relational product, in which @{term "(x',y')"} precedes
+@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
+lexicographic product, and therefore does not need to be defined separately.*}
constdefs
less_than :: "(nat*nat)set"
-"less_than == trancl pred_nat"
+ "less_than == trancl pred_nat"
measure :: "('a => 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<y)"
+by (simp add: less_than_def less_def)
+
+lemma full_nat_induct:
+ assumes ih: "(!!n. (ALL m. Suc m <= n --> 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