rule subrelI (for nice Isar proofs of relation inequalities)
authorkrauss
Fri May 07 15:03:53 2010 +0200 (2010-05-07)
changeset 36728ae397b810c8b
parent 36726 47ba1770da8e
child 36729 f5b63d2bd8fa
rule subrelI (for nice Isar proofs of relation inequalities)
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Fri May 07 09:59:59 2010 +0200
     1.2 +++ b/src/HOL/Relation.thy	Fri May 07 15:03:53 2010 +0200
     1.3 @@ -639,9 +639,16 @@
     1.4    done
     1.5  
     1.6  
     1.7 -subsection {* Version of @{text lfp_induct} for binary relations *}
     1.8 +subsection {* Miscellaneous *}
     1.9 +
    1.10 +text {* Version of @{thm[source] lfp_induct} for binary relations *}
    1.11  
    1.12  lemmas lfp_induct2 = 
    1.13    lfp_induct_set [of "(a, b)", split_format (complete)]
    1.14  
    1.15 +text {* Version of @{thm[source] subsetI} for binary relations *}
    1.16 +
    1.17 +lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
    1.18 +by auto
    1.19 +
    1.20  end