author | nipkow |
Thu, 21 Feb 2008 17:33:58 +0100 | |
changeset 26105 | ae06618225ec |
parent 26072 | f65a7fa2da6c |
child 26175 | 11e338832c31 |
permissions | -rw-r--r-- |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
1 |
(* ID: $Id$ |
10213 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1992 University of Cambridge |
|
4 |
*) |
|
5 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
6 |
header {*Well-founded Recursion*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
7 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
8 |
theory Wellfounded_Recursion |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
9 |
imports Transitive_Closure Nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
10 |
uses ("Tools/function_package/size.ML") |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
11 |
begin |
10213 | 12 |
|
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
13 |
inductive |
22263 | 14 |
wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool" |
15 |
for R :: "('a * 'a) set" |
|
16 |
and F :: "('a => 'b) => 'a => 'b" |
|
17 |
where |
|
18 |
wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==> |
|
19 |
wfrec_rel R F x (F g x)" |
|
11328 | 20 |
|
10213 | 21 |
constdefs |
22 |
wf :: "('a * 'a)set => bool" |
|
23 |
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))" |
|
24 |
||
22263 | 25 |
wfP :: "('a => 'a => bool) => bool" |
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
26 |
"wfP r == wf {(x, y). r x y}" |
22263 | 27 |
|
10213 | 28 |
acyclic :: "('a*'a)set => bool" |
29 |
"acyclic r == !x. (x,x) ~: r^+" |
|
30 |
||
31 |
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" |
|
32 |
"cut f r x == (%y. if (y,x):r then f y else arbitrary)" |
|
33 |
||
11328 | 34 |
adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" |
35 |
"adm_wf R F == ALL f g x. |
|
36 |
(ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" |
|
10213 | 37 |
|
11328 | 38 |
wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" |
22845 | 39 |
[code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
22263 | 40 |
|
41 |
abbreviation acyclicP :: "('a => 'a => bool) => bool" where |
|
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
42 |
"acyclicP r == acyclic {(x, y). r x y}" |
10213 | 43 |
|
22390 | 44 |
class wellorder = linorder + |
25207 | 45 |
assumes wf: "wf {(x, y). x < y}" |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
46 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
47 |
|
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
48 |
lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r" |
22263 | 49 |
by (simp add: wfP_def) |
50 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
51 |
lemma wfUNIVI: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
52 |
"(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
53 |
by (unfold wf_def, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
54 |
|
22263 | 55 |
lemmas wfPUNIVI = wfUNIVI [to_pred] |
56 |
||
19766 | 57 |
text{*Restriction to domain @{term A} and range @{term B}. If @{term r} is |
58 |
well-founded over their intersection, then @{term "wf r"}*} |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
59 |
lemma wfI: |
19766 | 60 |
"[| r \<subseteq> A <*> B; |
61 |
!!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
62 |
==> wf r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
63 |
by (unfold wf_def, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
64 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
65 |
lemma wf_induct: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
66 |
"[| wf(r); |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
67 |
!!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
68 |
|] ==> P(a)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
69 |
by (unfold wf_def, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
70 |
|
22263 | 71 |
lemmas wfP_induct = wf_induct [to_pred] |
72 |
||
18458 | 73 |
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
17042
da5cfaa258f7
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
nipkow
parents:
15950
diff
changeset
|
74 |
|
25425
9191942c4ead
Removed some case_names and consumes attributes that are now no longer
berghofe
parents:
25207
diff
changeset
|
75 |
lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
22263 | 76 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
77 |
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
78 |
by (erule_tac a=a in wf_induct, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
79 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
80 |
(* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
81 |
lemmas wf_asym = wf_not_sym [elim_format] |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
82 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
83 |
lemma wf_not_refl [simp]: "wf(r) ==> (a,a) ~: r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
84 |
by (blast elim: wf_asym) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
85 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
86 |
(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
87 |
lemmas wf_irrefl = wf_not_refl [elim_format] |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
88 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
89 |
text{*transitive closure of a well-founded relation is well-founded! *} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
90 |
lemma wf_trancl: "wf(r) ==> wf(r^+)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
91 |
apply (subst wf_def, clarify) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
92 |
apply (rule allE, assumption) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
93 |
--{*Retains the universal formula for later use!*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
94 |
apply (erule mp) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
95 |
apply (erule_tac a = x in wf_induct) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
96 |
apply (blast elim: tranclE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
97 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
98 |
|
22263 | 99 |
lemmas wfP_trancl = wf_trancl [to_pred] |
100 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
101 |
lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
102 |
apply (subst trancl_converse [symmetric]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
103 |
apply (erule wf_trancl) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
104 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
105 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
106 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
107 |
subsubsection{*Other simple well-foundedness results*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
108 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
109 |
|
19870 | 110 |
text{*Minimal-element characterization of well-foundedness*} |
111 |
lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))" |
|
112 |
proof (intro iffI strip) |
|
113 |
fix Q::"'a set" and x |
|
114 |
assume "wf r" and "x \<in> Q" |
|
115 |
thus "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" |
|
116 |
by (unfold wf_def, |
|
117 |
blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) |
|
118 |
next |
|
22766 | 119 |
assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)" |
120 |
show "wf r" |
|
121 |
proof (rule wfUNIVI) |
|
122 |
fix P :: "'a \<Rightarrow> bool" and x |
|
123 |
assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" |
|
124 |
let ?Q = "{x. \<not> P x}" |
|
125 |
have "x \<in> ?Q \<longrightarrow> (\<exists>z\<in>?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)" |
|
126 |
by (rule 1 [THEN spec, THEN spec]) |
|
127 |
hence "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp |
|
128 |
with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast |
|
129 |
thus "P x" by simp |
|
130 |
qed |
|
19870 | 131 |
qed |
132 |
||
23186
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
133 |
lemma wfE_min: |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
134 |
assumes p:"wf R" "x \<in> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
135 |
obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
136 |
using p |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
137 |
unfolding wf_eq_minimal |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
138 |
by blast |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
139 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
140 |
lemma wfI_min: |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
141 |
"(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
142 |
\<Longrightarrow> wf R" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
143 |
unfolding wf_eq_minimal |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
144 |
by blast |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
145 |
|
22263 | 146 |
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] |
147 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
148 |
text{*Well-foundedness of subsets*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
149 |
lemma wf_subset: "[| wf(r); p<=r |] ==> wf(p)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
150 |
apply (simp (no_asm_use) add: wf_eq_minimal) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
151 |
apply fast |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
152 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
153 |
|
22263 | 154 |
lemmas wfP_subset = wf_subset [to_pred] |
155 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
156 |
text{*Well-foundedness of the empty relation*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
157 |
lemma wf_empty [iff]: "wf({})" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
158 |
by (simp add: wf_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
159 |
|
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
160 |
lemmas wfP_empty [iff] = |
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
161 |
wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq] |
22263 | 162 |
|
19870 | 163 |
lemma wf_Int1: "wf r ==> wf (r Int r')" |
164 |
by (erule wf_subset, rule Int_lower1) |
|
165 |
||
166 |
lemma wf_Int2: "wf r ==> wf (r' Int r)" |
|
167 |
by (erule wf_subset, rule Int_lower2) |
|
168 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
169 |
text{*Well-foundedness of insert*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
170 |
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
171 |
apply (rule iffI) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
172 |
apply (blast elim: wf_trancl [THEN wf_irrefl] |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
173 |
intro: rtrancl_into_trancl1 wf_subset |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
174 |
rtrancl_mono [THEN [2] rev_subsetD]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
175 |
apply (simp add: wf_eq_minimal, safe) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
176 |
apply (rule allE, assumption, erule impE, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
177 |
apply (erule bexE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
178 |
apply (rename_tac "a", case_tac "a = x") |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
179 |
prefer 2 |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
180 |
apply blast |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
181 |
apply (case_tac "y:Q") |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
182 |
prefer 2 apply blast |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
183 |
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
184 |
apply assumption |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
185 |
apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
186 |
--{*essential for speed*} |
15343 | 187 |
txt{*Blast with new substOccur fails*} |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
188 |
apply (fast intro: converse_rtrancl_into_rtrancl) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
189 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
190 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
191 |
text{*Well-foundedness of image*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
192 |
lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
193 |
apply (simp only: wf_eq_minimal, clarify) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
194 |
apply (case_tac "EX p. f p : Q") |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
195 |
apply (erule_tac x = "{p. f p : Q}" in allE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
196 |
apply (fast dest: inj_onD, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
197 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
198 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
199 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
200 |
subsubsection{*Well-Foundedness Results for Unions*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
201 |
|
26044
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
202 |
lemma wf_union_compatible: |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
203 |
assumes "wf R" "wf S" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
204 |
assumes comp: "S O R \<subseteq> R" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
205 |
shows "wf (R \<union> S)" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
206 |
proof (rule wfI_min) |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
207 |
fix x :: 'a and Q |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
208 |
let ?Q' = "{ x\<in>Q. \<forall>y. (y,x)\<in>R \<longrightarrow> y \<notin> Q }" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
209 |
assume "x \<in> Q" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
210 |
obtain a where "a \<in> ?Q'" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
211 |
by (rule wfE_min[OF `wf R` `x \<in> Q`]) blast |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
212 |
with `wf S` |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
213 |
obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min) |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
214 |
{ |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
215 |
fix y assume ySz: "(y, z) \<in> S" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
216 |
then have "y \<notin> ?Q'" by (rule zmin) |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
217 |
|
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
218 |
have "y \<notin> Q" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
219 |
proof |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
220 |
assume "y \<in> Q" |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
221 |
with `y \<notin> ?Q'` |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
222 |
obtain w where wRy: "(w, y) \<in> R" and "w \<in> Q" by auto |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
223 |
from wRy ySz have "(w, z) \<in> S O R" by (rule rel_compI) |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
224 |
with comp have "(w, z) \<in> R" .. |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
225 |
with `z \<in> ?Q'` have "w \<notin> Q" by blast |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
226 |
from this `w \<in> Q` show False .. |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
227 |
qed |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
228 |
} |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
229 |
with `z \<in> ?Q'` |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
230 |
show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
231 |
qed |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
232 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
233 |
text{*Well-foundedness of indexed union with disjoint domains and ranges*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
234 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
235 |
lemma wf_UN: "[| ALL i:I. wf(r i); |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
236 |
ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
237 |
|] ==> wf(UN i:I. r i)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
238 |
apply (simp only: wf_eq_minimal, clarify) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
239 |
apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i") |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
240 |
prefer 2 |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
241 |
apply force |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
242 |
apply clarify |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
243 |
apply (drule bspec, assumption) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
244 |
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
245 |
apply (blast elim!: allE) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
246 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
247 |
|
23744
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
248 |
lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", |
7c9e6e2fe249
Adapted to changes in infrastructure for converting between
berghofe
parents:
23389
diff
changeset
|
249 |
to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard] |
22263 | 250 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
251 |
lemma wf_Union: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
252 |
"[| ALL r:R. wf r; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
253 |
ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
254 |
|] ==> wf(Union R)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
255 |
apply (simp add: Union_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
256 |
apply (blast intro: wf_UN) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
257 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
258 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
259 |
(*Intuition: we find an (R u S)-min element of a nonempty subset A |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
260 |
by case distinction. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
261 |
1. There is a step a -R-> b with a,b : A. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
262 |
Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
263 |
By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
264 |
subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
265 |
have an S-successor and is thus S-min in A as well. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
266 |
2. There is no such step. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
267 |
Pick an S-min element of A. In this case it must be an R-min |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
268 |
element of A as well. |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
269 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
270 |
*) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
271 |
lemma wf_Un: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
272 |
"[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)" |
26044
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
273 |
using wf_union_compatible[of s r] |
32889481ec4c
lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
krauss
parents:
25425
diff
changeset
|
274 |
by (auto simp: Un_ac) |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
275 |
|
23186
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
276 |
lemma wf_union_merge: |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
277 |
"wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B") |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
278 |
proof |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
279 |
assume "wf ?A" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
280 |
with wf_trancl have wfT: "wf (?A^+)" . |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
281 |
moreover have "?B \<subseteq> ?A^+" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
282 |
by (subst trancl_unfold, subst trancl_unfold) blast |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
283 |
ultimately show "wf ?B" by (rule wf_subset) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
284 |
next |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
285 |
assume "wf ?B" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
286 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
287 |
show "wf ?A" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
288 |
proof (rule wfI_min) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
289 |
fix Q :: "'a set" and x |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
290 |
assume "x \<in> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
291 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
292 |
with `wf ?B` |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
293 |
obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
294 |
by (erule wfE_min) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
295 |
hence A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
296 |
and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
297 |
and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
298 |
by auto |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
299 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
300 |
show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
301 |
proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
302 |
case True |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
303 |
with `z \<in> Q` A3 show ?thesis by blast |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
304 |
next |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
305 |
case False |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
306 |
then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
307 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
308 |
have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
309 |
proof (intro allI impI) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
310 |
fix y assume "(y, z') \<in> ?A" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
311 |
thus "y \<notin> Q" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
312 |
proof |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
313 |
assume "(y, z') \<in> R" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
314 |
hence "(y, z) \<in> R O R" using `(z', z) \<in> R` .. |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
315 |
with A1 show "y \<notin> Q" . |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
316 |
next |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
317 |
assume "(y, z') \<in> S" |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
318 |
hence "(y, z) \<in> R O S" using `(z', z) \<in> R` .. |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
319 |
with A2 show "y \<notin> Q" . |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
320 |
qed |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
321 |
qed |
23389 | 322 |
with `z' \<in> Q` show ?thesis .. |
23186
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
323 |
qed |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
324 |
qed |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
325 |
qed |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
326 |
|
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
327 |
lemma wf_comp_self: "wf R = wf (R O R)" (* special case *) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
328 |
by (fact wf_union_merge[where S = "{}", simplified]) |
f948708bc100
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
krauss
parents:
22845
diff
changeset
|
329 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
330 |
subsubsection {*acyclic*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
331 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
332 |
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
333 |
by (simp add: acyclic_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
334 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
335 |
lemma wf_acyclic: "wf r ==> acyclic r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
336 |
apply (simp add: acyclic_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
337 |
apply (blast elim: wf_trancl [THEN wf_irrefl]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
338 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
339 |
|
22263 | 340 |
lemmas wfP_acyclicP = wf_acyclic [to_pred] |
341 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
342 |
lemma acyclic_insert [iff]: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
343 |
"acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
344 |
apply (simp add: acyclic_def trancl_insert) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
345 |
apply (blast intro: rtrancl_trans) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
346 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
347 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
348 |
lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
349 |
by (simp add: acyclic_def trancl_converse) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
350 |
|
22263 | 351 |
lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] |
352 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
353 |
lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
354 |
apply (simp add: acyclic_def antisym_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
355 |
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
356 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
357 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
358 |
(* Other direction: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
359 |
acyclic = no loops |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
360 |
antisym = only self loops |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
361 |
Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
362 |
==> antisym( r^* ) = acyclic(r - Id)"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
363 |
*) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
364 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
365 |
lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
366 |
apply (simp add: acyclic_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
367 |
apply (blast intro: trancl_mono) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
368 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
369 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
370 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
371 |
subsection{*Well-Founded Recursion*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
372 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
373 |
text{*cut*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
374 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
375 |
lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
376 |
by (simp add: expand_fun_eq cut_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
377 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
378 |
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
379 |
by (simp add: cut_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
380 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
381 |
text{*Inductive characterization of wfrec combinator; for details see: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
382 |
John Harrison, "Inductive definitions: automation and application"*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
383 |
|
22263 | 384 |
lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y" |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
385 |
apply (simp add: adm_wf_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
386 |
apply (erule_tac a=x in wf_induct) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
387 |
apply (rule ex1I) |
22263 | 388 |
apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI) |
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
389 |
apply (fast dest!: theI') |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
390 |
apply (erule wfrec_rel.cases, simp) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
391 |
apply (erule allE, erule allE, erule allE, erule mp) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
392 |
apply (fast intro: the_equality [symmetric]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
393 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
394 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
395 |
lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
396 |
apply (simp add: adm_wf_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
397 |
apply (intro strip) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
398 |
apply (rule cuts_eq [THEN iffD2, THEN subst], assumption) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
399 |
apply (rule refl) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
400 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
401 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
402 |
lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
403 |
apply (simp add: wfrec_def) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
404 |
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
405 |
apply (rule wfrec_rel.wfrecI) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
406 |
apply (intro strip) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
407 |
apply (erule adm_lemma [THEN wfrec_unique, THEN theI']) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
408 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
409 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
410 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
411 |
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
412 |
lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
413 |
apply auto |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
414 |
apply (blast intro: wfrec) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
415 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
416 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
417 |
|
17459 | 418 |
subsection {* Code generator setup *} |
419 |
||
420 |
consts_code |
|
17654
38496187809d
Renamed wf_rec to wfrec in consts_code declaration.
berghofe
parents:
17459
diff
changeset
|
421 |
"wfrec" ("\<module>wfrec?") |
17459 | 422 |
attach {* |
17654
38496187809d
Renamed wf_rec to wfrec in consts_code declaration.
berghofe
parents:
17459
diff
changeset
|
423 |
fun wfrec f x = f (wfrec f) x; |
17459 | 424 |
*} |
425 |
||
426 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
427 |
subsection{*Variants for TFL: the Recdef Package*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
428 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
429 |
lemma tfl_wf_induct: "ALL R. wf R --> |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
430 |
(ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
431 |
apply clarify |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
432 |
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
433 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
434 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
435 |
lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
436 |
apply clarify |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
437 |
apply (rule cut_apply, assumption) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
438 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
439 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
440 |
lemma tfl_wfrec: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
441 |
"ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
442 |
apply clarify |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
443 |
apply (erule wfrec) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
444 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
445 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
446 |
subsection {*LEAST and wellorderings*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
447 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
448 |
text{* See also @{text wf_linord_ex_has_least} and its consequences in |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
449 |
@{text Wellfounded_Relations.ML}*} |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
450 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
451 |
lemma wellorder_Least_lemma [rule_format]: |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
452 |
"P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
453 |
apply (rule_tac a = k in wf [THEN wf_induct]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
454 |
apply (rule impI) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
455 |
apply (rule classical) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
456 |
apply (rule_tac s = x in Least_equality [THEN ssubst], auto) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
457 |
apply (auto simp add: linorder_not_less [symmetric]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
458 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
459 |
|
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
460 |
lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard] |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
461 |
lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard] |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
462 |
|
15950 | 463 |
-- "The following 3 lemmas are due to Brian Huffman" |
464 |
lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)" |
|
465 |
apply (erule exE) |
|
466 |
apply (erule LeastI) |
|
467 |
done |
|
468 |
||
469 |
lemma LeastI2: |
|
470 |
"[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)" |
|
471 |
by (blast intro: LeastI) |
|
472 |
||
473 |
lemma LeastI2_ex: |
|
474 |
"[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)" |
|
475 |
by (blast intro: LeastI_ex) |
|
476 |
||
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
477 |
lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)" |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
478 |
apply (simp (no_asm_use) add: linorder_not_le [symmetric]) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
479 |
apply (erule contrapos_nn) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
480 |
apply (erule Least_le) |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
481 |
done |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
482 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
483 |
subsection {* @{typ nat} is well-founded *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
484 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
485 |
lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
486 |
proof (rule ext, rule ext, rule iffI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
487 |
fix n m :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
488 |
assume "m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
489 |
then show "(\<lambda>m n. n = Suc m)^++ m n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
490 |
proof (induct n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
491 |
case 0 then show ?case by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
492 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
493 |
case (Suc n) then show ?case |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
494 |
by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
495 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
496 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
497 |
fix n m :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
498 |
assume "(\<lambda>m n. n = Suc m)^++ m n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
499 |
then show "m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
500 |
by (induct n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
501 |
(simp_all add: less_Suc_eq_le reflexive le_less) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
502 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
503 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
504 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
505 |
pred_nat :: "(nat * nat) set" where |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
506 |
"pred_nat = {(m, n). n = Suc m}" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
507 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
508 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
509 |
less_than :: "(nat * nat)set" where |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
510 |
"less_than = pred_nat^+" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
511 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
512 |
lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
513 |
unfolding less_nat_rel pred_nat_def trancl_def by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
514 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
515 |
lemma pred_nat_trancl_eq_le: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
516 |
"(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
517 |
unfolding less_eq rtrancl_eq_or_trancl by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
518 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
519 |
lemma wf_pred_nat: "wf pred_nat" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
520 |
apply (unfold wf_def pred_nat_def, clarify) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
521 |
apply (induct_tac x, blast+) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
522 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
523 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
524 |
lemma wf_less_than [iff]: "wf less_than" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
525 |
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
526 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
527 |
lemma trans_less_than [iff]: "trans less_than" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
528 |
by (simp add: less_than_def trans_trancl) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
529 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
530 |
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
531 |
by (simp add: less_than_def less_eq) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
532 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
533 |
lemma wf_less: "wf {(x, y::nat). x < y}" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
534 |
using wf_less_than by (simp add: less_than_def less_eq [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
535 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
536 |
text {* Complete induction, aka course-of-values induction *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
537 |
lemma nat_less_induct: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
538 |
assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
539 |
apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
540 |
apply (rule prem) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
541 |
apply (unfold less_eq [symmetric], assumption) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
542 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
543 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
544 |
lemmas less_induct = nat_less_induct [rule_format, case_names less] |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
545 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
546 |
text {* Type @{typ nat} is a wellfounded order *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
547 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
548 |
instance nat :: wellorder |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
549 |
by intro_classes |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
550 |
(assumption | |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
551 |
rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+ |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
552 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
553 |
lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
554 |
apply (rule nat_less_induct) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
555 |
apply (case_tac n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
556 |
apply (case_tac [2] nat) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
557 |
apply (blast intro: less_trans)+ |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
558 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
559 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
560 |
text {* The method of infinite descent, frequently used in number theory. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
561 |
Provided by Roelof Oosterhuis. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
562 |
$P(n)$ is true for all $n\in\mathbb{N}$ if |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
563 |
\begin{itemize} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
564 |
\item case ``0'': given $n=0$ prove $P(n)$, |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
565 |
\item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
566 |
a smaller integer $m$ such that $\neg P(m)$. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
567 |
\end{itemize} *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
568 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
569 |
lemma infinite_descent0[case_names 0 smaller]: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
570 |
"\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
571 |
by (induct n rule: less_induct, case_tac "n>0", auto) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
572 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
573 |
text{* A compact version without explicit base case: *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
574 |
lemma infinite_descent: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
575 |
"\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m \<rbrakk> \<Longrightarrow> P n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
576 |
by (induct n rule: less_induct, auto) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
577 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
578 |
text {* Infinite descent using a mapping to $\mathbb{N}$: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
579 |
$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
580 |
\begin{itemize} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
581 |
\item case ``0'': given $V(x)=0$ prove $P(x)$, |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
582 |
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
583 |
\end{itemize} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
584 |
NB: the proof also shows how to use the previous lemma. *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
585 |
corollary infinite_descent0_measure [case_names 0 smaller]: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
586 |
assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
587 |
and A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
588 |
shows "P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
589 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
590 |
obtain n where "n = V x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
591 |
moreover have "\<And>x. V x = n \<Longrightarrow> P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
592 |
proof (induct n rule: infinite_descent0) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
593 |
case 0 -- "i.e. $V(x) = 0$" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
594 |
with A0 show "P x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
595 |
next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
596 |
case (smaller n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
597 |
then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
598 |
with A1 obtain y where "V y < V x \<and> \<not> P y" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
599 |
with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
600 |
thus ?case by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
601 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
602 |
ultimately show "P x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
603 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
604 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
605 |
text{* Again, without explicit base case: *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
606 |
lemma infinite_descent_measure: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
607 |
assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
608 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
609 |
from assms obtain n where "n = V x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
610 |
moreover have "!!x. V x = n \<Longrightarrow> P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
611 |
proof (induct n rule: infinite_descent, auto) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
612 |
fix x assume "\<not> P x" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
613 |
with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
614 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
615 |
ultimately show "P x" by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
616 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
617 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
618 |
text {* @{text LEAST} theorems for type @{typ nat}*} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
619 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
620 |
lemma Least_Suc: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
621 |
"[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
622 |
apply (case_tac "n", auto) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
623 |
apply (frule LeastI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
624 |
apply (drule_tac P = "%x. P (Suc x) " in LeastI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
625 |
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
626 |
apply (erule_tac [2] Least_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
627 |
apply (case_tac "LEAST x. P x", auto) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
628 |
apply (drule_tac P = "%x. P (Suc x) " in Least_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
629 |
apply (blast intro: order_antisym) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
630 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
631 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
632 |
lemma Least_Suc2: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
633 |
"[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
634 |
by (erule (1) Least_Suc [THEN ssubst], simp) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
635 |
|
26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
636 |
lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)" |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
637 |
apply(cases n) apply blast |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
638 |
apply(rule_tac x="LEAST k. P(k)" in exI) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
639 |
apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
640 |
done |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
641 |
|
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
642 |
lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)" |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
643 |
apply(cases n) apply blast |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
644 |
apply(frule (1) ex_least_nat_le) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
645 |
apply(erule exE) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
646 |
apply(case_tac k) apply simp |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
647 |
apply(rename_tac k1) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
648 |
apply(rule_tac x=k1 in exI) |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
649 |
apply fastsimp |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
650 |
done |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
651 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
652 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
653 |
subsection {* size of a datatype value *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
654 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
655 |
use "Tools/function_package/size.ML" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
656 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
657 |
setup Size.setup |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
658 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
659 |
lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
660 |
by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
26044
diff
changeset
|
661 |
|
15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
662 |
ML |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
663 |
{* |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
664 |
val wf_def = thm "wf_def"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
665 |
val wfUNIVI = thm "wfUNIVI"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
666 |
val wfI = thm "wfI"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
667 |
val wf_induct = thm "wf_induct"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
668 |
val wf_not_sym = thm "wf_not_sym"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
669 |
val wf_asym = thm "wf_asym"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
670 |
val wf_not_refl = thm "wf_not_refl"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
671 |
val wf_irrefl = thm "wf_irrefl"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
672 |
val wf_trancl = thm "wf_trancl"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
673 |
val wf_converse_trancl = thm "wf_converse_trancl"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
674 |
val wf_eq_minimal = thm "wf_eq_minimal"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
675 |
val wf_subset = thm "wf_subset"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
676 |
val wf_empty = thm "wf_empty"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
677 |
val wf_insert = thm "wf_insert"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
678 |
val wf_UN = thm "wf_UN"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
679 |
val wf_Union = thm "wf_Union"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
680 |
val wf_Un = thm "wf_Un"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
681 |
val wf_prod_fun_image = thm "wf_prod_fun_image"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
682 |
val acyclicI = thm "acyclicI"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
683 |
val wf_acyclic = thm "wf_acyclic"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
684 |
val acyclic_insert = thm "acyclic_insert"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
685 |
val acyclic_converse = thm "acyclic_converse"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
686 |
val acyclic_impl_antisym_rtrancl = thm "acyclic_impl_antisym_rtrancl"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
687 |
val acyclic_subset = thm "acyclic_subset"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
688 |
val cuts_eq = thm "cuts_eq"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
689 |
val cut_apply = thm "cut_apply"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
690 |
val wfrec_unique = thm "wfrec_unique"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
691 |
val wfrec = thm "wfrec"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
692 |
val def_wfrec = thm "def_wfrec"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
693 |
val tfl_wf_induct = thm "tfl_wf_induct"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
694 |
val tfl_cut_apply = thm "tfl_cut_apply"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
695 |
val tfl_wfrec = thm "tfl_wfrec"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
696 |
val LeastI = thm "LeastI"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
697 |
val Least_le = thm "Least_le"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
698 |
val not_less_Least = thm "not_less_Least"; |
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
11451
diff
changeset
|
699 |
*} |
11137 | 700 |
|
10213 | 701 |
end |