src/HOL/Transitive_Closure.thy
changeset 45976 9dc0d950baa9
parent 45607 16b4f5774621
child 46127 af3b95160b59
equal deleted inserted replaced
45975:5e78c499a7ff 45976:9dc0d950baa9
   771   apply (cases n, simp)
   771   apply (cases n, simp)
   772   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   772   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   773   done
   773   done
   774 
   774 
   775 lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
   775 lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
   776 by(induct n) auto
   776   by (induct n) auto
   777 
   777 
   778 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
   778 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
   779 by (induct n) (simp, simp add: O_assoc [symmetric])
   779   by (induct n) (simp, simp add: O_assoc [symmetric])
   780 
   780 
   781 lemma rel_pow_empty:
   781 lemma rel_pow_empty:
   782   "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"
   782   "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"
   783   by (cases n) auto
   783   by (cases n) auto
   784 
   784