src/HOL/Transitive_Closure.thy
 changeset 60758 d8d85a8172b5 parent 60681 9ce7463350a9 child 61032 b57df8eecad6
--- a/src/HOL/Transitive_Closure.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -3,7 +3,7 @@
*)

-section {* Reflexive and Transitive closure of a relation *}
+section \<open>Reflexive and Transitive closure of a relation\<close>

theory Transitive_Closure
imports Relation
@@ -11,14 +11,14 @@

ML_file "~~/src/Provers/trancl.ML"

-text {*
+text \<open>
@{text rtrancl} is reflexive/transitive closure,
@{text trancl} is transitive closure,
@{text reflcl} is reflexive closure.

These postfix operators have \emph{maximum priority}, forcing their
operands to be atomic.
-*}
+\<close>

inductive_set
rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"   ("(_^*)"  999)
@@ -68,7 +68,7 @@
reflcl  ("(_\<^sup>=)"  999)

-subsection {* Reflexive closure *}
+subsection \<open>Reflexive closure\<close>

lemma refl_reflcl[simp]: "refl(r^=)"
@@ -82,23 +82,23 @@
lemma reflclp_idemp [simp]: "(P^==)^==  =  P^=="
by blast

-subsection {* Reflexive-transitive closure *}
+subsection \<open>Reflexive-transitive closure\<close>

lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"

lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
-  -- {* @{text rtrancl} of @{text r} contains @{text r} *}
+  -- \<open>@{text rtrancl} of @{text r} contains @{text r}\<close>
apply (simp only: split_tupled_all)
apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
done

lemma r_into_rtranclp [intro]: "r x y ==> r^** x y"
-  -- {* @{text rtrancl} of @{text r} contains @{text r} *}
+  -- \<open>@{text rtrancl} of @{text r} contains @{text r}\<close>
by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl])

lemma rtranclp_mono: "r \<le> s ==> r^** \<le> s^**"
-  -- {* monotonicity of @{text rtrancl} *}
+  -- \<open>monotonicity of @{text rtrancl}\<close>
apply (rule predicate2I)
apply (erule rtranclp.induct)
apply (rule_tac  rtranclp.rtrancl_into_rtrancl, blast+)
@@ -129,7 +129,7 @@
lemma refl_rtrancl: "refl (r^*)"
by (unfold refl_on_def) fast

-text {* Transitivity of transitive closure. *}
+text \<open>Transitivity of transitive closure.\<close>
lemma trans_rtrancl: "trans (r^*)"
proof (rule transI)
fix x y z
@@ -141,7 +141,7 @@
show "(x, y) \<in> r\<^sup>*" by fact
next
case (step u v)
-    from (x, u) \<in> r\<^sup>* and (u, v) \<in> r
+    from \<open>(x, u) \<in> r\<^sup>*\<close> and \<open>(u, v) \<in> r\<close>
show "(x, v) \<in> r\<^sup>*" ..
qed
qed
@@ -159,7 +159,7 @@
obtains
(base) "a = b"
| (step) y where "(a, y) : r^*" and "(y, b) : r"
-  -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
+  -- \<open>elimination of @{text rtrancl} -- by induction on a special formula\<close>
apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
apply (rule_tac  major [THEN rtrancl_induct])
prefer 2 apply blast
@@ -179,9 +179,9 @@

lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]

-text {*
+text \<open>
\medskip More @{term "r^*"} equations and inclusions.
-*}
+\<close>

lemma rtranclp_idemp [simp]: "(r^**)^** = r^**"
apply (auto intro!: order_antisym)
@@ -336,7 +336,7 @@
qed

-subsection {* Transitive closure *}
+subsection \<open>Transitive closure\<close>

lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
@@ -347,9 +347,9 @@
lemma r_into_trancl': "!!p. p : r ==> p : r^+"
by (simp only: split_tupled_all) (erule r_into_trancl)

-text {*
+text \<open>
\medskip Conversions between @{text trancl} and @{text rtrancl}.
-*}
+\<close>

lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b"
by (erule tranclp.induct) iprover+
@@ -363,7 +363,7 @@
lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]

lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c"
-  -- {* intro rule from @{text r} and @{text rtrancl} *}
+  -- \<open>intro rule from @{text r} and @{text rtrancl}\<close>
apply (erule rtranclp.cases)
apply iprover
apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])
@@ -372,7 +372,7 @@

lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]

-text {* Nice induction rule for @{text trancl} *}
+text \<open>Nice induction rule for @{text trancl}\<close>
lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:
assumes a: "r^++ a b"
and cases: "!!y. r a y ==> P y"
@@ -395,7 +395,7 @@
and cases: "!!x y. r x y ==> P x y"
"!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"
shows "P x y"
-  -- {* Another induction rule for trancl, incorporating transitivity *}
+  -- \<open>Another induction rule for trancl, incorporating transitivity\<close>
by (iprover intro: major [THEN tranclp_induct] cases)

lemmas trancl_trans_induct = tranclp_trans_induct [to_set]
@@ -418,7 +418,7 @@
lemma trancl_unfold: "r^+ = r Un r^+ O r"
by (auto intro: trancl_into_trancl elim: tranclE)

-text {* Transitivity of @{term "r^+"} *}
+text \<open>Transitivity of @{term "r^+"}\<close>
lemma trans_trancl [simp]: "trans (r^+)"
proof (rule transI)
fix x y z
@@ -427,11 +427,11 @@
then show "(x, z) \<in> r^+"
proof induct
case (base u)
-    from (x, y) \<in> r^+ and (y, u) \<in> r
+    from \<open>(x, y) \<in> r^+\<close> and \<open>(y, u) \<in> r\<close>
show "(x, u) \<in> r^+" ..
next
case (step u v)
-    from (x, u) \<in> r^+ and (u, v) \<in> r
+    from \<open>(x, u) \<in> r^+\<close> and \<open>(u, v) \<in> r\<close>
show "(x, v) \<in> r^+" ..
qed
qed
@@ -521,12 +521,12 @@
from this(2) show P
proof (cases rule: rtranclp.cases)
case rtrancl_refl
-    with r x y base show P by iprover
+    with \<open>r x y\<close> base show P by iprover
next
case rtrancl_into_rtrancl
from this have "tranclp r y z"
by (iprover intro: rtranclp_into_tranclp1)
-    with r x y step show P by iprover
+    with \<open>r x y\<close> step show P by iprover
qed
qed

@@ -596,7 +596,7 @@

lemma trancl_insert:
"(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
-  -- {* primitive recursion for @{text trancl} over finite relations *}
+  -- \<open>primitive recursion for @{text trancl} over finite relations\<close>
apply (rule equalityI)
apply (rule subsetI)
apply (simp only: split_tupled_all)
@@ -617,7 +617,7 @@
by(simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast

-text {* Simplifying nested closures *}
+text \<open>Simplifying nested closures\<close>

lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"
@@ -629,7 +629,7 @@
by auto

-text {* @{text Domain} and @{text Range} *}
+text \<open>@{text Domain} and @{text Range}\<close>

lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
by blast
@@ -673,8 +673,8 @@
done

-text {* More about converse @{text rtrancl} and @{text trancl}, should
-  be merged with main body. *}
+text \<open>More about converse @{text rtrancl} and @{text trancl}, should
+  be merged with main body.\<close>

lemma single_valued_confluent:
"\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>
@@ -720,9 +720,9 @@

declare trancl_into_rtrancl [elim]

-subsection {* The power operation on relations *}
+subsection \<open>The power operation on relations\<close>

-text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
+text \<open>@{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R}\<close>

relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
@@ -744,7 +744,7 @@
shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
by (induct n) (simp_all add: relcompp_relcomp_eq)

-text {* for code generation *}
+text \<open>for code generation\<close>

definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
relpow_code_def [code_abbrev]: "relpow = compow"
@@ -973,7 +973,7 @@
"(P^**) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y"
by (auto dest: rtranclp_imp_Sup_relpowp)

-text{* By Sternagel/Thiemann: *}
+text\<open>By Sternagel/Thiemann:\<close>
lemma relpow_fun_conv:
"((a,b) \<in> R ^^ n) = (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f(Suc i)) \<in> R))"
proof (induct n arbitrary: b)
@@ -1011,19 +1011,19 @@
proof(induct k arbitrary: b)
case 0
hence "R \<noteq> {}" by auto
-      with card_0_eq[OF finite R] have "card R >= Suc 0" by auto
+      with card_0_eq[OF \<open>finite R\<close>] have "card R >= Suc 0" by auto
thus ?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)]
+      from Suc(1)[OF \<open>(a,a') : R^^(Suc k)\<close>]
obtain n where "n \<le> card R" and "(a,a') \<in> R ^^ n" by auto
-      have "(a,b) : R^^(Suc n)" using (a,a') \<in> R^^n and (a',b)\<in> R by auto
+      have "(a,b) : R^^(Suc n)" using \<open>(a,a') \<in> R^^n\<close> and \<open>(a',b)\<in> R\<close> by auto
{ assume "n < card R"
-        hence ?case using (a,b): R^^(Suc n) Suc_leI[OF n < card R] by blast
+        hence ?case using \<open>(a,b): R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast
} moreover
{ assume "n = card R"
-        from (a,b) \<in> R ^^ (Suc n)[unfolded relpow_fun_conv]
+        from \<open>(a,b) \<in> R ^^ (Suc n)\<close>[unfolded relpow_fun_conv]
obtain f where "f 0 = a" and "f(Suc n) = b"
and steps: "\<And>i. i <= n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto
let ?p = "%i. (f i, f(Suc i))"
@@ -1031,7 +1031,7 @@
have "?p  ?N <= R" using steps by auto
from card_mono[OF assms(1) this]
have "card(?p  ?N) <= card R" .
-        also have "\<dots> < card ?N" using n = card R by simp
+        also have "\<dots> < card ?N" using \<open>n = card R\<close> 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 \<noteq> j" and
pij: "?p i = ?p j" by(auto simp: inj_on_def)
@@ -1045,7 +1045,7 @@
let ?n = "Suc(n - (j - i))"
have abl: "(a,b) \<in> 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
+          show "?g ?n = b" using \<open>f(Suc n) = b\<close> j ij by auto
next
fix k assume "k < ?n"
show "(?g k, ?g (Suc k)) \<in> R"
@@ -1062,19 +1062,19 @@
thus ?thesis using ij pij steps[OF i] by simp
next
case False
-              with i \<le> k have "i < k" by auto
-              hence small: "k + (j - i) <= n" using k<?n by arith
-              show ?thesis using steps[OF small] i<k by auto
+              with \<open>i \<le> k\<close> have "i < k" by auto
+              hence small: "k + (j - i) <= n" using \<open>k<?n\<close> by arith
+              show ?thesis using steps[OF small] \<open>i<k\<close> by auto
qed
qed
-        qed (simp add: f 0 = a)
+        qed (simp add: \<open>f 0 = a\<close>)
moreover have "?n <= n" using i j ij by arith
-        ultimately have ?case using n = card R by blast
+        ultimately have ?case using \<open>n = card R\<close> by blast
}
-      ultimately show ?case using n \<le> card R by force
+      ultimately show ?case using \<open>n \<le> card R\<close> by force
qed
}
-  thus ?thesis using gr0_implies_Suc[OF k>0] by auto
+  thus ?thesis using gr0_implies_Suc[OF \<open>k>0\<close>] by auto
qed

lemma relpow_finite_bounded:
@@ -1121,7 +1121,7 @@
done

-subsection {* Bounded transitive closure *}
+subsection \<open>Bounded transitive closure\<close>

definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
where
@@ -1151,15 +1151,15 @@
have "(a, b) \<in> ntrancl n R O (Id \<union> R)"
proof (cases "i = 1")
case True
-      from this (a, b) \<in> R ^^ i show ?thesis
+      from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis
unfolding ntrancl_def by auto
next
case False
-      from this 0 < i obtain j where j: "i = Suc j" "0 < j"
+      from this \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
by (cases i) auto
-      from this (a, b) \<in> R ^^ i obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
+      from this \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
by auto
-      from c1 j i \<le> Suc (Suc n) have "(a, c) \<in> ntrancl n R"
+      from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R"
unfolding ntrancl_def by fastforce
from this c2 show ?thesis by fastforce
qed
@@ -1180,7 +1180,7 @@
by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def)

-subsection {* Acyclic relations *}
+subsection \<open>Acyclic relations\<close>

definition acyclic :: "('a * 'a) set => bool" where
"acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"
@@ -1235,9 +1235,9 @@
done

-subsection {* Setup of transitivity reasoner *}
+subsection \<open>Setup of transitivity reasoner\<close>

-ML {*
+ML \<open>

structure Trancl_Tac = Trancl_Tac
(
@@ -1284,30 +1284,30 @@
in dec t end
| decomp _ = NONE;
);
-*}
+\<close>

-setup {*
+setup \<open>
map_theory_simpset (fn ctxt => ctxt
-*}
+\<close>

-text {* Optional methods. *}
+text \<open>Optional methods.\<close>

method_setup trancl =
-  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}
-  {* simple transitivity reasoner *}
+  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close>
+  \<open>simple transitivity reasoner\<close>
method_setup rtrancl =
-  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}
-  {* simple transitivity reasoner *}
+  \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close>
+  \<open>simple transitivity reasoner\<close>
method_setup tranclp =
-  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}
-  {* simple transitivity reasoner (predicate version) *}
+  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close>
+  \<open>simple transitivity reasoner (predicate version)\<close>
method_setup rtranclp =
-  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}
-  {* simple transitivity reasoner (predicate version) *}
+  \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close>
+  \<open>simple transitivity reasoner (predicate version)\<close>

end