diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -6,13 +6,13 @@
     Author:     Andrei Popescu, TU Muenchen
 *)
 
-section {*Well-founded Recursion*}
+section \<open>Well-founded Recursion\<close>
 
 theory Wellfounded
 imports Transitive_Closure
 begin
 
-subsection {* Basic Definitions *}
+subsection \<open>Basic Definitions\<close>
 
 definition wf :: "('a * 'a) set => bool" where
   "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -29,8 +29,8 @@
 
 lemmas wfPUNIVI = wfUNIVI [to_pred]
 
-text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
-    well-founded over their intersection, then @{term "wf r"}*}
+text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
+    well-founded over their intersection, then @{term "wf r"}\<close>
 lemma wfI: 
  "[| r \<subseteq> A <*> B; 
      !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
@@ -75,9 +75,9 @@
 unfolding wf_def by (blast intro: less_induct)
 
 
-subsection {* Basic Results *}
+subsection \<open>Basic Results\<close>
 
-text {* Point-free characterization of well-foundedness *}
+text \<open>Point-free characterization of well-foundedness\<close>
 
 lemma wfE_pf:
   assumes wf: "wf R"
@@ -105,7 +105,7 @@
   with a show "P x" by blast
 qed
 
-text{*Minimal-element characterization of well-foundedness*}
+text\<open>Minimal-element characterization of well-foundedness\<close>
 
 lemma wfE_min:
   assumes wf: "wf R" and Q: "x \<in> Q"
@@ -131,7 +131,7 @@
 
 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
 
-text{* Well-foundedness of transitive closure *}
+text\<open>Well-foundedness of transitive closure\<close>
 
 lemma wf_trancl:
   assumes "wf r"
@@ -143,17 +143,17 @@
     have "P x"
     proof (rule induct_step)
       fix y assume "(y, x) : r^+"
-      with `wf r` show "P y"
+      with \<open>wf r\<close> show "P y"
       proof (induct x arbitrary: y)
         case (less x)
-        note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
-        from `(y, x) : r^+` show "P y"
+        note hyp = \<open>\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'\<close>
+        from \<open>(y, x) : r^+\<close> show "P y"
         proof cases
           case base
           show "P y"
           proof (rule induct_step)
             fix y' assume "(y', y) : r^+"
-            with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
+            with \<open>(y, x) : r\<close> show "P y'" by (rule hyp [of y y'])
           qed
         next
           case step
@@ -172,7 +172,7 @@
   apply (erule wf_trancl)
   done
 
-text {* Well-foundedness of subsets *}
+text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   apply (simp (no_asm_use) add: wf_eq_minimal)
@@ -181,7 +181,7 @@
 
 lemmas wfP_subset = wf_subset [to_pred]
 
-text {* Well-foundedness of the empty relation *}
+text \<open>Well-foundedness of the empty relation\<close>
 
 lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
@@ -203,7 +203,7 @@
   apply (rule Int_lower2)
   done  
 
-text {* Exponentiation *}
+text \<open>Exponentiation\<close>
 
 lemma wf_exp:
   assumes "wf (R ^^ n)"
@@ -211,11 +211,11 @@
 proof (rule wfI_pf)
   fix A assume "A \<subseteq> R `` A"
   then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
-  with `wf (R ^^ n)`
+  with \<open>wf (R ^^ n)\<close>
   show "A = {}" by (rule wfE_pf)
 qed
 
-text {* Well-foundedness of insert *}
+text \<open>Well-foundedness of insert\<close>
 
 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
 apply (rule iffI)
@@ -233,12 +233,12 @@
 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
  apply assumption
 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) 
-  --{*essential for speed*}
-txt{*Blast with new substOccur fails*}
+  --\<open>essential for speed\<close>
+txt\<open>Blast with new substOccur fails\<close>
 apply (fast intro: converse_rtrancl_into_rtrancl)
 done
 
-text{*Well-foundedness of image*}
+text\<open>Well-foundedness of image\<close>
 
 lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)"
 apply (simp only: wf_eq_minimal, clarify)
@@ -248,7 +248,7 @@
 done
 
 
-subsection {* Well-Foundedness Results for Unions *}
+subsection \<open>Well-Foundedness Results for Unions\<close>
 
 lemma wf_union_compatible:
   assumes "wf R" "wf S"
@@ -259,8 +259,8 @@
   let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   assume "x \<in> Q"
   obtain a where "a \<in> ?Q'"
-    by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
-  with `wf S`
+    by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
+  with \<open>wf S\<close>
   obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
   { 
     fix y assume "(y, z) \<in> S"
@@ -269,19 +269,19 @@
     have "y \<notin> Q"
     proof 
       assume "y \<in> Q"
-      with `y \<notin> ?Q'` 
+      with \<open>y \<notin> ?Q'\<close> 
       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
-      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
-      with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
-      with `z \<in> ?Q'` have "w \<notin> Q" by blast 
-      with `w \<in> Q` show False by contradiction
+      from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
+      with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
+      with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast 
+      with \<open>w \<in> Q\<close> show False by contradiction
     qed
   }
-  with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
+  with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
 qed
 
 
-text {* Well-foundedness of indexed union with disjoint domains and ranges *}
+text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close>
 
 lemma wf_UN: "[| ALL i:I. wf(r i);  
          ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
@@ -340,7 +340,7 @@
     fix Q :: "'a set" and x 
     assume "x \<in> Q"
 
-    with `wf ?B`
+    with \<open>wf ?B\<close>
     obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
       by (erule wfE_min)
     then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
@@ -351,7 +351,7 @@
     show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
     proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
       case True
-      with `z \<in> Q` A3 show ?thesis by blast
+      with \<open>z \<in> Q\<close> A3 show ?thesis by blast
     next
       case False 
       then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
@@ -362,24 +362,24 @@
         then show "y \<notin> Q"
         proof
           assume "(y, z') \<in> R" 
-          then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
+          then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> ..
           with A1 show "y \<notin> Q" .
         next
           assume "(y, z') \<in> S" 
-          then have "(y, z) \<in> S O R" using  `(z', z) \<in> R` ..
+          then have "(y, z) \<in> S O R" using  \<open>(z', z) \<in> R\<close> ..
           with A2 show "y \<notin> Q" .
         qed
       qed
-      with `z' \<in> Q` show ?thesis ..
+      with \<open>z' \<in> Q\<close> show ?thesis ..
     qed
   qed
 qed
 
-lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
+lemma wf_comp_self: "wf R = wf (R O R)"  -- \<open>special case\<close>
   by (rule wf_union_merge [where S = "{}", simplified])
 
 
-subsection {* Well-Foundedness of Composition *}
+subsection \<open>Well-Foundedness of Composition\<close>
 
 text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
 
@@ -437,7 +437,7 @@
 qed
 
 
-subsection {* Acyclic relations *}
+subsection \<open>Acyclic relations\<close>
 
 lemma wf_acyclic: "wf r ==> acyclic r"
 apply (simp add: acyclic_def)
@@ -446,7 +446,7 @@
 
 lemmas wfP_acyclicP = wf_acyclic [to_pred]
 
-text{* Wellfoundedness of finite acyclic relations*}
+text\<open>Wellfoundedness of finite acyclic relations\<close>
 
 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
 apply (erule finite_induct, blast)
@@ -463,7 +463,7 @@
 by (blast intro: finite_acyclic_wf wf_acyclic)
 
 
-subsection {* @{typ nat} is well-founded *}
+subsection \<open>@{typ nat} is well-founded\<close>
 
 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
 proof (rule ext, rule ext, rule iffI)
@@ -517,12 +517,12 @@
   by (rule Wellfounded.wellorder_class.wf)
 
 
-subsection {* Accessible Part *}
+subsection \<open>Accessible Part\<close>
 
-text {*
+text \<open>
  Inductive definition of the accessible part @{term "acc r"} of a
  relation; see also @{cite "paulin-tlca"}.
-*}
+\<close>
 
 inductive_set
   acc :: "('a * 'a) set => 'a set"
@@ -545,7 +545,7 @@
   by (simp add: acc_def)
 
 
-text {* Induction rules *}
+text \<open>Induction rules\<close>
 
 theorem accp_induct:
   assumes major: "accp r a"
@@ -613,7 +613,7 @@
   done
 
 
-text {* Smaller relations have bigger accessible parts: *}
+text \<open>Smaller relations have bigger accessible parts:\<close>
 
 lemma accp_subset:
   assumes sub: "R1 \<le> R2"
@@ -630,8 +630,8 @@
 qed
 
 
-text {* This is a generalized induction theorem that works on
-  subsets of the accessible part. *}
+text \<open>This is a generalized induction theorem that works on
+  subsets of the accessible part.\<close>
 
 lemma accp_subset_induct:
   assumes subset: "D \<le> accp R"
@@ -640,9 +640,9 @@
     and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   shows "P x"
 proof -
-  from subset and `D x`
+  from subset and \<open>D x\<close>
   have "accp R x" ..
-  then show "P x" using `D x`
+  then show "P x" using \<open>D x\<close>
   proof (induct x)
     fix x
     assume "D x"
@@ -652,7 +652,7 @@
 qed
 
 
-text {* Set versions of the above theorems *}
+text \<open>Set versions of the above theorems\<close>
 
 lemmas acc_induct = accp_induct [to_set]
 
@@ -677,9 +677,9 @@
 lemmas acc_subset_induct = accp_subset_induct [to_set]
 
 
-subsection {* Tools for building wellfounded relations *}
+subsection \<open>Tools for building wellfounded relations\<close>
 
-text {* Inverse Image *}
+text \<open>Inverse Image\<close>
 
 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
@@ -691,7 +691,7 @@
 apply blast
 done
 
-text {* Measure functions into @{typ nat} *}
+text \<open>Measure functions into @{typ nat}\<close>
 
 definition measure :: "('a => nat) => ('a * 'a)set"
 where "measure = inv_image less_than"
@@ -713,7 +713,7 @@
 done
 
 
-text{* Lexicographic combinations *}
+text\<open>Lexicographic combinations\<close>
 
 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
   "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
@@ -731,13 +731,13 @@
   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   by (auto simp:lex_prod_def)
 
-text{* @{term "op <*lex*>"} preserves transitivity *}
+text\<open>@{term "op <*lex*>"} preserves transitivity\<close>
 
 lemma trans_lex_prod [intro!]: 
     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
 by (unfold trans_def lex_prod_def, blast) 
 
-text {* lexicographic combinations with measure functions *}
+text \<open>lexicographic combinations with measure functions\<close>
 
 definition 
   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
@@ -754,7 +754,7 @@
 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
 unfolding mlex_prod_def by auto
 
-text {* proper subset relation on finite sets *}
+text \<open>proper subset relation on finite sets\<close>
 
 definition finite_psubset  :: "('a set * 'a set) set"
 where "finite_psubset = {(A,B). A < B & finite B}"
@@ -772,7 +772,7 @@
 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
 unfolding finite_psubset_def by auto
 
-text {* max- and min-extension of order to finite sets *}
+text \<open>max- and min-extension of order to finite sets\<close>
 
 inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
 for R :: "('a \<times> 'a) set"
@@ -828,9 +828,9 @@
           next
             assume "M \<noteq> {}"
             from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 
-              by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto
+              by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
 
-            with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
+            with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
           qed
           with finites have "?N1 \<union> ?N2 \<in> ?W" 
             by (rule add_less) simp
@@ -869,22 +869,22 @@
     with nonempty
     obtain e x where "x \<in> Q" "e \<in> x" by force
     then have eU: "e \<in> \<Union>Q" by auto
-    with `wf r` 
+    with \<open>wf r\<close> 
     obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 
       by (erule wfE_min)
     from z obtain m where "m \<in> Q" "z \<in> m" by auto
-    from `m \<in> Q`
+    from \<open>m \<in> Q\<close>
     show ?thesis
     proof (rule, intro bexI allI impI)
       fix n
       assume smaller: "(n, m) \<in> min_ext r"
-      with `z \<in> m` obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
+      with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
       then show "n \<notin> Q" using z(2) by auto
     qed      
   qed
 qed
 
-text{* Bounded increase must terminate: *}
+text\<open>Bounded increase must terminate:\<close>
 
 lemma wf_bounded_measure:
 fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"