src/HOL/Transitive_Closure.thy
 changeset 60681 9ce7463350a9 parent 58889 5b7a9633cfa8 child 60758 d8d85a8172b5
equal inserted replaced
60680:589ed01b94fe 60681:9ce7463350a9
`   101   -- {* monotonicity of @{text rtrancl} *}`
`   101   -- {* monotonicity of @{text rtrancl} *}`
`   102   apply (rule predicate2I)`
`   102   apply (rule predicate2I)`
`   103   apply (erule rtranclp.induct)`
`   103   apply (erule rtranclp.induct)`
`   104    apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)`
`   104    apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)`
`   105   done`
`   105   done`
`       `
`   106 `
`       `
`   107 lemma mono_rtranclp[mono]:`
`       `
`   108    "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x^** a b \<longrightarrow> y^** a b"`
`       `
`   109    using rtranclp_mono[of x y] by auto`
`   106 `
`   110 `
`   107 lemmas rtrancl_mono = rtranclp_mono [to_set]`
`   111 lemmas rtrancl_mono = rtranclp_mono [to_set]`
`   108 `
`   112 `
`   109 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:`
`   113 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:`
`   110   assumes a: "r^** a b"`
`   114   assumes a: "r^** a b"`