src/HOL/Filter.thy
changeset 60758 d8d85a8172b5
parent 60752 b48830b670a1
child 60974 6a6f15d8fbc4
     1.1 --- a/src/HOL/Filter.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,17 +3,17 @@
     1.4      Author:     Johannes Hölzl
     1.5  *)
     1.6  
     1.7 -section {* Filters on predicates *}
     1.8 +section \<open>Filters on predicates\<close>
     1.9  
    1.10  theory Filter
    1.11  imports Set_Interval Lifting_Set
    1.12  begin
    1.13  
    1.14 -subsection {* Filters *}
    1.15 +subsection \<open>Filters\<close>
    1.16  
    1.17 -text {*
    1.18 +text \<open>
    1.19    This definition also allows non-proper filters.
    1.20 -*}
    1.21 +\<close>
    1.22  
    1.23  locale is_filter =
    1.24    fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.25 @@ -34,7 +34,7 @@
    1.26    using assms by (simp add: Abs_filter_inverse)
    1.27  
    1.28  
    1.29 -subsubsection {* Eventually *}
    1.30 +subsubsection \<open>Eventually\<close>
    1.31  
    1.32  definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.33    where "eventually P F \<longleftrightarrow> Rep_filter F P"
    1.34 @@ -237,7 +237,7 @@
    1.35    frequently_all
    1.36    frequently_imp_iff
    1.37  
    1.38 -ML {*
    1.39 +ML \<open>
    1.40    fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
    1.41      let
    1.42        val mp_thms = facts RL @{thms eventually_rev_mp}
    1.43 @@ -252,16 +252,16 @@
    1.44      in
    1.45        CASES cases (resolve_tac ctxt [raw_elim_thm] i)
    1.46      end)
    1.47 -*}
    1.48 +\<close>
    1.49  
    1.50 -method_setup eventually_elim = {*
    1.51 +method_setup eventually_elim = \<open>
    1.52    Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
    1.53 -*} "elimination of eventually quantifiers"
    1.54 +\<close> "elimination of eventually quantifiers"
    1.55  
    1.56 -subsubsection {* Finer-than relation *}
    1.57 +subsubsection \<open>Finer-than relation\<close>
    1.58  
    1.59 -text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
    1.60 -filter @{term F'}. *}
    1.61 +text \<open>@{term "F \<le> F'"} means that filter @{term F} is finer than
    1.62 +filter @{term F'}.\<close>
    1.63  
    1.64  instantiation filter :: (type) complete_lattice
    1.65  begin
    1.66 @@ -457,12 +457,12 @@
    1.67    then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
    1.68    proof induct
    1.69      case empty then show ?case
    1.70 -      using `B \<noteq> {}` by auto
    1.71 +      using \<open>B \<noteq> {}\<close> by auto
    1.72    next
    1.73      case (insert x X)
    1.74      then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
    1.75        by auto
    1.76 -    with `insert x X \<subseteq> B` base[of b x] show ?case
    1.77 +    with \<open>insert x X \<subseteq> B\<close> base[of b x] show ?case
    1.78        by (auto intro: order_trans)
    1.79    qed
    1.80    then obtain b where "b \<in> B" "b \<le> Inf X"
    1.81 @@ -477,7 +477,7 @@
    1.82    unfolding INF_def by (subst eventually_Inf_base) auto
    1.83  
    1.84  
    1.85 -subsubsection {* Map function for filters *}
    1.86 +subsubsection \<open>Map function for filters\<close>
    1.87  
    1.88  definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
    1.89    where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
    1.90 @@ -526,7 +526,7 @@
    1.91      unfolding le_filter_def eventually_filtermap
    1.92      by (subst (1 2) eventually_INF) auto
    1.93  qed
    1.94 -subsubsection {* Standard filters *}
    1.95 +subsubsection \<open>Standard filters\<close>
    1.96  
    1.97  definition principal :: "'a set \<Rightarrow> 'a filter" where
    1.98    "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
    1.99 @@ -576,7 +576,7 @@
   1.100  lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   1.101    unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
   1.102  
   1.103 -subsubsection {* Order filters *}
   1.104 +subsubsection \<open>Order filters\<close>
   1.105  
   1.106  definition at_top :: "('a::order) filter"
   1.107    where "at_top = (INF k. principal {k ..})"
   1.108 @@ -648,7 +648,7 @@
   1.109    unfolding trivial_limit_def
   1.110    by (metis eventually_at_top_linorder order_refl)
   1.111  
   1.112 -subsection {* Sequentially *}
   1.113 +subsection \<open>Sequentially\<close>
   1.114  
   1.115  abbreviation sequentially :: "nat filter"
   1.116    where "sequentially \<equiv> at_top"
   1.117 @@ -734,7 +734,7 @@
   1.118      by (blast intro: finite_subset)
   1.119  qed
   1.120  
   1.121 -subsection {* Limits *}
   1.122 +subsection \<open>Limits\<close>
   1.123  
   1.124  definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.125    "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
   1.126 @@ -828,7 +828,7 @@
   1.127    fix i j assume "i \<in> I" "j \<in> I"
   1.128    with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
   1.129      by auto
   1.130 -qed (auto simp: eventually_principal `I \<noteq> {}`)
   1.131 +qed (auto simp: eventually_principal \<open>I \<noteq> {}\<close>)
   1.132  
   1.133  lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   1.134    unfolding filterlim_def filtermap_filtermap ..
   1.135 @@ -850,7 +850,7 @@
   1.136      LIM x F. if P x then f x else g x :> G"
   1.137    unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
   1.138  
   1.139 -subsection {* Limits to @{const at_top} and @{const at_bot} *}
   1.140 +subsection \<open>Limits to @{const at_top} and @{const at_bot}\<close>
   1.141  
   1.142  lemma filterlim_at_top:
   1.143    fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.144 @@ -890,7 +890,7 @@
   1.145      have "eventually (\<lambda>x. g z \<le> x) at_top"
   1.146        by (rule eventually_ge_at_top)
   1.147      with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
   1.148 -      by eventually_elim (metis mono bij `P z`)
   1.149 +      by eventually_elim (metis mono bij \<open>P z\<close>)
   1.150    qed
   1.151  qed
   1.152  
   1.153 @@ -937,7 +937,7 @@
   1.154    by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   1.155  
   1.156  
   1.157 -subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
   1.158 +subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
   1.159  
   1.160  context begin interpretation lifting_syntax .
   1.161  
   1.162 @@ -1011,7 +1011,7 @@
   1.163      fix P' Q'
   1.164      assume "G P'" "G Q'"
   1.165      moreover
   1.166 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   1.167 +    from bi_total_fun[OF \<open>bi_unique A\<close> bi_total_eq, unfolded bi_total_def]
   1.168      obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   1.169      have "F P = G P'" "F Q = G Q'" by transfer_prover+
   1.170      ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
   1.171 @@ -1021,7 +1021,7 @@
   1.172      fix P' Q'
   1.173      assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
   1.174      moreover
   1.175 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   1.176 +    from bi_total_fun[OF \<open>bi_unique A\<close> bi_total_eq, unfolded bi_total_def]
   1.177      obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   1.178      have "F P = G P'" by transfer_prover
   1.179      moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
   1.180 @@ -1046,7 +1046,7 @@
   1.181    shows "left_total (rel_filter A)"
   1.182  proof(rule left_totalI)
   1.183    fix F :: "'a filter"
   1.184 -  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
   1.185 +  from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
   1.186    obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   1.187      unfolding  bi_total_def by blast
   1.188    moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover