diff --git a/src/HOL/Quotient.thy b/src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy +++ b/src/HOL/Quotient.thy @@ -1,868 +1,883 @@ (* Title: HOL/Quotient.thy Author: Cezary Kaliszyk and Christian Urban *) section \Definition of Quotient Types\ theory Quotient imports Lifting keywords "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal_defn and "/" and "quotient_definition" :: thy_goal_defn and "copy_bnf" :: thy_defn and "lift_bnf" :: thy_goal_defn begin text \ Basic definition for equivalence relations that are represented by predicates. \ text \Composition of Relations\ abbreviation rel_conj :: "('a \ 'b \ bool) \ ('b \ 'a \ bool) \ 'a \ 'b \ bool" (infixr "OOO" 75) where "r1 OOO r2 \ r1 OO r2 OO r1" lemma eq_comp_r: shows "((=) OOO R) = R" by (auto simp add: fun_eq_iff) context includes lifting_syntax begin subsection \Quotient Predicate\ definition "Quotient3 R Abs Rep \ (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s)" lemma Quotient3I: assumes "\a. Abs (Rep a) = a" and "\a. R (Rep a) (Rep a)" and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" shows "Quotient3 R Abs Rep" using assms unfolding Quotient3_def by blast context fixes R Abs Rep assumes a: "Quotient3 R Abs Rep" begin lemma Quotient3_abs_rep: "Abs (Rep a) = a" using a unfolding Quotient3_def by simp lemma Quotient3_rep_reflp: "R (Rep a) (Rep a)" using a unfolding Quotient3_def by blast lemma Quotient3_rel: "R r r \ R s s \ Abs r = Abs s \ R r s" \ \orientation does not loop on rewriting\ using a unfolding Quotient3_def by blast lemma Quotient3_refl1: "R r s \ R r r" using a unfolding Quotient3_def by fast lemma Quotient3_refl2: "R r s \ R s s" using a unfolding Quotient3_def by fast lemma Quotient3_rel_rep: "R (Rep a) (Rep b) \ a = b" using a unfolding Quotient3_def by metis lemma Quotient3_rep_abs: "R r r \ R (Rep (Abs r)) r" using a unfolding Quotient3_def by blast lemma Quotient3_rel_abs: "R r s \ Abs r = Abs s" using a unfolding Quotient3_def by blast lemma Quotient3_symp: "symp R" using a unfolding Quotient3_def using sympI by metis lemma Quotient3_transp: "transp R" using a unfolding Quotient3_def using transpI by (metis (full_types)) lemma Quotient3_part_equivp: "part_equivp R" by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI) lemma abs_o_rep: "Abs \ Rep = id" unfolding fun_eq_iff by (simp add: Quotient3_abs_rep) lemma equals_rsp: assumes b: "R xa xb" "R ya yb" shows "R xa ya = R xb yb" using b Quotient3_symp Quotient3_transp by (blast elim: sympE transpE) lemma rep_abs_rsp: assumes b: "R x1 x2" shows "R x1 (Rep (Abs x2))" using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp by metis lemma rep_abs_rsp_left: assumes b: "R x1 x2" shows "R (Rep (Abs x1)) x2" using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp by metis end lemma identity_quotient3: "Quotient3 (=) id id" unfolding Quotient3_def id_def by blast lemma fun_quotient3: assumes q1: "Quotient3 R1 abs1 rep1" and q2: "Quotient3 R2 abs2 rep2" shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - have "(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" for a using q1 q2 by (simp add: Quotient3_def fun_eq_iff) moreover have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a by (rule rel_funI) (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], simp (no_asm) add: Quotient3_def, simp) moreover have "(R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" for r s proof - have "(R1 ===> R2) r s \ (R1 ===> R2) r r" unfolding rel_fun_def using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) moreover have "(R1 ===> R2) r s \ (R1 ===> R2) s s" unfolding rel_fun_def using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] by (metis (full_types) part_equivp_def) moreover have "(R1 ===> R2) r s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s" by (auto simp add: rel_fun_def fun_eq_iff) (use q1 q2 in \unfold Quotient3_def, metis\) moreover have "((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s) \ (R1 ===> R2) r s" by (auto simp add: rel_fun_def fun_eq_iff) (use q1 q2 in \unfold Quotient3_def, metis map_fun_apply\) ultimately show ?thesis by blast qed ultimately show ?thesis by (intro Quotient3I) (assumption+) qed lemma lambda_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" unfolding fun_eq_iff using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma lambda_prs1: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" unfolding fun_eq_iff using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp text\ In the following theorem R1 can be instantiated with anything, but we know some of the types of the Rep and Abs functions; so by solving Quotient assumptions we can get a unique R1 that will be provable; which is why we need to use \apply_rsp\ and not the primed version\ lemma apply_rspQ3: fixes f g::"'a \ 'c" assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: rel_funE) lemma apply_rspQ3'': assumes "Quotient3 R Abs Rep" and "(R ===> S) f f" shows "S (f (Rep x)) (f (Rep x))" proof - from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) then show ?thesis using assms(2) by (auto intro: apply_rsp') qed subsection \lemmas for regularisation of ball and bex\ lemma ball_reg_eqv: fixes P :: "'a \ bool" assumes a: "equivp R" shows "Ball (Respects R) P = (All P)" using a unfolding equivp_def by (auto simp add: in_respects) lemma bex_reg_eqv: fixes P :: "'a \ bool" assumes a: "equivp R" shows "Bex (Respects R) P = (Ex P)" using a unfolding equivp_def by (auto simp add: in_respects) lemma ball_reg_right: assumes a: "\x. x \ R \ P x \ Q x" shows "All P \ Ball R Q" using a by fast lemma bex_reg_left: assumes a: "\x. x \ R \ Q x \ P x" shows "Bex R Q \ Ex P" using a by fast lemma ball_reg_left: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" using a by (metis equivp_reflp in_respects) lemma bex_reg_right: assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" using a by (metis equivp_reflp in_respects) lemma ball_reg_eqv_range: fixes P::"'a \ bool" and x::"'a" assumes a: "equivp R2" - shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" - apply(rule iffI) - apply(rule allI) - apply(drule_tac x="\y. f x" in bspec) - apply(simp add: in_respects rel_fun_def) - apply(rule impI) - using a equivp_reflp_symp_transp[of "R2"] - apply (auto elim: equivpE reflpE) - done + shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" +proof (intro allI iffI) + fix f + assume "\f \ Respects (R1 ===> R2). P (f x)" + moreover have "(\y. f x) \ Respects (R1 ===> R2)" + using a equivp_reflp_symp_transp[of "R2"] + by(auto simp add: in_respects rel_fun_def elim: equivpE reflpE) + ultimately show "P (f x)" + by auto +qed auto lemma bex_reg_eqv_range: assumes a: "equivp R2" shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" - apply(auto) - apply(rule_tac x="\y. f x" in bexI) - apply(simp) - apply(simp add: Respects_def in_respects rel_fun_def) - apply(rule impI) - using a equivp_reflp_symp_transp[of "R2"] - apply (auto elim: equivpE reflpE) - done +proof - + { fix f + assume "P (f x)" + have "(\y. f x) \ Respects (R1 ===> R2)" + using a equivp_reflp_symp_transp[of "R2"] + by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) } + then show ?thesis + by auto +qed (* Next four lemmas are unused *) lemma all_reg: assumes a: "\x :: 'a. (P x \ Q x)" and b: "All P" shows "All Q" using a b by fast lemma ex_reg: assumes a: "\x :: 'a. (P x \ Q x)" and b: "Ex P" shows "Ex Q" using a b by fast lemma ball_reg: assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Ball R P" shows "Ball R Q" using a b by fast lemma bex_reg: assumes a: "\x :: 'a. (x \ R \ P x \ Q x)" and b: "Bex R P" shows "Bex R Q" using a b by fast lemma ball_all_comm: assumes "\y. (\x\P. A x y) \ (\x. B x y)" shows "(\x\P. \y. A x y) \ (\x. \y. B x y)" using assms by auto lemma bex_ex_comm: assumes "(\y. \x. A x y) \ (\y. \x\P. B x y)" shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" using assms by auto subsection \Bounded abstraction\ definition Babs :: "'a set \ ('a \ 'b) \ 'a \ 'b" where "x \ p \ Babs p m x = m x" lemma babs_rsp: assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" - apply (auto simp add: Babs_def in_respects rel_fun_def) - apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") - using a apply (simp add: Babs_def rel_fun_def) - apply (simp add: in_respects rel_fun_def) - using Quotient3_rel[OF q] - by metis +proof (clarsimp simp add: Babs_def in_respects rel_fun_def) + fix x y + assume "R1 x y" + then have "x \ Respects R1 \ y \ Respects R1" + unfolding in_respects rel_fun_def using Quotient3_rel[OF q]by metis + then show "R2 (Babs (Respects R1) f x) (Babs (Respects R1) g y)" + using \R1 x y\ a by (simp add: Babs_def rel_fun_def) +qed lemma babs_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" - shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" - apply (rule ext) - apply (simp add:) - apply (subgoal_tac "Rep1 x \ Respects R1") - apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) - apply (simp add: in_respects Quotient3_rel_rep[OF q1]) - done +shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" +proof - + { fix x + have "Rep1 x \ Respects R1" + by (simp add: in_respects Quotient3_rel_rep[OF q1]) + then have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" + by (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) + } + then show ?thesis + by force +qed lemma babs_simp: assumes q: "Quotient3 R1 Abs Rep" shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" - apply(rule iffI) - apply(simp_all only: babs_rsp[OF q]) - apply(auto simp add: Babs_def rel_fun_def) - apply(metis Babs_def in_respects Quotient3_rel[OF q]) - done + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + unfolding rel_fun_def by (metis Babs_def in_respects Quotient3_rel[OF q]) +qed (simp add: babs_rsp[OF q]) -(* If a user proves that a particular functional relation - is an equivalence this may be useful in regularising *) +text \If a user proves that a particular functional relation + is an equivalence, this may be useful in regularising\ lemma babs_reg_eqv: shows "equivp R \ Babs (Respects R) P = P" by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp) (* 3 lemmas needed for proving repabs_inj *) lemma ball_rsp: assumes a: "(R ===> (=)) f g" shows "Ball (Respects R) f = Ball (Respects R) g" using a by (auto simp add: Ball_def in_respects elim: rel_funE) lemma bex_rsp: assumes a: "(R ===> (=)) f g" shows "(Bex (Respects R) f = Bex (Respects R) g)" using a by (auto simp add: Bex_def in_respects elim: rel_funE) lemma bex1_rsp: assumes a: "(R ===> (=)) f g" shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" using a by (auto elim: rel_funE simp add: Ex1_def in_respects) -(* 2 lemmas needed for cleaning of quantifiers *) +text \Two lemmas needed for cleaning of quantifiers\ + lemma all_prs: assumes a: "Quotient3 R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def by metis lemma ex_prs: assumes a: "Quotient3 R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def by metis subsection \\Bex1_rel\ quantifier\ definition Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" where "Bex1_rel R P \ (\x \ Respects R. P x) \ (\x \ Respects R. \y \ Respects R. ((P x \ P y) \ (R x y)))" lemma bex1_rel_aux: "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R x\ \ Bex1_rel R y" unfolding Bex1_rel_def by (metis in_respects) lemma bex1_rel_aux2: "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R y\ \ Bex1_rel R x" unfolding Bex1_rel_def by (metis in_respects) lemma bex1_rel_rsp: assumes a: "Quotient3 R absf repf" shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)" unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2) lemma ex1_prs: assumes "Quotient3 R absf repf" shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" - apply (auto simp: Bex1_rel_def Respects_def) - apply (metis Quotient3_def assms) - apply (metis (full_types) Quotient3_def assms) - by (meson Quotient3_rel assms) + (is "?lhs = ?rhs") + using assms + apply (auto simp add: Bex1_rel_def Respects_def) + by (metis (full_types) Quotient3_def)+ lemma bex1_bexeq_reg: shows "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects) lemma bex1_bexeq_reg_eqv: assumes a: "equivp R" shows "(\!x. P x) \ Bex1_rel R P" using equivp_reflp[OF a] by (metis (full_types) Bex1_rel_def in_respects) subsection \Various respects and preserve lemmas\ lemma quot_rel_rsp: assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> (=)) R R" apply(rule rel_funI)+ by (meson assms equals_rsp) lemma o_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" and q3: "Quotient3 R3 Abs3 Rep3" shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) (\) = (\)" and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) (\) = (\)" using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] by (simp_all add: fun_eq_iff) lemma o_rsp: "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) (\) (\)" "((=) ===> (R1 ===> (=)) ===> R1 ===> (=)) (\) (\)" by (force elim: rel_funE)+ lemma cond_prs: assumes a: "Quotient3 R absf repf" shows "absf (if a then repf b else repf c) = (if a then b else c)" using a unfolding Quotient3_def by auto lemma if_prs: assumes q: "Quotient3 R Abs Rep" shows "(id ---> Rep ---> Rep ---> Abs) If = If" using Quotient3_abs_rep[OF q] by (auto simp add: fun_eq_iff) lemma if_rsp: assumes q: "Quotient3 R Abs Rep" shows "((=) ===> R ===> R ===> R) If If" by force lemma let_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by (auto simp add: fun_eq_iff) lemma let_rsp: shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" by (force elim: rel_funE) lemma id_rsp: shows "(R ===> R) id id" by auto lemma id_prs: assumes a: "Quotient3 R Abs Rep" shows "(Rep ---> Abs) id = id" by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) end locale quot_type = fixes R :: "'a \ 'a \ bool" and Abs :: "'a set \ 'b" and Rep :: "'b \ 'a set" assumes equivp: "part_equivp R" and rep_prop: "\y. \x. R x x \ Rep y = Collect (R x)" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\c. (\x. ((R x x) \ (c = Collect (R x)))) \ (Rep (Abs c)) = c" and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" begin definition abs :: "'a \ 'b" where "abs x = Abs (Collect (R x))" definition rep :: "'b \ 'a" where "rep a = (SOME x. x \ Rep a)" lemma some_collect: assumes "R r r" shows "R (SOME x. x \ Collect (R r)) = R r" apply simp by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: shows "Quotient3 R abs rep" unfolding Quotient3_def abs_def rep_def proof (intro conjI allI) fix a r s show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) qed have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" proof - assume "R r r" and "R s s" then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" by (metis abs_inverse) also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" by rule simp_all finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp qed then show "R r s \ R r r \ R s s \ (Abs (Collect (R r)) = Abs (Collect (R s)))" using equivp[simplified part_equivp_def] by metis qed end subsection \Quotient composition\ - lemma OOO_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" fixes R2' :: "'a \ 'a \ bool" fixes R2 :: "'b \ 'b \ bool" assumes R1: "Quotient3 R1 Abs1 Rep1" assumes R2: "Quotient3 R2 Abs2 Rep2" assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" proof - have *: "(R1 OOO R2') r r \ (R1 OOO R2') s s \ (Abs2 \ Abs1) r = (Abs2 \ Abs1) s \ (R1 OOO R2') r s" for r s - apply safe - subgoal for a b c d - apply simp - apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) - using Quotient3_refl1 R1 rep_abs_rsp apply fastforce - apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI) - apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) - by (metis Quotient3_rel R1 rep_abs_rsp_left) - subgoal for x y - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Quotient3_refl1 [OF R2], drule Rep1) - by (metis (full_types) Quotient3_def R1 relcompp.relcompI) - subgoal for x y - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Quotient3_refl2 [OF R2], drule Rep1) - by (metis (full_types) Quotient3_def R1 relcompp.relcompI) - subgoal for x y - by simp (metis (full_types) Abs1 Quotient3_rel R1 R2) - done + proof (intro iffI conjI; clarify) + show "(R1 OOO R2') r s" + if r: "R1 r a" "R2' a b" "R1 b r" and eq: "(Abs2 \ Abs1) r = (Abs2 \ Abs1) s" + and s: "R1 s c" "R2' c d" "R1 d s" for a b c d + proof - + have "R1 r (Rep1 (Abs1 r))" + using r Quotient3_refl1 R1 rep_abs_rsp by fastforce + moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))" + using that + apply (simp add: ) + apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) + done + moreover have "R1 (Rep1 (Abs1 s)) s" + by (metis s Quotient3_rel R1 rep_abs_rsp_left) + ultimately show ?thesis + by (metis relcomppI) + qed + next + fix x y + assume xy: "R1 r x" "R2' x y" "R1 y s" + then have "R2 (Abs1 x) (Abs1 y)" + by (iprover dest: Abs1 elim: Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1]) + then have "R2' (Rep1 (Abs1 x)) (Rep1 (Abs1 x))" "R2' (Rep1 (Abs1 y)) (Rep1 (Abs1 y))" + by (simp_all add: Quotient3_refl1 [OF R2] Quotient3_refl2 [OF R2] Rep1) + with \R1 r x\ \R1 y s\ show "(R1 OOO R2') r r" "(R1 OOO R2') s s" + by (metis (full_types) Quotient3_def R1 relcompp.relcompI)+ + show "(Abs2 \ Abs1) r = (Abs2 \ Abs1) s" + using xy by simp (metis (full_types) Abs1 Quotient3_rel R1 R2) + qed show ?thesis apply (rule Quotient3I) using * apply (simp_all add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) apply (metis Quotient3_rep_reflp R1 R2 Rep1 relcompp.relcompI) done qed lemma OOO_eq_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" assumes R1: "Quotient3 R1 Abs1 Rep1" assumes R2: "Quotient3 (=) Abs2 Rep2" shows "Quotient3 (R1 OOO (=)) (Abs2 \ Abs1) (Rep1 \ Rep2)" using assms by (rule OOO_quotient3) auto subsection \Quotient3 to Quotient\ lemma Quotient3_to_Quotient: assumes "Quotient3 R Abs Rep" and "T \ \x y. R x x \ Abs x = y" shows "Quotient R Abs Rep T" using assms unfolding Quotient3_def by (intro QuotientI) blast+ lemma Quotient3_to_Quotient_equivp: assumes q: "Quotient3 R Abs Rep" and T_def: "T \ \x y. Abs x = y" and eR: "equivp R" shows "Quotient R Abs Rep T" proof (intro QuotientI) fix a show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep) next fix a show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp) next fix r s show "R r s = (R r r \ R s s \ Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) next show "T = (\x y. R x x \ Abs x = y)" using T_def equivp_reflp[OF eR] by simp qed subsection \ML setup\ text \Auxiliary data for the quotient package\ named_theorems quot_equiv "equivalence relation theorems" and quot_respect "respectfulness theorems" and quot_preserve "preservation theorems" and id_simps "identity simp rules for maps" and quot_thm "quotient theorems" ML_file \Tools/Quotient/quotient_info.ML\ declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]] lemmas [quot_thm] = fun_quotient3 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp lemmas [quot_preserve] = if_prs o_prs let_prs id_prs lemmas [quot_equiv] = identity_equivp text \Lemmas about simplifying id's.\ lemmas [id_simps] = id_def[symmetric] map_fun_id id_apply id_o o_id eq_comp_r vimage_id text \Translation functions for the lifting process.\ ML_file \Tools/Quotient/quotient_term.ML\ text \Definitions of the quotient types.\ ML_file \Tools/Quotient/quotient_type.ML\ text \Definitions for quotient constants.\ ML_file \Tools/Quotient/quotient_def.ML\ text \ An auxiliary constant for recording some information about the lifted theorem in a tactic. \ definition Quot_True :: "'a \ bool" where "Quot_True x \ True" lemma shows QT_all: "Quot_True (All P) \ Quot_True P" and QT_ex: "Quot_True (Ex P) \ Quot_True P" and QT_ex1: "Quot_True (Ex1 P) \ Quot_True P" and QT_lam: "Quot_True (\x. P x) \ (\x. Quot_True (P x))" and QT_ext: "(\x. Quot_True (a x) \ f x = g x) \ (Quot_True a \ f = g)" by (simp_all add: Quot_True_def ext) lemma QT_imp: "Quot_True a \ Quot_True b" by (simp add: Quot_True_def) context includes lifting_syntax begin text \Tactics for proving the lifted theorems\ ML_file \Tools/Quotient/quotient_tacs.ML\ end subsection \Methods / Interface\ method_setup lifting = \Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\ \lift theorems to quotient types\ method_setup lifting_setup = \Attrib.thm >> (fn thm => fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\ \set up the three goals for the quotient lifting procedure\ method_setup descending = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\ \decend theorems to the raw level\ method_setup descending_setup = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\ \set up the three goals for the decending theorems\ method_setup partiality_descending = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\ \decend theorems to the raw level\ method_setup partiality_descending_setup = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\ \set up the three goals for the decending theorems\ method_setup regularize = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\ \prove the regularization goals from the quotient lifting procedure\ method_setup injection = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\ \prove the rep/abs injection goals from the quotient lifting procedure\ method_setup cleaning = \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\ \prove the cleaning goals from the quotient lifting procedure\ attribute_setup quot_lifted = \Scan.succeed Quotient_Tacs.lifted_attrib\ \lift theorems to quotient types\ no_notation rel_conj (infixr "OOO" 75) section \Lifting of BNFs\ lemma sum_insert_Inl_unit: "x \ A \ (\y. x = Inr y \ Inr y \ B) \ x \ insert (Inl ()) B" by (cases x) (simp_all) lemma lift_sum_unit_vimage_commute: "insert (Inl ()) (Inr ` f -` A) = map_sum id f -` insert (Inl ()) (Inr ` A)" by (auto simp: map_sum_def split: sum.splits) lemma insert_Inl_int_map_sum_unit: "insert (Inl ()) A \ range (map_sum id f) \ {}" by (auto simp: map_sum_def split: sum.splits) lemma image_map_sum_unit_subset: "A \ insert (Inl ()) (Inr ` B) \ map_sum id f ` A \ insert (Inl ()) (Inr ` f ` B)" by auto lemma subset_lift_sum_unitD: "A \ insert (Inl ()) (Inr ` B) \ Inr x \ A \ x \ B" unfolding insert_def by auto lemma UNIV_sum_unit_conv: "insert (Inl ()) (range Inr) = UNIV" unfolding UNIV_sum UNIV_unit image_insert image_empty Un_insert_left sup_bot.left_neutral.. lemma subset_vimage_image_subset: "A \ f -` B \ f ` A \ B" by auto lemma relcompp_mem_Grp_neq_bot: "A \ range f \ {} \ (\x y. x \ A \ y \ A) OO (Grp UNIV f)\\ \ bot" unfolding Grp_def relcompp_apply fun_eq_iff by blast lemma comp_projr_Inr: "projr \ Inr = id" by auto lemma in_rel_sum_in_image_projr: "B \ {(x,y). rel_sum ((=) :: unit \ unit \ bool) A x y} \ Inr ` C = fst ` B \ snd ` B = Inr ` D \ map_prod projr projr ` B \ {(x,y). A x y}" by (force simp: projr_def image_iff dest!: spec[of _ "Inl ()"] split: sum.splits) lemma subset_rel_sumI: "B \ {(x,y). A x y} \ rel_sum ((=) :: unit => unit => bool) A (if x \ B then Inr (fst x) else Inl ()) (if x \ B then Inr (snd x) else Inl ())" by auto lemma relcompp_eq_Grp_neq_bot: "(=) OO (Grp UNIV f)\\ \ bot" unfolding Grp_def relcompp_apply fun_eq_iff by blast lemma rel_fun_rel_OO1: "(rel_fun Q (rel_fun R (=))) A B \ conversep Q OO A OO R \ B" by (auto simp: rel_fun_def) lemma rel_fun_rel_OO2: "(rel_fun Q (rel_fun R (=))) A B \ Q OO B OO conversep R \ A" by (auto simp: rel_fun_def) lemma rel_sum_eq2_nonempty: "rel_sum (=) A OO rel_sum (=) B \ bot" by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"]) lemma rel_sum_eq3_nonempty: "rel_sum (=) A OO (rel_sum (=) B OO rel_sum (=) C) \ bot" by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"]) lemma hypsubst: "A = B \ x \ B \ (x \ A \ P) \ P" by simp lemma Quotient_crel_quotient: "Quotient R Abs Rep T \ equivp R \ T \ (\x y. Abs x = y)" by (drule Quotient_cr_rel) (auto simp: fun_eq_iff equivp_reflp intro!: eq_reflection) lemma Quotient_crel_typedef: "Quotient (eq_onp P) Abs Rep T \ T \ (\x y. x = Rep y)" unfolding Quotient_def by (auto 0 4 simp: fun_eq_iff eq_onp_def intro: sym intro!: eq_reflection) lemma Quotient_crel_typecopy: "Quotient (=) Abs Rep T \ T \ (\x y. x = Rep y)" by (subst (asm) eq_onp_True[symmetric]) (rule Quotient_crel_typedef) lemma equivp_add_relconj: assumes equiv: "equivp R" "equivp R'" and le: "S OO T OO U \ R OO STU OO R'" shows "R OO S OO T OO U OO R' \ R OO STU OO R'" proof - have trans: "R OO R \ R" "R' OO R' \ R'" using equiv unfolding equivp_reflp_symp_transp transp_relcompp by blast+ have "R OO S OO T OO U OO R' = R OO (S OO T OO U) OO R'" unfolding relcompp_assoc .. also have "\ \ R OO (R OO STU OO R') OO R'" by (intro le relcompp_mono order_refl) also have "\ \ (R OO R) OO STU OO (R' OO R')" unfolding relcompp_assoc .. also have "\ \ R OO STU OO R'" by (intro trans relcompp_mono order_refl) finally show ?thesis . qed lemma Grp_conversep_eq_onp: "((BNF_Def.Grp UNIV f)\\ OO BNF_Def.Grp UNIV f) = eq_onp (\x. x \ range f)" by (auto simp: fun_eq_iff Grp_def eq_onp_def image_iff) lemma Grp_conversep_nonempty: "(BNF_Def.Grp UNIV f)\\ OO BNF_Def.Grp UNIV f \ bot" by (auto simp: fun_eq_iff Grp_def) lemma relcomppI2: "r a b \ s b c \ t c d \ (r OO s OO t) a d" by (auto) lemma rel_conj_eq_onp: "equivp R \ rel_conj R (eq_onp P) \ R" by (auto simp: eq_onp_def transp_def equivp_def) lemma Quotient_Quotient3: "Quotient R Abs Rep T \ Quotient3 R Abs Rep" unfolding Quotient_def Quotient3_def by blast lemma Quotient_reflp_imp_equivp: "Quotient R Abs Rep T \ reflp R \ equivp R" using Quotient_symp Quotient_transp equivpI by blast lemma Quotient_eq_onp_typedef: "Quotient (eq_onp P) Abs Rep cr \ type_definition Rep Abs {x. P x}" unfolding Quotient_def eq_onp_def by unfold_locales auto lemma Quotient_eq_onp_type_copy: "Quotient (=) Abs Rep cr \ type_definition Rep Abs UNIV" unfolding Quotient_def eq_onp_def by unfold_locales auto ML_file "Tools/BNF/bnf_lift.ML" hide_fact sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit image_map_sum_unit_subset subset_lift_sum_unitD UNIV_sum_unit_conv subset_vimage_image_subset relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty hypsubst equivp_add_relconj Grp_conversep_eq_onp Grp_conversep_nonempty relcomppI2 rel_conj_eq_onp Quotient_reflp_imp_equivp Quotient_Quotient3 end diff --git a/src/HOL/Transitive_Closure.thy b/src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy +++ b/src/HOL/Transitive_Closure.thy @@ -1,1345 +1,1356 @@ (* Title: HOL/Transitive_Closure.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) section \Reflexive and Transitive closure of a relation\ theory Transitive_Closure imports Relation abbrevs "^*" = "\<^sup>*" "\<^sup>*\<^sup>*" and "^+" = "\<^sup>+" "\<^sup>+\<^sup>+" and "^=" = "\<^sup>=" "\<^sup>=\<^sup>=" begin ML_file \~~/src/Provers/trancl.ML\ text \ \rtrancl\ is reflexive/transitive closure, \trancl\ is transitive closure, \reflcl\ is reflexive closure. These postfix operators have \<^emph>\maximum priority\, forcing their operands to be atomic. \ context notes [[inductive_internals]] begin inductive_set rtrancl :: "('a \ 'a) set \ ('a \ 'a) set" ("(_\<^sup>*)" [1000] 999) for r :: "('a \ 'a) set" where rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \ r\<^sup>*" | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \ r\<^sup>* \ (b, c) \ r \ (a, c) \ r\<^sup>*" inductive_set trancl :: "('a \ 'a) set \ ('a \ 'a) set" ("(_\<^sup>+)" [1000] 999) for r :: "('a \ 'a) set" where r_into_trancl [intro, Pure.intro]: "(a, b) \ r \ (a, b) \ r\<^sup>+" | trancl_into_trancl [Pure.intro]: "(a, b) \ r\<^sup>+ \ (b, c) \ r \ (a, c) \ r\<^sup>+" notation rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) declare rtrancl_def [nitpick_unfold del] rtranclp_def [nitpick_unfold del] trancl_def [nitpick_unfold del] tranclp_def [nitpick_unfold del] end abbreviation reflcl :: "('a \ 'a) set \ ('a \ 'a) set" ("(_\<^sup>=)" [1000] 999) where "r\<^sup>= \ r \ Id" abbreviation reflclp :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000) where "r\<^sup>=\<^sup>= \ sup r (=)" notation (ASCII) rtrancl ("(_^*)" [1000] 999) and trancl ("(_^+)" [1000] 999) and reflcl ("(_^=)" [1000] 999) and rtranclp ("(_^**)" [1000] 1000) and tranclp ("(_^++)" [1000] 1000) and reflclp ("(_^==)" [1000] 1000) subsection \Reflexive closure\ lemma refl_reflcl[simp]: "refl (r\<^sup>=)" by (simp add: refl_on_def) lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r" by (simp add: antisym_def) lemma trans_reflclI[simp]: "trans r \ trans (r\<^sup>=)" unfolding trans_def by blast lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>=" by blast subsection \Reflexive-transitive closure\ lemma reflcl_set_eq [pred_set_conv]: "(sup (\x y. (x, y) \ r) (=)) = (\x y. (x, y) \ r \ Id)" by (auto simp: fun_eq_iff) lemma r_into_rtrancl [intro]: "\p. p \ r \ p \ r\<^sup>*" \ \\rtrancl\ of \r\ contains \r\\ - apply (simp only: split_tupled_all) - apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) - done + by (simp add: split_tupled_all rtrancl_refl [THEN rtrancl_into_rtrancl]) lemma r_into_rtranclp [intro]: "r x y \ r\<^sup>*\<^sup>* x y" \ \\rtrancl\ of \r\ contains \r\\ by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) lemma rtranclp_mono: "r \ s \ r\<^sup>*\<^sup>* \ s\<^sup>*\<^sup>*" \ \monotonicity of \rtrancl\\ - apply (rule predicate2I) - apply (erule rtranclp.induct) - apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) - done +proof (rule predicate2I) + show "s\<^sup>*\<^sup>* x y" if "r \ s" "r\<^sup>*\<^sup>* x y" for x y + using \r\<^sup>*\<^sup>* x y\ \r \ s\ + by (induction rule: rtranclp.induct) (blast intro: rtranclp.rtrancl_into_rtrancl)+ +qed lemma mono_rtranclp[mono]: "(\a b. x a b \ y a b) \ x\<^sup>*\<^sup>* a b \ y\<^sup>*\<^sup>* a b" using rtranclp_mono[of x y] by auto lemmas rtrancl_mono = rtranclp_mono [to_set] theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: assumes a: "r\<^sup>*\<^sup>* a b" and cases: "P a" "\y z. r\<^sup>*\<^sup>* a y \ r y z \ P y \ P z" shows "P b" using a by (induct x\a b) (rule cases)+ lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] lemmas rtranclp_induct2 = rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] lemmas rtrancl_induct2 = rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] lemma refl_rtrancl: "refl (r\<^sup>*)" unfolding refl_on_def by fast text \Transitivity of transitive closure.\ lemma trans_rtrancl: "trans (r\<^sup>*)" proof (rule transI) fix x y z assume "(x, y) \ r\<^sup>*" assume "(y, z) \ r\<^sup>*" then show "(x, z) \ r\<^sup>*" proof induct case base show "(x, y) \ r\<^sup>*" by fact next case (step u v) from \(x, u) \ r\<^sup>*\ and \(u, v) \ r\ show "(x, v) \ r\<^sup>*" .. qed qed lemmas rtrancl_trans = trans_rtrancl [THEN transD] lemma rtranclp_trans: assumes "r\<^sup>*\<^sup>* x y" and "r\<^sup>*\<^sup>* y z" shows "r\<^sup>*\<^sup>* x z" using assms(2,1) by induct iprover+ lemma rtranclE [cases set: rtrancl]: fixes a b :: 'a assumes major: "(a, b) \ r\<^sup>*" obtains (base) "a = b" | (step) y where "(a, y) \ r\<^sup>*" and "(y, b) \ r" \ \elimination of \rtrancl\ -- by induction on a special formula\ proof - have "a = b \ (\y. (a, y) \ r\<^sup>* \ (y, b) \ r)" by (rule major [THEN rtrancl_induct]) blast+ then show ?thesis by (auto intro: base step) qed lemma rtrancl_Int_subset: "Id \ s \ (r\<^sup>* \ s) O r \ s \ r\<^sup>* \ s" - apply clarify - apply (erule rtrancl_induct, auto) - done + by (fastforce elim: rtrancl_induct) lemma converse_rtranclp_into_rtranclp: "r a b \ r\<^sup>*\<^sup>* b c \ r\<^sup>*\<^sup>* a c" by (rule rtranclp_trans) iprover+ lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] text \\<^medskip> More \<^term>\r\<^sup>*\ equations and inclusions.\ lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" - apply (auto intro!: order_antisym) - apply (erule rtranclp_induct) - apply (rule rtranclp.rtrancl_refl) - apply (blast intro: rtranclp_trans) - done +proof - + have "r\<^sup>*\<^sup>*\<^sup>*\<^sup>* x y \ r\<^sup>*\<^sup>* x y" for x y + by (induction rule: rtranclp_induct) (blast intro: rtranclp_trans)+ + then show ?thesis + by (auto intro!: order_antisym) +qed lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] lemma rtrancl_idemp_self_comp [simp]: "R\<^sup>* O R\<^sup>* = R\<^sup>*" - apply (rule set_eqI) - apply (simp only: split_tupled_all) - apply (blast intro: rtrancl_trans) - done + by (force intro: rtrancl_trans) lemma rtrancl_subset_rtrancl: "r \ s\<^sup>* \ r\<^sup>* \ s\<^sup>*" -by (drule rtrancl_mono, simp) + by (drule rtrancl_mono, simp) lemma rtranclp_subset: "R \ S \ S \ R\<^sup>*\<^sup>* \ S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" - apply (drule rtranclp_mono) - apply (drule rtranclp_mono, simp) - done + by (fastforce dest: rtranclp_mono) lemmas rtrancl_subset = rtranclp_subset [to_set] lemma rtranclp_sup_rtranclp: "(sup (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*))\<^sup>*\<^sup>* = (sup R S)\<^sup>*\<^sup>*" by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] lemma rtranclp_reflclp [simp]: "(R\<^sup>=\<^sup>=)\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" by (blast intro!: rtranclp_subset) lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set] lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*" by (rule rtrancl_subset [symmetric]) auto lemma rtranclp_r_diff_Id: "(inf r (\))\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" by (rule rtranclp_subset [symmetric]) auto theorem rtranclp_converseD: assumes "(r\\)\<^sup>*\<^sup>* x y" shows "r\<^sup>*\<^sup>* y x" using assms by induct (iprover intro: rtranclp_trans dest!: conversepD)+ lemmas rtrancl_converseD = rtranclp_converseD [to_set] theorem rtranclp_converseI: assumes "r\<^sup>*\<^sup>* y x" shows "(r\\)\<^sup>*\<^sup>* x y" using assms by induct (iprover intro: rtranclp_trans conversepI)+ lemmas rtrancl_converseI = rtranclp_converseI [to_set] lemma rtrancl_converse: "(r\)\<^sup>* = (r\<^sup>*)\" by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) lemma sym_rtrancl: "sym r \ sym (r\<^sup>*)" by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) theorem converse_rtranclp_induct [consumes 1, case_names base step]: assumes major: "r\<^sup>*\<^sup>* a b" and cases: "P b" "\y z. r y z \ r\<^sup>*\<^sup>* z b \ P z \ P y" shows "P a" using rtranclp_converseI [OF major] by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] lemmas converse_rtranclp_induct2 = converse_rtranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names refl step] lemmas converse_rtrancl_induct2 = converse_rtrancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete), consumes 1, case_names refl step] lemma converse_rtranclpE [consumes 1, case_names base step]: assumes major: "r\<^sup>*\<^sup>* x z" and cases: "x = z \ P" "\y. r x y \ r\<^sup>*\<^sup>* y z \ P" shows P proof - have "x = z \ (\y. r x y \ r\<^sup>*\<^sup>* y z)" by (rule_tac major [THEN converse_rtranclp_induct]) iprover+ then show ?thesis by (auto intro: cases) qed lemmas converse_rtranclE = converse_rtranclpE [to_set] lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r" by (blast elim: rtranclE converse_rtranclE intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) lemma rtrancl_unfold: "r\<^sup>* = Id \ r\<^sup>* O r" by (auto intro: rtrancl_into_rtrancl elim: rtranclE) lemma rtrancl_Un_separatorE: "(a, b) \ (P \ Q)\<^sup>* \ \x y. (a, x) \ P\<^sup>* \ (x, y) \ Q \ x = y \ (a, b) \ P\<^sup>*" proof (induct rule: rtrancl.induct) case rtrancl_refl then show ?case by blast next case rtrancl_into_rtrancl then show ?case by (blast intro: rtrancl_trans) qed lemma rtrancl_Un_separator_converseE: "(a, b) \ (P \ Q)\<^sup>* \ \x y. (x, b) \ P\<^sup>* \ (y, x) \ Q \ y = x \ (a, b) \ P\<^sup>*" proof (induct rule: converse_rtrancl_induct) case base then show ?case by blast next case step then show ?case by (blast intro: rtrancl_trans) qed lemma Image_closed_trancl: assumes "r `` X \ X" shows "r\<^sup>* `` X = X" proof - from assms have **: "{y. \x\X. (x, y) \ r} \ X" by auto have "x \ X" if 1: "(y, x) \ r\<^sup>*" and 2: "y \ X" for x y proof - from 1 show "x \ X" proof induct case base show ?case by (fact 2) next case step with ** show ?case by auto qed qed then show ?thesis by auto qed subsection \Transitive closure\ -lemma trancl_mono: "\p. p \ r\<^sup>+ \ r \ s \ p \ s\<^sup>+" - apply (simp add: split_tupled_all) - apply (erule trancl.induct) - apply (iprover dest: subsetD)+ - done +lemma trancl_mono: + assumes "p \ r\<^sup>+" "r \ s" + shows "p \ s\<^sup>+" +proof - + have "\(a, b) \ r\<^sup>+; r \ s\ \ (a, b) \ s\<^sup>+" for a b + by (induction rule: trancl.induct) (iprover dest: subsetD)+ + with assms show ?thesis + by (cases p) force +qed lemma r_into_trancl': "\p. p \ r \ p \ r\<^sup>+" by (simp only: split_tupled_all) (erule r_into_trancl) text \\<^medskip> Conversions between \trancl\ and \rtrancl\.\ lemma tranclp_into_rtranclp: "r\<^sup>+\<^sup>+ a b \ r\<^sup>*\<^sup>* a b" by (erule tranclp.induct) iprover+ lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] lemma rtranclp_into_tranclp1: assumes "r\<^sup>*\<^sup>* a b" shows "r b c \ r\<^sup>+\<^sup>+ a c" using assms by (induct arbitrary: c) iprover+ lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] -lemma rtranclp_into_tranclp2: "r a b \ r\<^sup>*\<^sup>* b c \ r\<^sup>+\<^sup>+ a c" +lemma rtranclp_into_tranclp2: + assumes "r a b" "r\<^sup>*\<^sup>* b c" shows "r\<^sup>+\<^sup>+ a c" \ \intro rule from \r\ and \rtrancl\\ - apply (erule rtranclp.cases, iprover) - apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) - apply (simp | rule r_into_rtranclp)+ - done + using \r\<^sup>*\<^sup>* b c\ +proof (cases rule: rtranclp.cases) + case rtrancl_refl + with assms show ?thesis + by iprover +next + case rtrancl_into_rtrancl + with assms show ?thesis + by (auto intro: rtranclp_trans [THEN rtranclp_into_tranclp1]) +qed lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] text \Nice induction rule for \trancl\\ lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: assumes a: "r\<^sup>+\<^sup>+ a b" and cases: "\y. r a y \ P y" "\y z. r\<^sup>+\<^sup>+ a y \ r y z \ P y \ P z" shows "P b" using a by (induct x\a b) (iprover intro: cases)+ lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] lemmas tranclp_induct2 = tranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names base step] lemmas trancl_induct2 = trancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete), consumes 1, case_names base step] lemma tranclp_trans_induct: assumes major: "r\<^sup>+\<^sup>+ x y" and cases: "\x y. r x y \ P x y" "\x y z. r\<^sup>+\<^sup>+ x y \ P x y \ r\<^sup>+\<^sup>+ y z \ P y z \ P x z" shows "P x y" \ \Another induction rule for trancl, incorporating transitivity\ by (iprover intro: major [THEN tranclp_induct] cases) lemmas trancl_trans_induct = tranclp_trans_induct [to_set] lemma tranclE [cases set: trancl]: assumes "(a, b) \ r\<^sup>+" obtains (base) "(a, b) \ r" | (step) c where "(a, c) \ r\<^sup>+" and "(c, b) \ r" using assms by cases simp_all lemma trancl_Int_subset: "r \ s \ (r\<^sup>+ \ s) O r \ s \ r\<^sup>+ \ s" - apply clarify - apply (erule trancl_induct, auto) - done + by (fastforce simp add: elim: trancl_induct) lemma trancl_unfold: "r\<^sup>+ = r \ r\<^sup>+ O r" by (auto intro: trancl_into_trancl elim: tranclE) text \Transitivity of \<^term>\r\<^sup>+\\ lemma trans_trancl [simp]: "trans (r\<^sup>+)" proof (rule transI) fix x y z assume "(x, y) \ r\<^sup>+" assume "(y, z) \ r\<^sup>+" then show "(x, z) \ r\<^sup>+" proof induct case (base u) from \(x, y) \ r\<^sup>+\ and \(y, u) \ r\ show "(x, u) \ r\<^sup>+" .. next case (step u v) from \(x, u) \ r\<^sup>+\ and \(u, v) \ r\ show "(x, v) \ r\<^sup>+" .. qed qed lemmas trancl_trans = trans_trancl [THEN transD] lemma tranclp_trans: assumes "r\<^sup>+\<^sup>+ x y" and "r\<^sup>+\<^sup>+ y z" shows "r\<^sup>+\<^sup>+ x z" using assms(2,1) by induct iprover+ lemma trancl_id [simp]: "trans r \ r\<^sup>+ = r" - apply auto - apply (erule trancl_induct, assumption) - apply (unfold trans_def, blast) - done + unfolding trans_def by (fastforce simp add: elim: trancl_induct) lemma rtranclp_tranclp_tranclp: assumes "r\<^sup>*\<^sup>* x y" shows "\z. r\<^sup>+\<^sup>+ y z \ r\<^sup>+\<^sup>+ x z" using assms by induct (iprover intro: tranclp_trans)+ lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] lemma tranclp_into_tranclp2: "r a b \ r\<^sup>+\<^sup>+ b c \ r\<^sup>+\<^sup>+ a c" by (erule tranclp_trans [OF tranclp.r_into_trancl]) lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] -lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\\ x y \ (r\\)\<^sup>+\<^sup>+ x y" - apply (drule conversepD) - apply (erule tranclp_induct) - apply (iprover intro: conversepI tranclp_trans)+ - done +lemma tranclp_converseI: + assumes "(r\<^sup>+\<^sup>+)\\ x y" shows "(r\\)\<^sup>+\<^sup>+ x y" + using conversepD [OF assms] +proof (induction rule: tranclp_induct) + case (base y) + then show ?case + by (iprover intro: conversepI) +next + case (step y z) + then show ?case + by (iprover intro: conversepI tranclp_trans) +qed lemmas trancl_converseI = tranclp_converseI [to_set] -lemma tranclp_converseD: "(r\\)\<^sup>+\<^sup>+ x y \ (r\<^sup>+\<^sup>+)\\ x y" - apply (rule conversepI) - apply (erule tranclp_induct) - apply (iprover dest: conversepD intro: tranclp_trans)+ - done +lemma tranclp_converseD: + assumes "(r\\)\<^sup>+\<^sup>+ x y" shows "(r\<^sup>+\<^sup>+)\\ x y" +proof - + have "r\<^sup>+\<^sup>+ y x" + using assms + by (induction rule: tranclp_induct) (iprover dest: conversepD intro: tranclp_trans)+ + then show ?thesis + by (rule conversepI) +qed lemmas trancl_converseD = tranclp_converseD [to_set] lemma tranclp_converse: "(r\\)\<^sup>+\<^sup>+ = (r\<^sup>+\<^sup>+)\\" by (fastforce simp add: fun_eq_iff intro!: tranclp_converseI dest!: tranclp_converseD) lemmas trancl_converse = tranclp_converse [to_set] lemma sym_trancl: "sym r \ sym (r\<^sup>+)" by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) lemma converse_tranclp_induct [consumes 1, case_names base step]: assumes major: "r\<^sup>+\<^sup>+ a b" and cases: "\y. r y b \ P y" "\y z. r y z \ r\<^sup>+\<^sup>+ z b \ P z \ P y" shows "P a" - apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) - apply (blast intro: cases) - apply (blast intro: assms dest!: tranclp_converseD) - done +proof - + have "r\\\<^sup>+\<^sup>+ b a" + by (intro tranclp_converseI conversepI major) + then show ?thesis + by (induction rule: tranclp_induct) (blast intro: cases dest: tranclp_converseD)+ +qed lemmas converse_trancl_induct = converse_tranclp_induct [to_set] lemma tranclpD: "R\<^sup>+\<^sup>+ x y \ \z. R x z \ R\<^sup>*\<^sup>* z y" - apply (erule converse_tranclp_induct, auto) - apply (blast intro: rtranclp_trans) - done +proof (induction rule: converse_tranclp_induct) + case (step u v) + then show ?case + by (blast intro: rtranclp_trans) +qed auto lemmas tranclD = tranclpD [to_set] lemma converse_tranclpE: assumes major: "tranclp r x z" and base: "r x z \ P" and step: "\y. r x y \ tranclp r y z \ P" shows P proof - from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z" by iprover from this(2) show P proof (cases rule: rtranclp.cases) case rtrancl_refl with \r x y\ base show P by iprover next case rtrancl_into_rtrancl - from this have "tranclp r y z" + then have "tranclp r y z" by (iprover intro: rtranclp_into_tranclp1) with \r x y\ step show P by iprover qed qed lemmas converse_tranclE = converse_tranclpE [to_set] lemma tranclD2: "(x, y) \ R\<^sup>+ \ \z. (x, z) \ R\<^sup>* \ (z, y) \ R" by (blast elim: tranclE intro: trancl_into_rtrancl) lemma irrefl_tranclI: "r\ \ r\<^sup>* = {} \ (x, x) \ r\<^sup>+" by (blast elim: tranclE dest: trancl_into_rtrancl) lemma irrefl_trancl_rD: "\x. (x, x) \ r\<^sup>+ \ (x, y) \ r \ x \ y" by (blast dest: r_into_trancl) lemma trancl_subset_Sigma_aux: "(a, b) \ r\<^sup>* \ r \ A \ A \ a = b \ a \ A" by (induct rule: rtrancl_induct) auto -lemma trancl_subset_Sigma: "r \ A \ A \ r\<^sup>+ \ A \ A" - apply (clarsimp simp:) - apply (erule tranclE) - apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ - done +lemma trancl_subset_Sigma: + assumes "r \ A \ A" shows "r\<^sup>+ \ A \ A" +proof (rule trancl_Int_subset [OF assms]) + show "(r\<^sup>+ \ A \ A) O r \ A \ A" + using assms by auto +qed lemma reflclp_tranclp [simp]: "(r\<^sup>+\<^sup>+)\<^sup>=\<^sup>= = r\<^sup>*\<^sup>*" - apply (safe intro!: order_antisym) - apply (erule tranclp_into_rtranclp) - apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) - done + by (fast elim: rtranclp.cases tranclp_into_rtranclp dest: rtranclp_into_tranclp1) lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set] lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" proof - have "(a, b) \ (r\<^sup>=)\<^sup>+ \ (a, b) \ r\<^sup>*" for a b by (force dest: trancl_into_rtrancl) moreover have "(a, b) \ (r\<^sup>=)\<^sup>+" if "(a, b) \ r\<^sup>*" for a b using that proof (cases a b rule: rtranclE) case step show ?thesis by (rule rtrancl_into_trancl1) (use step in auto) qed auto ultimately show ?thesis by auto qed lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>=" by simp lemma trancl_empty [simp]: "{}\<^sup>+ = {}" by (auto elim: trancl_induct) lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" by (rule subst [OF reflcl_trancl]) simp lemma rtranclpD: "R\<^sup>*\<^sup>* a b \ a = b \ a \ b \ R\<^sup>+\<^sup>+ a b" by (force simp: reflclp_tranclp [symmetric] simp del: reflclp_tranclp) lemmas rtranclD = rtranclpD [to_set] lemma rtrancl_eq_or_trancl: "(x,y) \ R\<^sup>* \ x = y \ x \ y \ (x, y) \ R\<^sup>+" by (fast elim: trancl_into_rtrancl dest: rtranclD) lemma trancl_unfold_right: "r\<^sup>+ = r\<^sup>* O r" by (auto dest: tranclD2 intro: rtrancl_into_trancl1) lemma trancl_unfold_left: "r\<^sup>+ = r O r\<^sup>*" by (auto dest: tranclD intro: rtrancl_into_trancl2) lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \ {(a, b). (a, y) \ r\<^sup>* \ (x, b) \ r\<^sup>*}" \ \primitive recursion for \trancl\ over finite relations\ proof - have "\a b. (a, b) \ (insert (y, x) r)\<^sup>+ \ (a, b) \ r\<^sup>+ \ {(a, b). (a, y) \ r\<^sup>* \ (x, b) \ r\<^sup>*}" by (erule trancl_induct) (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)+ moreover have "r\<^sup>+ \ {(a, b). (a, y) \ r\<^sup>* \ (x, b) \ r\<^sup>*} \ (insert (y, x) r)\<^sup>+" by (blast intro: trancl_mono rtrancl_mono [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) ultimately show ?thesis by auto qed lemma trancl_insert2: "(insert (a, b) r)\<^sup>+ = r\<^sup>+ \ {(x, y). ((x, a) \ r\<^sup>+ \ x = a) \ ((b, y) \ r\<^sup>+ \ y = b)}" by (auto simp: trancl_insert rtrancl_eq_or_trancl) lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \ {(x, y). (x, a) \ r\<^sup>* \ (b, y) \ r\<^sup>*}" using trancl_insert[of a b r] by (simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast text \Simplifying nested closures\ lemma rtrancl_trancl_absorb[simp]: "(R\<^sup>*)\<^sup>+ = R\<^sup>*" by (simp add: trans_rtrancl) lemma trancl_rtrancl_absorb[simp]: "(R\<^sup>+)\<^sup>* = R\<^sup>*" by (subst reflcl_trancl[symmetric]) simp lemma rtrancl_reflcl_absorb[simp]: "(R\<^sup>*)\<^sup>= = R\<^sup>*" by auto text \\Domain\ and \Range\\ lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" by blast lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" by blast lemma rtrancl_Un_subset: "(R\<^sup>* \ S\<^sup>*) \ (R \ S)\<^sup>*" by (rule rtrancl_Un_rtrancl [THEN subst]) fast lemma in_rtrancl_UnI: "x \ R\<^sup>* \ x \ S\<^sup>* \ x \ (R \ S)\<^sup>*" by (blast intro: subsetD [OF rtrancl_Un_subset]) lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" by (unfold Domain_unfold) (blast dest: tranclD) lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric]) lemma Not_Domain_rtrancl: assumes "x \ Domain R" shows "(x, y) \ R\<^sup>* \ x = y" proof - have "(x, y) \ R\<^sup>* \ x = y" by (erule rtrancl_induct) (use assms in auto) then show ?thesis by auto qed lemma trancl_subset_Field2: "r\<^sup>+ \ Field r \ Field r" - apply clarify - apply (erule trancl_induct) - apply (auto simp: Field_def) - done + by (rule trancl_Int_subset) (auto simp: Field_def) lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r" proof show "finite (r\<^sup>+) \ finite r" by (blast intro: r_into_trancl' finite_subset) show "finite r \ finite (r\<^sup>+)" - apply (rule trancl_subset_Field2 [THEN finite_subset]) - apply (auto simp: finite_Field) - done + by (auto simp: finite_Field trancl_subset_Field2 [THEN finite_subset]) qed lemma finite_rtrancl_Image[simp]: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)" proof (rule ccontr) assume "infinite (R\<^sup>* `` A)" with assms show False by(simp add: rtrancl_trancl_reflcl Un_Image del: reflcl_trancl) qed text \More about converse \rtrancl\ and \trancl\, should be merged with main body.\ lemma single_valued_confluent: assumes "single_valued r" and xy: "(x, y) \ r\<^sup>*" and xz: "(x, z) \ r\<^sup>*" shows "(y, z) \ r\<^sup>* \ (z, y) \ r\<^sup>*" using xy proof (induction rule: rtrancl_induct) case base show ?case by (simp add: assms) next case (step y z) with xz \single_valued r\ show ?case - apply (auto simp: elim: converse_rtranclE dest: single_valuedD) - apply (blast intro: rtrancl_trans) - done + by (auto elim: converse_rtranclE dest: single_valuedD intro: rtrancl_trans) qed lemma r_r_into_trancl: "(a, b) \ R \ (b, c) \ R \ (a, c) \ R\<^sup>+" by (fast intro: trancl_trans) lemma trancl_into_trancl: "(a, b) \ r\<^sup>+ \ (b, c) \ r \ (a, c) \ r\<^sup>+" by (induct rule: trancl_induct) (fast intro: r_r_into_trancl trancl_trans)+ -lemma tranclp_rtranclp_tranclp: "r\<^sup>+\<^sup>+ a b \ r\<^sup>*\<^sup>* b c \ r\<^sup>+\<^sup>+ a c" - apply (drule tranclpD) - apply (elim exE conjE) - apply (drule rtranclp_trans, assumption) - apply (drule (2) rtranclp_into_tranclp2) - done +lemma tranclp_rtranclp_tranclp: + assumes "r\<^sup>+\<^sup>+ a b" "r\<^sup>*\<^sup>* b c" shows "r\<^sup>+\<^sup>+ a c" +proof - + obtain z where "r a z" "r\<^sup>*\<^sup>* z c" + using assms by (iprover dest: tranclpD rtranclp_trans) + then show ?thesis + by (blast dest: rtranclp_into_tranclp2) +qed lemma rtranclp_conversep: "r\\\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*\\" by(auto simp add: fun_eq_iff intro: rtranclp_converseI rtranclp_converseD) lemmas symp_rtranclp = sym_rtrancl[to_pred] lemmas symp_conv_conversep_eq = sym_conv_converse_eq[to_pred] lemmas rtranclp_tranclp_absorb [simp] = rtrancl_trancl_absorb[to_pred] lemmas tranclp_rtranclp_absorb [simp] = trancl_rtrancl_absorb[to_pred] lemmas rtranclp_reflclp_absorb [simp] = rtrancl_reflcl_absorb[to_pred] lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] lemmas transitive_closure_trans [trans] = r_r_into_trancl trancl_trans rtrancl_trans trancl.trancl_into_trancl trancl_into_trancl2 rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl rtrancl_trancl_trancl trancl_rtrancl_trancl lemmas transitive_closurep_trans' [trans] = tranclp_trans rtranclp_trans tranclp.trancl_into_trancl tranclp_into_tranclp2 rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp declare trancl_into_rtrancl [elim] subsection \Symmetric closure\ definition symclp :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" where "symclp r x y \ r x y \ r y x" lemma symclpI [simp, intro?]: shows symclpI1: "r x y \ symclp r x y" - and symclpI2: "r y x \ symclp r x y" -by(simp_all add: symclp_def) + and symclpI2: "r y x \ symclp r x y" + by(simp_all add: symclp_def) lemma symclpE [consumes 1, cases pred]: assumes "symclp r x y" obtains (base) "r x y" | (sym) "r y x" -using assms by(auto simp add: symclp_def) + using assms by(auto simp add: symclp_def) lemma symclp_pointfree: "symclp r = sup r r\\" by(auto simp add: symclp_def fun_eq_iff) lemma symclp_greater: "r \ symclp r" by(simp add: symclp_pointfree) lemma symclp_conversep [simp]: "symclp r\\ = symclp r" by(simp add: symclp_pointfree sup.commute) lemma symp_symclp [simp]: "symp (symclp r)" by(auto simp add: symp_def elim: symclpE intro: symclpI) lemma symp_symclp_eq: "symp r \ symclp r = r" by(simp add: symclp_pointfree symp_conv_conversep_eq) lemma symp_rtranclp_symclp [simp]: "symp (symclp r)\<^sup>*\<^sup>*" by(simp add: symp_rtranclp) lemma rtranclp_symclp_sym [sym]: "(symclp r)\<^sup>*\<^sup>* x y \ (symclp r)\<^sup>*\<^sup>* y x" by(rule sympD[OF symp_rtranclp_symclp]) lemma symclp_idem [simp]: "symclp (symclp r) = symclp r" by(simp add: symclp_pointfree sup_commute converse_join) lemma reflp_rtranclp [simp]: "reflp R\<^sup>*\<^sup>*" using refl_rtrancl[to_pred, of R] reflp_refl_eq[of "{(x, y). R\<^sup>*\<^sup>* x y}"] by simp subsection \The power operation on relations\ text \\R ^^ n = R O \ O R\, the n-fold composition of \R\\ overloading relpow \ "compow :: nat \ ('a \ 'a) set \ ('a \ 'a) set" relpowp \ "compow :: nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" begin primrec relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where "relpow 0 R = Id" | "relpow (Suc n) R = (R ^^ n) O R" primrec relpowp :: "nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" where "relpowp 0 R = HOL.eq" | "relpowp (Suc n) R = (R ^^ n) OO R" end lemma relpowp_relpow_eq [pred_set_conv]: "(\x y. (x, y) \ R) ^^ n = (\x y. (x, y) \ R ^^ n)" for R :: "'a rel" by (induct n) (simp_all add: relcompp_relcomp_eq) text \For code generation:\ definition relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where relpow_code_def [code_abbrev]: "relpow = compow" definition relpowp :: "nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" where relpowp_code_def [code_abbrev]: "relpowp = compow" lemma [code]: "relpow (Suc n) R = (relpow n R) O R" "relpow 0 R = Id" by (simp_all add: relpow_code_def) lemma [code]: "relpowp (Suc n) R = (R ^^ n) OO R" "relpowp 0 R = HOL.eq" by (simp_all add: relpowp_code_def) hide_const (open) relpow hide_const (open) relpowp lemma relpow_1 [simp]: "R ^^ 1 = R" for R :: "('a \ 'a) set" by simp lemma relpowp_1 [simp]: "P ^^ 1 = P" for P :: "'a \ 'a \ bool" by (fact relpow_1 [to_pred]) lemma relpow_0_I: "(x, x) \ R ^^ 0" by simp lemma relpowp_0_I: "(P ^^ 0) x x" by (fact relpow_0_I [to_pred]) lemma relpow_Suc_I: "(x, y) \ R ^^ n \ (y, z) \ R \ (x, z) \ R ^^ Suc n" by auto lemma relpowp_Suc_I: "(P ^^ n) x y \ P y z \ (P ^^ Suc n) x z" by (fact relpow_Suc_I [to_pred]) lemma relpow_Suc_I2: "(x, y) \ R \ (y, z) \ R ^^ n \ (x, z) \ R ^^ Suc n" by (induct n arbitrary: z) (simp, fastforce) lemma relpowp_Suc_I2: "P x y \ (P ^^ n) y z \ (P ^^ Suc n) x z" by (fact relpow_Suc_I2 [to_pred]) lemma relpow_0_E: "(x, y) \ R ^^ 0 \ (x = y \ P) \ P" by simp lemma relpowp_0_E: "(P ^^ 0) x y \ (x = y \ Q) \ Q" by (fact relpow_0_E [to_pred]) lemma relpow_Suc_E: "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R ^^ n \ (y, z) \ R \ P) \ P" by auto lemma relpowp_Suc_E: "(P ^^ Suc n) x z \ (\y. (P ^^ n) x y \ P y z \ Q) \ Q" by (fact relpow_Suc_E [to_pred]) lemma relpow_E: "(x, z) \ R ^^ n \ (n = 0 \ x = z \ P) \ (\y m. n = Suc m \ (x, y) \ R ^^ m \ (y, z) \ R \ P) \ P" by (cases n) auto lemma relpowp_E: "(P ^^ n) x z \ (n = 0 \ x = z \ Q) \ (\y m. n = Suc m \ (P ^^ m) x y \ P y z \ Q) \ Q" by (fact relpow_E [to_pred]) lemma relpow_Suc_D2: "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R \ (y, z) \ R ^^ n)" by (induct n arbitrary: x z) (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+ lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \ \y. P x y \ (P ^^ n) y z" by (fact relpow_Suc_D2 [to_pred]) lemma relpow_Suc_E2: "(x, z) \ R ^^ Suc n \ (\y. (x, y) \ R \ (y, z) \ R ^^ n \ P) \ P" by (blast dest: relpow_Suc_D2) lemma relpowp_Suc_E2: "(P ^^ Suc n) x z \ (\y. P x y \ (P ^^ n) y z \ Q) \ Q" by (fact relpow_Suc_E2 [to_pred]) lemma relpow_Suc_D2': "\x y z. (x, y) \ R ^^ n \ (y, z) \ R \ (\w. (x, w) \ R \ (w, z) \ R ^^ n)" by (induct n) (simp_all, blast) lemma relpowp_Suc_D2': "\x y z. (P ^^ n) x y \ P y z \ (\w. P x w \ (P ^^ n) w z)" by (fact relpow_Suc_D2' [to_pred]) lemma relpow_E2: assumes "(x, z) \ R ^^ n" "n = 0 \ x = z \ P" "\y m. n = Suc m \ (x, y) \ R \ (y, z) \ R ^^ m \ P" shows "P" proof (cases n) case 0 with assms show ?thesis by simp next case (Suc m) with assms relpow_Suc_D2' [of m R] show ?thesis by force qed lemma relpowp_E2: "(P ^^ n) x z \ (n = 0 \ x = z \ Q) \ (\y m. n = Suc m \ P x y \ (P ^^ m) y z \ Q) \ Q" by (fact relpow_E2 [to_pred]) lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" by (induct n) auto lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" by (fact relpow_add [to_pred]) lemma relpow_commute: "R O R ^^ n = R ^^ n O R" by (induct n) (simp_all add: O_assoc [symmetric]) lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" by (fact relpow_commute [to_pred]) lemma relpow_empty: "0 < n \ ({} :: ('a \ 'a) set) ^^ n = {}" by (cases n) auto lemma relpowp_bot: "0 < n \ (\ :: 'a \ 'a \ bool) ^^ n = \" by (fact relpow_empty [to_pred]) lemma rtrancl_imp_UN_relpow: assumes "p \ R\<^sup>*" shows "p \ (\n. R ^^ n)" proof (cases p) case (Pair x y) with assms have "(x, y) \ R\<^sup>*" by simp then have "(x, y) \ (\n. R ^^ n)" proof induct case base show ?case by (blast intro: relpow_0_I) next case step then show ?case by (blast intro: relpow_Suc_I) qed with Pair show ?thesis by simp qed lemma rtranclp_imp_Sup_relpowp: assumes "(P\<^sup>*\<^sup>*) x y" shows "(\n. P ^^ n) x y" using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp lemma relpow_imp_rtrancl: assumes "p \ R ^^ n" shows "p \ R\<^sup>*" proof (cases p) case (Pair x y) with assms have "(x, y) \ R ^^ n" by simp then have "(x, y) \ R\<^sup>*" proof (induct n arbitrary: x y) case 0 then show ?case by simp next case Suc then show ?case by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) qed with Pair show ?thesis by simp qed lemma relpowp_imp_rtranclp: "(P ^^ n) x y \ (P\<^sup>*\<^sup>*) x y" using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\n. R ^^ n)" by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\n. P ^^ n)" using rtrancl_is_UN_relpow [to_pred, of P] by auto lemma rtrancl_power: "p \ R\<^sup>* \ (\n. p \ R ^^ n)" by (simp add: rtrancl_is_UN_relpow) lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \ (\n. (P ^^ n) x y)" by (simp add: rtranclp_is_Sup_relpowp) lemma trancl_power: "p \ R\<^sup>+ \ (\n > 0. p \ R ^^ n)" proof - - have "((a, b) \ R\<^sup>+) = (\n>0. (a, b) \ R ^^ n)" for a b + have "(a, b) \ R\<^sup>+ \ (\n>0. (a, b) \ R ^^ n)" for a b proof safe show "(a, b) \ R\<^sup>+ \ \n>0. (a, b) \ R ^^ n" - apply (drule tranclD2) - apply (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold) - done + by (fastforce simp: rtrancl_is_UN_relpow relcomp_unfold dest: tranclD2) show "(a, b) \ R\<^sup>+" if "n > 0" "(a, b) \ R ^^ n" for n proof (cases n) case (Suc m) with that show ?thesis by (auto simp: dest: relpow_imp_rtrancl rtrancl_into_trancl1) qed (use that in auto) qed then show ?thesis by (cases p) auto qed lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \ (\n > 0. (P ^^ n) x y)" using trancl_power [to_pred, of P "(x, y)"] by simp lemma rtrancl_imp_relpow: "p \ R\<^sup>* \ \n. p \ R ^^ n" by (auto dest: rtrancl_imp_UN_relpow) lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \ \n. (P ^^ n) x y" by (auto dest: rtranclp_imp_Sup_relpowp) text \By Sternagel/Thiemann:\ lemma relpow_fun_conv: "(a, b) \ R ^^ n \ (\f. f 0 = a \ f n = b \ (\i R))" proof (induct n arbitrary: b) case 0 show ?case by auto next case (Suc n) show ?case proof (simp add: relcomp_unfold Suc) show "(\y. (\f. f 0 = a \ f n = y \ (\i R)) \ (y,b) \ R) \ (\f. f 0 = a \ f(Suc n) = b \ (\i R))" (is "?l = ?r") proof assume ?l then obtain c f where 1: "f 0 = a" "f n = c" "\i. i < n \ (f i, f (Suc i)) \ R" "(c,b) \ R" by auto let ?g = "\ m. if m = Suc n then b else f m" show ?r by (rule exI[of _ ?g]) (simp add: 1) next assume ?r then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\i. i < Suc n \ (f i, f (Suc i)) \ R" by auto show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) qed qed qed lemma relpowp_fun_conv: "(P ^^ n) x y \ (\f. f 0 = x \ f n = y \ (\i 'a) set" assumes "finite R" and "k > 0" shows "R^^k \ (\n\{n. 0 < n \ n \ card R}. R^^n)" (is "_ \ ?r") proof - have "(a, b) \ R^^(Suc k) \ \n. 0 < n \ n \ card R \ (a, b) \ R^^n" for a b k proof (induct k arbitrary: b) case 0 then have "R \ {}" by auto with card_0_eq[OF \finite R\] have "card R \ Suc 0" by auto then show ?case using 0 by force next case (Suc k) then obtain a' where "(a, a') \ R^^(Suc k)" and "(a', b) \ R" by auto from Suc(1)[OF \(a, a') \ R^^(Suc k)\] obtain n where "n \ card R" and "(a, a') \ R ^^ n" by auto have "(a, b) \ R^^(Suc n)" using \(a, a') \ R^^n\ and \(a', b)\ R\ by auto from \n \ card R\ consider "n < card R" | "n = card R" by force then show ?case proof cases case 1 then show ?thesis using \(a, b) \ R^^(Suc n)\ Suc_leI[OF \n < card R\] by blast next case 2 from \(a, b) \ R ^^ (Suc n)\ [unfolded relpow_fun_conv] obtain f where "f 0 = a" and "f (Suc n) = b" and steps: "\i. i \ n \ (f i, f (Suc i)) \ R" by auto let ?p = "\i. (f i, f(Suc i))" let ?N = "{i. i \ n}" have "?p ` ?N \ R" using steps by auto from card_mono[OF assms(1) this] have "card (?p ` ?N) \ card R" . also have "\ < card ?N" using \n = card R\ by simp finally have "\ inj_on ?p ?N" by (rule pigeonhole) then obtain i j where i: "i \ n" and j: "j \ n" and ij: "i \ j" and pij: "?p i = ?p j" by (auto simp: inj_on_def) let ?i = "min i j" let ?j = "max i j" have i: "?i \ n" and j: "?j \ n" and pij: "?p ?i = ?p ?j" and ij: "?i < ?j" using i j ij pij unfolding min_def max_def by auto from i j pij ij obtain i j where i: "i \ n" and j: "j \ n" and ij: "i < j" and pij: "?p i = ?p j" by blast let ?g = "\l. if l \ i then f l else f (l + (j - i))" let ?n = "Suc (n - (j - i))" have abl: "(a, b) \ R ^^ ?n" unfolding relpow_fun_conv proof (rule exI[of _ ?g], intro conjI impI allI) show "?g ?n = b" using \f(Suc n) = b\ j ij by auto next fix k assume "k < ?n" show "(?g k, ?g (Suc k)) \ R" proof (cases "k < i") case True with i have "k \ n" by auto from steps[OF this] show ?thesis using True by simp next case False then have "i \ k" by auto show ?thesis proof (cases "k = i") case True then show ?thesis using ij pij steps[OF i] by simp next case False with \i \ k\ have "i < k" by auto then have small: "k + (j - i) \ n" using \k by arith show ?thesis using steps[OF small] \i by auto qed qed qed (simp add: \f 0 = a\) moreover have "?n \ n" using i j ij by arith ultimately show ?thesis using \n = card R\ by blast qed qed then show ?thesis using gr0_implies_Suc[OF \k > 0\] by auto qed lemma relpow_finite_bounded: fixes R :: "('a \ 'a) set" assumes "finite R" shows "R^^k \ (\n\{n. n \ card R}. R^^n)" - apply (cases k, force) - apply (use relpow_finite_bounded1[OF assms, of k] in auto) - done +proof (cases k) + case (Suc k') + then show ?thesis + using relpow_finite_bounded1[OF assms, of k] by auto +qed force lemma rtrancl_finite_eq_relpow: "finite R \ R\<^sup>* = (\n\{n. n \ card R}. R^^n)" by (fastforce simp: rtrancl_power dest: relpow_finite_bounded) -lemma trancl_finite_eq_relpow: "finite R \ R\<^sup>+ = (\n\{n. 0 < n \ n \ card R}. R^^n)" - apply (auto simp: trancl_power) - apply (auto dest: relpow_finite_bounded1) - done +lemma trancl_finite_eq_relpow: + assumes "finite R" shows "R\<^sup>+ = (\n\{n. 0 < n \ n \ card R}. R^^n)" +proof - + have "\a b n. \0 < n; (a, b) \ R ^^ n\ \ \x>0. x \ card R \ (a, b) \ R ^^ x" + using assms by (auto dest: relpow_finite_bounded1) + then show ?thesis + by (auto simp: trancl_power) +qed lemma finite_relcomp[simp,intro]: assumes "finite R" and "finite S" shows "finite (R O S)" proof- have "R O S = (\(x, y)\R. \(u, v)\S. if u = y then {(x, v)} else {})" by (force simp: split_def image_constant_conv split: if_splits) then show ?thesis using assms by clarsimp qed lemma finite_relpow [simp, intro]: fixes R :: "('a \ 'a) set" assumes "finite R" shows "n > 0 \ finite (R^^n)" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case by (cases n) (use assms in simp_all) qed lemma single_valued_relpow: fixes R :: "('a \ 'a) set" shows "single_valued R \ single_valued (R ^^ n)" proof (induct n arbitrary: R) case 0 then show ?case by simp next case (Suc n) show ?case by (rule single_valuedI) (use Suc in \fast dest: single_valuedD elim: relpow_Suc_E\) qed subsection \Bounded transitive closure\ definition ntrancl :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where "ntrancl n R = (\i\{i. 0 < i \ i \ Suc n}. R ^^ i)" lemma ntrancl_Zero [simp, code]: "ntrancl 0 R = R" proof show "R \ ntrancl 0 R" unfolding ntrancl_def by fastforce have "0 < i \ i \ Suc 0 \ i = 1" for i by auto then show "ntrancl 0 R \ R" unfolding ntrancl_def by auto qed lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \ R)" proof have "(a, b) \ ntrancl n R O (Id \ R)" if "(a, b) \ ntrancl (Suc n) R" for a b proof - from that obtain i where "0 < i" "i \ Suc (Suc n)" "(a, b) \ R ^^ i" unfolding ntrancl_def by auto show ?thesis proof (cases "i = 1") case True - from this \(a, b) \ R ^^ i\ show ?thesis + with \(a, b) \ R ^^ i\ show ?thesis by (auto simp: ntrancl_def) next case False with \0 < i\ obtain j where j: "i = Suc j" "0 < j" by (cases i) auto with \(a, b) \ R ^^ i\ obtain c where c1: "(a, c) \ R ^^ j" and c2: "(c, b) \ R" by auto from c1 j \i \ Suc (Suc n)\ have "(a, c) \ ntrancl n R" by (fastforce simp: ntrancl_def) with c2 show ?thesis by fastforce qed qed then show "ntrancl (Suc n) R \ ntrancl n R O (Id \ R)" by auto show "ntrancl n R O (Id \ R) \ ntrancl (Suc n) R" by (fastforce simp: ntrancl_def) qed lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \ r' O r)" by (auto simp: Let_def) lemma finite_trancl_ntranl: "finite R \ trancl R = ntrancl (card R - 1) R" by (cases "card R") (auto simp: trancl_finite_eq_relpow relpow_empty ntrancl_def) subsection \Acyclic relations\ definition acyclic :: "('a \ 'a) set \ bool" where "acyclic r \ (\x. (x,x) \ r\<^sup>+)" abbreviation acyclicP :: "('a \ 'a \ bool) \ bool" where "acyclicP r \ acyclic {(x, y). r x y}" lemma acyclic_irrefl [code]: "acyclic r \ irrefl (r\<^sup>+)" by (simp add: acyclic_def irrefl_def) lemma acyclicI: "\x. (x, x) \ r\<^sup>+ \ acyclic r" by (simp add: acyclic_def) lemma (in preorder) acyclicI_order: assumes *: "\a b. (a, b) \ r \ f b < f a" shows "acyclic r" proof - have "f b < f a" if "(a, b) \ r\<^sup>+" for a b using that by induct (auto intro: * less_trans) then show ?thesis by (auto intro!: acyclicI) qed lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \ acyclic r \ (x, y) \ r\<^sup>*" by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans) lemma acyclic_converse [iff]: "acyclic (r\) \ acyclic r" by (simp add: acyclic_def trancl_converse) lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] lemma acyclic_impl_antisym_rtrancl: "acyclic r \ antisym (r\<^sup>*)" by (simp add: acyclic_def antisym_def) (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) (* Other direction: acyclic = no loops antisym = only self loops Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \ acyclic(r - Id) \ antisym( r\<^sup>* ) = acyclic(r - Id)"; *) lemma acyclic_subset: "acyclic s \ r \ s \ acyclic r" unfolding acyclic_def by (blast intro: trancl_mono) subsection \Setup of transitivity reasoner\ ML \ structure Trancl_Tac = Trancl_Tac ( val r_into_trancl = @{thm trancl.r_into_trancl}; val trancl_trans = @{thm trancl_trans}; val rtrancl_refl = @{thm rtrancl.rtrancl_refl}; val r_into_rtrancl = @{thm r_into_rtrancl}; val trancl_into_rtrancl = @{thm trancl_into_rtrancl}; val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl}; val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl}; val rtrancl_trans = @{thm rtrancl_trans}; fun decomp (\<^const>\Trueprop\ $ t) = let fun dec (Const (\<^const_name>\Set.member\, _) $ (Const (\<^const_name>\Pair\, _) $ a $ b) $ rel) = let fun decr (Const (\<^const_name>\rtrancl\, _ ) $ r) = (r,"r*") | decr (Const (\<^const_name>\trancl\, _ ) $ r) = (r,"r+") | decr r = (r,"r"); val (rel,r) = decr (Envir.beta_eta_contract rel); in SOME (a,b,rel,r) end | dec _ = NONE in dec t end | decomp _ = NONE; ); structure Tranclp_Tac = Trancl_Tac ( val r_into_trancl = @{thm tranclp.r_into_trancl}; val trancl_trans = @{thm tranclp_trans}; val rtrancl_refl = @{thm rtranclp.rtrancl_refl}; val r_into_rtrancl = @{thm r_into_rtranclp}; val trancl_into_rtrancl = @{thm tranclp_into_rtranclp}; val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp}; val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp}; val rtrancl_trans = @{thm rtranclp_trans}; fun decomp (\<^const>\Trueprop\ $ t) = let fun dec (rel $ a $ b) = let fun decr (Const (\<^const_name>\rtranclp\, _ ) $ r) = (r,"r*") | decr (Const (\<^const_name>\tranclp\, _ ) $ r) = (r,"r+") | decr r = (r,"r"); val (rel,r) = decr rel; in SOME (a, b, rel, r) end | dec _ = NONE in dec t end | decomp _ = NONE; ); \ setup \ map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac) addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac) addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac) addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac)) \ lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*" by(auto simp add: transp_def) text \Optional methods.\ method_setup trancl = \Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\ \simple transitivity reasoner\ method_setup rtrancl = \Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\ \simple transitivity reasoner\ method_setup tranclp = \Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\ \simple transitivity reasoner (predicate version)\ method_setup rtranclp = \Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\ \simple transitivity reasoner (predicate version)\ end