summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Transitive_Closure_Table.thy

changeset 60500 | 903bb1495239 |

parent 58881 | b9556a055632 |

child 60519 | 84b8e5c2580e |

1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy Wed Jun 17 10:57:11 2015 +0200 1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Wed Jun 17 11:03:05 2015 +0200 1.3 @@ -1,6 +1,6 @@ 1.4 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) 1.5 1.6 -section {* A table-based implementation of the reflexive transitive closure *} 1.7 +section \<open>A table-based implementation of the reflexive transitive closure\<close> 1.8 1.9 theory Transitive_Closure_Table 1.10 imports Main 1.11 @@ -22,9 +22,9 @@ 1.12 then show ?case .. 1.13 next 1.14 case (step x z) 1.15 - from `\<exists>xs. rtrancl_path r z xs y` 1.16 + from \<open>\<exists>xs. rtrancl_path r z xs y\<close> 1.17 obtain xs where "rtrancl_path r z xs y" .. 1.18 - with `r x z` have "rtrancl_path r x (z # xs) y" 1.19 + with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y" 1.20 by (rule rtrancl_path.step) 1.21 then show ?case .. 1.22 qed 1.23 @@ -37,7 +37,7 @@ 1.24 show ?case by (rule rtranclp.rtrancl_refl) 1.25 next 1.26 case (step x y ys z) 1.27 - from `r x y` `r\<^sup>*\<^sup>* y z` show ?case 1.28 + from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case 1.29 by (rule converse_rtranclp_into_rtranclp) 1.30 qed 1.31 qed 1.32 @@ -53,7 +53,7 @@ 1.33 case (step x y xs) 1.34 then have "rtrancl_path r y (xs @ ys) z" 1.35 by simp 1.36 - with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z" 1.37 + with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z" 1.38 by (rule rtrancl_path.step) 1.39 then show ?case by simp 1.40 qed 1.41 @@ -83,7 +83,7 @@ 1.42 by (rule rtrancl_path.step) 1.43 then have "rtrancl_path r x ((a # as) @ [y]) y" 1.44 by simp 1.45 - then show ?thesis using `rtrancl_path r y ys z` 1.46 + then show ?thesis using \<open>rtrancl_path r y ys z\<close> 1.47 by (rule Cons(2)) 1.48 qed 1.49 qed 1.50 @@ -96,7 +96,7 @@ 1.51 show ?case 1.52 proof (cases "distinct (x # xs)") 1.53 case True 1.54 - with `rtrancl_path r x xs y` show ?thesis by (rule less) 1.55 + with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) 1.56 next 1.57 case False 1.58 then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" 1.59 @@ -108,7 +108,7 @@ 1.60 case Nil 1.61 with xxs have x: "x = a" and xs: "xs = bs @ a # cs" 1.62 by auto 1.63 - from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y" 1.64 + from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" 1.65 by (auto elim: rtrancl_path_appendE) 1.66 from xs have "length cs < length xs" by simp 1.67 then show ?thesis 1.68 @@ -117,7 +117,7 @@ 1.69 case (Cons d ds) 1.70 with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" 1.71 by auto 1.72 - with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a" 1.73 + with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a" 1.74 and ay: "rtrancl_path r a (bs @ a # cs) y" 1.75 by (auto elim: rtrancl_path_appendE) 1.76 from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) 1.77 @@ -152,7 +152,7 @@ 1.78 by auto 1.79 ultimately have "rtrancl_tab r (x # ys) y z" 1.80 by (rule step) 1.81 - with `x \<notin> set ys` `r x y` 1.82 + with \<open>x \<notin> set ys\<close> \<open>r x y\<close> 1.83 show ?case by (rule rtrancl_tab.step) 1.84 qed 1.85