CookBook/Package/Ind_Examples.thy
changeset 114 13fd0a83d3c3
parent 113 9b6c9d172378
child 115 039845fc96bd
equal deleted inserted replaced
113:9b6c9d172378 114:13fd0a83d3c3
    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)