converted Wellfounded_Relations to Isar script
authorpaulson
Tue Nov 30 16:27:44 2004 +0100 (2004-11-30)
changeset 15346ac272926fb77
parent 15345 3a5c538644ed
child 15347 14585bc8fa09
converted Wellfounded_Relations to Isar script
TODO
src/HOL/IsaMakefile
src/HOL/Wellfounded_Relations.ML
src/HOL/Wellfounded_Relations.thy
     1.1 --- a/TODO	Tue Nov 30 13:29:36 2004 +0100
     1.2 +++ b/TODO	Tue Nov 30 16:27:44 2004 +0100
     1.3 @@ -21,7 +21,5 @@
     1.4    NatArith.ML
     1.5    Relation_Power.ML
     1.6    Sum_Type.ML
     1.7 -  Wellfounded_Recursion.ML
     1.8 -  Wellfounded_Relations.ML
     1.9  
    1.10  - remove this file (Tobias)
     2.1 --- a/src/HOL/IsaMakefile	Tue Nov 30 13:29:36 2004 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Tue Nov 30 16:27:44 2004 +0100
     2.3 @@ -112,8 +112,7 @@
     2.4    Tools/specification_package.ML \
     2.5    Tools/split_rule.ML Tools/typedef_package.ML \
     2.6    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
     2.7 -  Wellfounded_Recursion.thy Wellfounded_Relations.ML \
     2.8 -  Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
     2.9 +  Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    2.10    blastdata.ML cladata.ML \
    2.11    document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    2.12  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
     3.1 --- a/src/HOL/Wellfounded_Relations.ML	Tue Nov 30 13:29:36 2004 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,185 +0,0 @@
     3.4 -(*  Title: 	HOL/Wellfounded_Relations
     3.5 -    ID:         $Id$
     3.6 -    Author: 	Konrad Slind
     3.7 -    Copyright   1996  TU Munich
     3.8 -
     3.9 -Derived WF relations: inverse image, lexicographic product, measure, ...
    3.10 -*)
    3.11 -
    3.12 -
    3.13 -section "`Less than' on the natural numbers";
    3.14 -
    3.15 -Goalw [less_than_def] "wf less_than"; 
    3.16 -by (rtac (wf_pred_nat RS wf_trancl) 1);
    3.17 -qed "wf_less_than";
    3.18 -AddIffs [wf_less_than];
    3.19 -
    3.20 -Goalw [less_than_def] "trans less_than"; 
    3.21 -by (rtac trans_trancl 1);
    3.22 -qed "trans_less_than";
    3.23 -AddIffs [trans_less_than];
    3.24 -
    3.25 -Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
    3.26 -by (Simp_tac 1);
    3.27 -qed "less_than_iff";
    3.28 -AddIffs [less_than_iff];
    3.29 -
    3.30 -Goal "(!!n. (ALL m. Suc m <= n --> P m) ==> P n) ==> P n";
    3.31 -by (rtac (wf_less_than RS wf_induct) 1);
    3.32 -by (resolve_tac (premises()) 1);
    3.33 -by Auto_tac;
    3.34 -qed_spec_mp "full_nat_induct";
    3.35 -
    3.36 -(*----------------------------------------------------------------------------
    3.37 - * The inverse image into a wellfounded relation is wellfounded.
    3.38 - *---------------------------------------------------------------------------*)
    3.39 -
    3.40 -Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
    3.41 -by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
    3.42 -by (Clarify_tac 1);
    3.43 -by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1);
    3.44 -by (blast_tac (claset() delrules [allE]) 2);
    3.45 -by (etac allE 1);
    3.46 -by (mp_tac 1);
    3.47 -by (Blast_tac 1);
    3.48 -qed "wf_inv_image";
    3.49 -Addsimps [wf_inv_image];
    3.50 -AddSIs [wf_inv_image];
    3.51 -
    3.52 -
    3.53 -(*----------------------------------------------------------------------------
    3.54 - * All measures are wellfounded.
    3.55 - *---------------------------------------------------------------------------*)
    3.56 -
    3.57 -Goalw [measure_def] "wf (measure f)";
    3.58 -by (rtac (wf_less_than RS wf_inv_image) 1);
    3.59 -qed "wf_measure";
    3.60 -AddIffs [wf_measure];
    3.61 -
    3.62 -val measure_induct = standard
    3.63 -    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
    3.64 -      (wf_measure RS wf_induct));
    3.65 -bind_thm ("measure_induct", measure_induct);
    3.66 -
    3.67 -(*----------------------------------------------------------------------------
    3.68 - * Wellfoundedness of lexicographic combinations
    3.69 - *---------------------------------------------------------------------------*)
    3.70 -
    3.71 -val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
    3.72 - "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
    3.73 -by (EVERY1 [rtac allI,rtac impI]);
    3.74 -by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
    3.75 -by (rtac (wfa RS spec RS mp) 1);
    3.76 -by (EVERY1 [rtac allI,rtac impI]);
    3.77 -by (rtac (wfb RS spec RS mp) 1);
    3.78 -by (Blast_tac 1);
    3.79 -qed "wf_lex_prod";
    3.80 -AddSIs [wf_lex_prod];
    3.81 -
    3.82 -(*---------------------------------------------------------------------------
    3.83 - * Transitivity of WF combinators.
    3.84 - *---------------------------------------------------------------------------*)
    3.85 -Goalw [trans_def, lex_prod_def]
    3.86 -    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
    3.87 -by (Simp_tac 1);
    3.88 -by (Blast_tac 1);
    3.89 -qed "trans_lex_prod";
    3.90 -AddSIs [trans_lex_prod];
    3.91 -
    3.92 -
    3.93 -(*---------------------------------------------------------------------------
    3.94 - * Wellfoundedness of proper subset on finite sets.
    3.95 - *---------------------------------------------------------------------------*)
    3.96 -Goalw [finite_psubset_def] "wf(finite_psubset)";
    3.97 -by (rtac (wf_measure RS wf_subset) 1);
    3.98 -by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
    3.99 -				 symmetric less_def])1);
   3.100 -by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
   3.101 -qed "wf_finite_psubset";
   3.102 -
   3.103 -Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
   3.104 -by (simp_tac (simpset() addsimps [psubset_def]) 1);
   3.105 -by (Blast_tac 1);
   3.106 -qed "trans_finite_psubset";
   3.107 -
   3.108 -(*---------------------------------------------------------------------------
   3.109 - * Wellfoundedness of finite acyclic relations
   3.110 - * Cannot go into WF because it needs Finite.
   3.111 - *---------------------------------------------------------------------------*)
   3.112 -
   3.113 -Goal "finite r ==> acyclic r --> wf r";
   3.114 -by (etac finite_induct 1);
   3.115 - by (Blast_tac 1);
   3.116 -by (split_all_tac 1);
   3.117 -by (Asm_full_simp_tac 1);
   3.118 -qed_spec_mp "finite_acyclic_wf";
   3.119 -
   3.120 -Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
   3.121 -by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
   3.122 -by (etac (acyclic_converse RS iffD2) 1);
   3.123 -qed "finite_acyclic_wf_converse";
   3.124 -
   3.125 -Goal "finite r ==> wf r = acyclic r";
   3.126 -by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
   3.127 -qed "wf_iff_acyclic_if_finite";
   3.128 -
   3.129 -
   3.130 -(*----------------------------------------------------------------------------
   3.131 - * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
   3.132 - *---------------------------------------------------------------------------*)
   3.133 -
   3.134 -Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
   3.135 -by (induct_tac "k" 1);
   3.136 - by (ALLGOALS Simp_tac);
   3.137 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   3.138 -val lemma = result();
   3.139 -
   3.140 -Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
   3.141 -\     ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))";
   3.142 -by (etac wf_induct 1);
   3.143 -by (Clarify_tac 1);
   3.144 -by (case_tac "EX j. (f (m+j), f m) : r^+" 1);
   3.145 - by (Clarify_tac 1);
   3.146 - by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
   3.147 -  by (Clarify_tac 1);
   3.148 -  by (res_inst_tac [("x","j+i")] exI 1);
   3.149 -  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   3.150 - by (Blast_tac 1);
   3.151 -by (res_inst_tac [("x","0")] exI 1);
   3.152 -by (Clarsimp_tac 1);
   3.153 -by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
   3.154 -by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
   3.155 -val lemma = result();
   3.156 -
   3.157 -Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
   3.158 -\     ==> EX i. ALL k. f (i+k) = f i";
   3.159 -by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
   3.160 -by Auto_tac;
   3.161 -qed "wf_weak_decr_stable";
   3.162 -
   3.163 -(* special case of the theorem above: <= *)
   3.164 -Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
   3.165 -by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
   3.166 -by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1);
   3.167 -by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
   3.168 -qed "weak_decr_stable";
   3.169 -
   3.170 -(*----------------------------------------------------------------------------
   3.171 - * Wellfoundedness of same_fst
   3.172 - *---------------------------------------------------------------------------*)
   3.173 -
   3.174 -Goalw[same_fst_def] "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R";
   3.175 -by (Asm_simp_tac 1);
   3.176 -qed "same_fstI";
   3.177 -AddSIs[same_fstI];
   3.178 -
   3.179 -val prems = goalw thy [same_fst_def]
   3.180 -  "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
   3.181 -by (full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
   3.182 -by (strip_tac 1);
   3.183 -by (rename_tac "a b" 1);
   3.184 -by (case_tac "wf(R a)" 1);
   3.185 - by (eres_inst_tac [("a","b")] wf_induct 1);
   3.186 - by (Blast_tac 1);
   3.187 -by (blast_tac (claset() addIs prems) 1);
   3.188 -qed "wf_same_fst";
     4.1 --- a/src/HOL/Wellfounded_Relations.thy	Tue Nov 30 13:29:36 2004 +0100
     4.2 +++ b/src/HOL/Wellfounded_Relations.thy	Tue Nov 30 16:27:44 2004 +0100
     4.3 @@ -1,36 +1,220 @@
     4.4 -(*  Title:      HOL/Wellfounded_Relations
     4.5 -    ID:         $Id$
     4.6 +(*  ID:   $Id$
     4.7      Author:     Konrad Slind
     4.8      Copyright   1995 TU Munich
     4.9 -
    4.10 -Derived WF relations: inverse image, lexicographic product, measure, ...
    4.11 -
    4.12 -The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
    4.13 -subset of the lexicographic product, and therefore does not need to be defined
    4.14 -separately.
    4.15  *)
    4.16  
    4.17 -Wellfounded_Relations = Finite_Set + 
    4.18 +header {*Well-founded Relations*}
    4.19 +
    4.20 +theory Wellfounded_Relations
    4.21 +imports Finite_Set
    4.22 +begin
    4.23 +
    4.24 +text{*Derived WF relations such as inverse image, lexicographic product and
    4.25 +measure. The simple relational product, in which @{term "(x',y')"} precedes
    4.26 +@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
    4.27 +lexicographic product, and therefore does not need to be defined separately.*}
    4.28  
    4.29  constdefs
    4.30   less_than :: "(nat*nat)set"
    4.31 -"less_than == trancl pred_nat"
    4.32 +    "less_than == trancl pred_nat"
    4.33  
    4.34   measure   :: "('a => nat) => ('a * 'a)set"
    4.35 -"measure == inv_image less_than"
    4.36 +    "measure == inv_image less_than"
    4.37  
    4.38   lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    4.39                 (infixr "<*lex*>" 80)
    4.40 -"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
    4.41 +    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
    4.42 +
    4.43 + finite_psubset  :: "('a set * 'a set) set"
    4.44 +   --{* finite proper subset*}
    4.45 +    "finite_psubset == {(A,B). A < B & finite B}"
    4.46 +
    4.47 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    4.48 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
    4.49 +   --{*For @{text rec_def} declarations where the first n parameters
    4.50 +       stay unchanged in the recursive call. 
    4.51 +       See @{text "Library/While_Combinator.thy"} for an application.*}
    4.52 +
    4.53 +
    4.54 +
    4.55 +
    4.56 +subsection{*Measure Functions make Wellfounded Relations*}
    4.57 +
    4.58 +subsubsection{*`Less than' on the natural numbers*}
    4.59 +
    4.60 +lemma wf_less_than [iff]: "wf less_than"
    4.61 +by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
    4.62 +
    4.63 +lemma trans_less_than [iff]: "trans less_than"
    4.64 +by (simp add: less_than_def trans_trancl)
    4.65 +
    4.66 +lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
    4.67 +by (simp add: less_than_def less_def)
    4.68 +
    4.69 +lemma full_nat_induct:
    4.70 +  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
    4.71 +  shows "P n"
    4.72 +apply (rule wf_less_than [THEN wf_induct])
    4.73 +apply (rule ih, auto)
    4.74 +done
    4.75 +
    4.76 +subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
    4.77 +
    4.78 +lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
    4.79 +apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
    4.80 +apply clarify
    4.81 +apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
    4.82 +prefer 2 apply (blast del: allE)
    4.83 +apply (erule allE)
    4.84 +apply (erule (1) notE impE)
    4.85 +apply blast
    4.86 +done
    4.87  
    4.88 - (* finite proper subset*)
    4.89 - finite_psubset  :: "('a set * 'a set) set"
    4.90 -"finite_psubset == {(A,B). A < B & finite B}"
    4.91 +
    4.92 +subsubsection{*Finally, All Measures are Wellfounded.*}
    4.93 +
    4.94 +lemma wf_measure [iff]: "wf (measure f)"
    4.95 +apply (unfold measure_def)
    4.96 +apply (rule wf_less_than [THEN wf_inv_image])
    4.97 +done
    4.98 +
    4.99 +lemmas measure_induct =
   4.100 +    wf_measure [THEN wf_induct, unfolded measure_def inv_image_def, 
   4.101 +                simplified, standard]
   4.102 +
   4.103 +
   4.104 +subsection{*Other Ways of Constructing Wellfounded Relations*}
   4.105 +
   4.106 +text{*Wellfoundedness of lexicographic combinations*}
   4.107 +lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   4.108 +apply (unfold wf_def lex_prod_def) 
   4.109 +apply (rule allI, rule impI)
   4.110 +apply (simp (no_asm_use) only: split_paired_All)
   4.111 +apply (drule spec, erule mp) 
   4.112 +apply (rule allI, rule impI)
   4.113 +apply (drule spec, erule mp, blast) 
   4.114 +done
   4.115 +
   4.116 +
   4.117 +text{*Transitivity of WF combinators.*}
   4.118 +lemma trans_lex_prod [intro!]: 
   4.119 +    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   4.120 +by (unfold trans_def lex_prod_def, blast) 
   4.121 +
   4.122 +
   4.123 +subsubsection{*Wellfoundedness of proper subset on finite sets.*}
   4.124 +lemma wf_finite_psubset: "wf(finite_psubset)"
   4.125 +apply (unfold finite_psubset_def)
   4.126 +apply (rule wf_measure [THEN wf_subset])
   4.127 +apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
   4.128 +apply (fast elim!: psubset_card_mono)
   4.129 +done
   4.130 +
   4.131 +lemma trans_finite_psubset: "trans finite_psubset"
   4.132 +by (simp add: finite_psubset_def psubset_def trans_def, blast)
   4.133 +
   4.134 +
   4.135 +subsubsection{*Wellfoundedness of finite acyclic relations*}
   4.136 +
   4.137 +text{*This proof belongs in this theory because it needs Finite.*}
   4.138  
   4.139 -(* For rec_defs where the first n parameters stay unchanged in the recursive
   4.140 -   call. See Library/While_Combinator.thy for an application.
   4.141 -*)
   4.142 - same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   4.143 -"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   4.144 +lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
   4.145 +apply (erule finite_induct, blast)
   4.146 +apply (simp (no_asm_simp) only: split_tupled_all)
   4.147 +apply simp
   4.148 +done
   4.149 +
   4.150 +lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
   4.151 +apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   4.152 +apply (erule acyclic_converse [THEN iffD2])
   4.153 +done
   4.154 +
   4.155 +lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
   4.156 +by (blast intro: finite_acyclic_wf wf_acyclic)
   4.157 +
   4.158 +
   4.159 +subsubsection{*Wellfoundedness of same_fst*}
   4.160 +
   4.161 +lemma same_fstI [intro!]:
   4.162 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   4.163 +by (simp add: same_fst_def)
   4.164 +
   4.165 +lemma wf_same_fst:
   4.166 +  assumes prem: "(!!x. P x ==> wf(R x))"
   4.167 +  shows "wf(same_fst P R)"
   4.168 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
   4.169 +apply (intro strip)
   4.170 +apply (rename_tac a b)
   4.171 +apply (case_tac "wf (R a)")
   4.172 + apply (erule_tac a = b in wf_induct, blast)
   4.173 +apply (blast intro: prem)
   4.174 +done
   4.175 +
   4.176 +
   4.177 +subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
   4.178 +   stabilize.*}
   4.179 +
   4.180 +text{*This material does not appear to be used any longer.*}
   4.181 +
   4.182 +lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
   4.183 +apply (induct_tac "k", simp_all)
   4.184 +apply (blast intro: rtrancl_trans)
   4.185 +done
   4.186 +
   4.187 +lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   4.188 +      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
   4.189 +apply (erule wf_induct, clarify)
   4.190 +apply (case_tac "EX j. (f (m+j), f m) : r^+")
   4.191 + apply clarify
   4.192 + apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
   4.193 +  apply clarify
   4.194 +  apply (rule_tac x = "j+i" in exI)
   4.195 +  apply (simp add: add_ac, blast)
   4.196 +apply (rule_tac x = 0 in exI, clarsimp)
   4.197 +apply (drule_tac i = m and k = k in lemma1)
   4.198 +apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   4.199 +done
   4.200 +
   4.201 +lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   4.202 +      ==> EX i. ALL k. f (i+k) = f i"
   4.203 +apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
   4.204 +done
   4.205 +
   4.206 +(* special case of the theorem above: <= *)
   4.207 +lemma weak_decr_stable:
   4.208 +     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
   4.209 +apply (rule_tac r = pred_nat in wf_weak_decr_stable)
   4.210 +apply (simp add: pred_nat_trancl_eq_le)
   4.211 +apply (intro wf_trancl wf_pred_nat)
   4.212 +done
   4.213 +
   4.214 +
   4.215 +ML
   4.216 +{*
   4.217 +val less_than_def = thm "less_than_def";
   4.218 +val measure_def = thm "measure_def";
   4.219 +val lex_prod_def = thm "lex_prod_def";
   4.220 +val finite_psubset_def = thm "finite_psubset_def";
   4.221 +
   4.222 +val wf_less_than = thm "wf_less_than";
   4.223 +val trans_less_than = thm "trans_less_than";
   4.224 +val less_than_iff = thm "less_than_iff";
   4.225 +val full_nat_induct = thm "full_nat_induct";
   4.226 +val wf_inv_image = thm "wf_inv_image";
   4.227 +val wf_measure = thm "wf_measure";
   4.228 +val measure_induct = thm "measure_induct";
   4.229 +val wf_lex_prod = thm "wf_lex_prod";
   4.230 +val trans_lex_prod = thm "trans_lex_prod";
   4.231 +val wf_finite_psubset = thm "wf_finite_psubset";
   4.232 +val trans_finite_psubset = thm "trans_finite_psubset";
   4.233 +val finite_acyclic_wf = thm "finite_acyclic_wf";
   4.234 +val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";
   4.235 +val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";
   4.236 +val wf_weak_decr_stable = thm "wf_weak_decr_stable";
   4.237 +val weak_decr_stable = thm "weak_decr_stable";
   4.238 +val same_fstI = thm "same_fstI";
   4.239 +val wf_same_fst = thm "wf_same_fst";
   4.240 +*}
   4.241 +
   4.242  
   4.243  end