104 * Wellfoundedness of finite acyclic relations |
104 * Wellfoundedness of finite acyclic relations |
105 * Cannot go into WF because it needs Finite |
105 * Cannot go into WF because it needs Finite |
106 *---------------------------------------------------------------------------*) |
106 *---------------------------------------------------------------------------*) |
107 |
107 |
108 goal thy "!!r. finite r ==> acyclic r --> wf r"; |
108 goal thy "!!r. finite r ==> acyclic r --> wf r"; |
109 be finite_induct 1; |
109 by (etac finite_induct 1); |
110 by(Blast_tac 1); |
110 by (Blast_tac 1); |
111 by(split_all_tac 1); |
111 by (split_all_tac 1); |
112 by(Asm_full_simp_tac 1); |
112 by (Asm_full_simp_tac 1); |
113 qed_spec_mp "finite_acyclic_wf"; |
113 qed_spec_mp "finite_acyclic_wf"; |
114 |
114 |
115 goal thy "!!r. finite r ==> wf r = acyclic r"; |
115 goal thy "!!r. finite r ==> wf r = acyclic r"; |
116 by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1); |
116 by (blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1); |
117 qed "wf_iff_acyclic_if_finite"; |
117 qed "wf_iff_acyclic_if_finite"; |
118 |
118 |
119 |
119 |
120 (*--------------------------------------------------------------------------- |
120 (*--------------------------------------------------------------------------- |
121 * A relation is wellfounded iff it has no infinite descending chain |
121 * A relation is wellfounded iff it has no infinite descending chain |
122 *---------------------------------------------------------------------------*) |
122 *---------------------------------------------------------------------------*) |
123 |
123 |
124 goalw thy [wf_eq_minimal RS eq_reflection] |
124 goalw thy [wf_eq_minimal RS eq_reflection] |
125 "wf r = (~(? f. !i. (f(Suc i),f i) : r))"; |
125 "wf r = (~(? f. !i. (f(Suc i),f i) : r))"; |
126 br iffI 1; |
126 by (rtac iffI 1); |
127 br notI 1; |
127 by (rtac notI 1); |
128 be exE 1; |
128 by (etac exE 1); |
129 by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1); |
129 by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1); |
130 by(Blast_tac 1); |
130 by (Blast_tac 1); |
131 be swap 1; |
131 by (etac swap 1); |
132 by (Asm_full_simp_tac 1); |
132 by (Asm_full_simp_tac 1); |
133 by (Step_tac 1); |
133 by (Step_tac 1); |
134 by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); |
134 by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); |
135 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); |
135 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); |
136 br allI 1; |
136 by (rtac allI 1); |
137 by(Simp_tac 1); |
137 by (Simp_tac 1); |
138 br selectI2EX 1; |
138 by (rtac selectI2EX 1); |
139 by(Blast_tac 1); |
139 by (Blast_tac 1); |
140 by(Blast_tac 1); |
140 by (Blast_tac 1); |
141 br allI 1; |
141 by (rtac allI 1); |
142 by(induct_tac "n" 1); |
142 by (induct_tac "n" 1); |
143 by(Asm_simp_tac 1); |
143 by (Asm_simp_tac 1); |
144 by(Simp_tac 1); |
144 by (Simp_tac 1); |
145 br selectI2EX 1; |
145 by (rtac selectI2EX 1); |
146 by(Blast_tac 1); |
146 by (Blast_tac 1); |
147 by(Blast_tac 1); |
147 by (Blast_tac 1); |
148 qed "wf_iff_no_infinite_down_chain"; |
148 qed "wf_iff_no_infinite_down_chain"; |