equal
deleted
inserted
replaced
47 contained in it, and then solve the goal by assumption. |
47 contained in it, and then solve the goal by assumption. |
48 |
48 |
49 (FIXME: add linenumbers to the proof below and the text above) |
49 (FIXME: add linenumbers to the proof below and the text above) |
50 *} |
50 *} |
51 |
51 |
52 lemma trcl_induct: |
52 lemma %linenos trcl_induct: |
53 assumes asm: "trcl R x y" |
53 assumes asm: "trcl R x y" |
54 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
54 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
55 apply(atomize (full)) |
55 apply(atomize (full)) |
56 apply(cut_tac asm) |
56 apply(cut_tac asm) |
57 apply(unfold trcl_def) |
57 apply(unfold trcl_def) |