82 |
82 |
83 goal WF.thy "wf r = (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q))"; |
83 goal WF.thy "wf r = (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q))"; |
84 by (blast_tac (!claset addSIs [lemma1, lemma2]) 1); |
84 by (blast_tac (!claset addSIs [lemma1, lemma2]) 1); |
85 qed "wf_eq_minimal"; |
85 qed "wf_eq_minimal"; |
86 |
86 |
|
87 (*--------------------------------------------------------------------------- |
|
88 * Wellfoundedness of subsets |
|
89 *---------------------------------------------------------------------------*) |
|
90 |
|
91 goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; |
|
92 by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); |
|
93 by (Fast_tac 1); |
|
94 qed "wf_subset"; |
|
95 |
|
96 (*--------------------------------------------------------------------------- |
|
97 * Wellfoundedness of the empty relation. |
|
98 *---------------------------------------------------------------------------*) |
|
99 |
|
100 goal thy "wf({})"; |
|
101 by (simp_tac (!simpset addsimps [wf_def]) 1); |
|
102 qed "wf_empty"; |
|
103 AddSIs [wf_empty]; |
|
104 |
|
105 (*--------------------------------------------------------------------------- |
|
106 * Wellfoundedness of `insert' |
|
107 *---------------------------------------------------------------------------*) |
|
108 |
|
109 goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; |
|
110 br iffI 1; |
|
111 by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs |
|
112 [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); |
|
113 by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); |
|
114 by(safe_tac (!claset)); |
|
115 by(EVERY1[rtac allE, atac, etac impE, Blast_tac]); |
|
116 be bexE 1; |
|
117 by(rename_tac "a" 1); |
|
118 by(case_tac "a = x" 1); |
|
119 by(res_inst_tac [("x","a")]bexI 2); |
|
120 ba 3; |
|
121 by(Blast_tac 2); |
|
122 by(case_tac "y:Q" 1); |
|
123 by(Blast_tac 2); |
|
124 by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1); |
|
125 ba 1; |
|
126 by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); |
|
127 qed "wf_insert"; |
|
128 AddIffs [wf_insert]; |
|
129 |
|
130 (*** acyclic ***) |
|
131 |
|
132 goalw WF.thy [acyclic_def] |
|
133 "!!r. wf r ==> acyclic r"; |
|
134 by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1); |
|
135 qed "wf_acyclic"; |
|
136 |
|
137 goalw WF.thy [acyclic_def] |
|
138 "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; |
|
139 by(simp_tac (!simpset addsimps [trancl_insert]) 1); |
|
140 by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1); |
|
141 qed "acyclic_insert"; |
|
142 AddIffs [acyclic_insert]; |
|
143 |
|
144 goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r"; |
|
145 by(simp_tac (!simpset addsimps [trancl_converse]) 1); |
|
146 qed "acyclic_converse"; |
87 |
147 |
88 (** cut **) |
148 (** cut **) |
89 |
149 |
90 (*This rewrite rule works upon formulae; thus it requires explicit use of |
150 (*This rewrite rule works upon formulae; thus it requires explicit use of |
91 H_cong to expose the equality*) |
151 H_cong to expose the equality*) |