src/HOL/Transitive_Closure.thy
changeset 60681 9ce7463350a9
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
equal deleted 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"