RtranclInductRev.thy

(* Isabelle 2014 *)

theory RtranclInductRev imports Main begin

lemma rtrancl_induct2_sub: "(x, y) : r^* ==>
  (ALL a. P a a) --> (ALL a b c. (a, b) : r & (b, c) : r^* & P b c --> P a c) --> P x y"
apply(drule rtrancl_converseI)
apply(erule rtrancl.induct)
apply(auto)
apply(rotate_tac 3)
apply(drule_tac x="c" in spec)
apply(rotate_tac -1)
apply(drule_tac x="b" in spec)
apply(rotate_tac -1)
apply(drule_tac x="a" in spec)
apply(drule rtrancl_converseD)
apply(auto)
done

theorem rtrancl_induct_rev:
  "[| (x, y) : r^*; !!a. P a a; !!a b c. [| (a, b) : r; (b, c) : r^*; P b c |] ==> P a c |] ==> P x y"
apply(erule rtrancl_induct2_sub[rule_format])
apply(auto)
done

lemma trancl_rev: "(x, y) : r^+ ==> (x, y) : ((r^-1)^+)^-1"
apply(erule trancl.induct)
apply(auto)
apply(rule trancl_trans)
defer
apply(simp)
apply(rule r_into_trancl)
apply(auto)
done

lemma trancl_induct2_sub: "(x, y) : r^+ ==>
  (ALL a b. (a, b) : r --> P a b) --> (ALL a b c. (a, b) : r & (b, c) : r^+ & P b c --> P a c) --> P x y"
apply(drule trancl_rev)
apply(drule converseD)
apply(erule trancl.induct)
apply(auto)
apply(rotate_tac -2)
apply(drule_tac x="c" in spec)
apply(rotate_tac -1)
apply(drule_tac x="b" in spec)
apply(rotate_tac -1)
apply(drule_tac x="a" in spec)
apply(drule mp)
apply(auto)
apply(drule trancl_converseD)
apply(auto)
done

theorem trancl_induct_rev:
  "[| (x, y) : r^+; !!a b. (a, b) : r ==> P a b; !!a b c. [| (a, b) : r; (b, c) : r^+; P b c |] ==> P a c |] ==> P x y"
apply(erule trancl_induct2_sub[rule_format])
apply(auto)
done

end