equal
deleted
inserted
replaced
461 show "x \<notin> Range {(Th th, Th holder)}" |
461 show "x \<notin> Range {(Th th, Th holder)}" |
462 proof |
462 proof |
463 assume "x \<in> Range {(Th th, Th holder)}" |
463 assume "x \<in> Range {(Th th, Th holder)}" |
464 hence eq_x: "x = Th holder" using RangeE by auto |
464 hence eq_x: "x = Th holder" using RangeE by auto |
465 show False |
465 show False |
466 proof(cases rule:vat_es.ancestors_headE[OF assms(1) start]) |
466 find_theorems ancestors tRAG |
|
467 proof(cases rule:vat_es.forest_s.ancestors_headE[OF assms(1) start]) |
467 case 1 |
468 case 1 |
468 from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG |
469 from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG |
469 show ?thesis by (auto simp:ancestors_def acyclic_def) |
470 show ?thesis by (auto simp:ancestors_def acyclic_def) |
470 next |
471 next |
471 case 2 |
472 case 2 |