merged

--- a/src/HOL/Library/Polynomial.thy	Thu Apr 09 09:12:47 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Apr 09 15:54:09 2015 +0200
@@ -7,7 +7,7 @@
 section {* Polynomials as type over a ring structure *}
 
 theory Polynomial
-imports Main GCD "~~/src/HOL/Library/More_List"
+imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
 begin
 
 subsection {* Auxiliary: operations for lists (later) representing coefficients *}
@@ -50,48 +50,13 @@
   "tl (x ## xs) = xs"
   by (simp add: cCons_def)
 
-
-subsection {* Almost everywhere zero functions *}
-
-definition almost_everywhere_zero :: "(nat \<Rightarrow> 'a::zero) \<Rightarrow> bool"
-where
-  "almost_everywhere_zero f \<longleftrightarrow> (\<exists>n. \<forall>i>n. f i = 0)"
-
-lemma almost_everywhere_zeroI:
-  "(\<And>i. i > n \<Longrightarrow> f i = 0) \<Longrightarrow> almost_everywhere_zero f"
-  by (auto simp add: almost_everywhere_zero_def)
-
-lemma almost_everywhere_zeroE:
-  assumes "almost_everywhere_zero f"
-  obtains n where "\<And>i. i > n \<Longrightarrow> f i = 0"
-proof -
-  from assms have "\<exists>n. \<forall>i>n. f i = 0" by (simp add: almost_everywhere_zero_def)
-  then obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by blast
-  with that show thesis .
-qed
-
-lemma almost_everywhere_zero_case_nat:
-  assumes "almost_everywhere_zero f"
-  shows "almost_everywhere_zero (case_nat a f)"
-  using assms
-  by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
-    blast
-
-lemma almost_everywhere_zero_Suc:
-  assumes "almost_everywhere_zero f"
-  shows "almost_everywhere_zero (\<lambda>n. f (Suc n))"
-proof -
-  from assms obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by (erule almost_everywhere_zeroE)
-  then have "\<And>i. i > n \<Longrightarrow> f (Suc i) = 0" by auto
-  then show ?thesis by (rule almost_everywhere_zeroI)
-qed
-
+lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
+  by (auto simp: MOST_nat) (metis Suc_lessE)
 
 subsection {* Definition of type @{text poly} *}
 
-typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. almost_everywhere_zero f}"
-  morphisms coeff Abs_poly
-  unfolding almost_everywhere_zero_def by auto
+typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
+  morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
 
 setup_lifting type_definition_poly
 
@@ -101,8 +66,7 @@
 lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
   by (simp add: poly_eq_iff)
 
-lemma coeff_almost_everywhere_zero:
-  "almost_everywhere_zero (coeff p)"
+lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
   using coeff [of p] by simp
 
 
@@ -116,8 +80,8 @@
   assumes "degree p < n"
   shows "coeff p n = 0"
 proof -
-  from coeff_almost_everywhere_zero
-  have "\<exists>n. \<forall>i>n. coeff p i = 0" by (blast intro: almost_everywhere_zeroE)
+  have "\<exists>n. \<forall>i>n. coeff p i = 0"
+    using MOST_coeff_eq_0 by (simp add: MOST_nat)
   then have "\<forall>i>degree p. coeff p i = 0"
     unfolding degree_def by (rule LeastI_ex)
   with assms show ?thesis by simp
@@ -139,7 +103,7 @@
 begin
 
 lift_definition zero_poly :: "'a poly"
-  is "\<lambda>_. 0" by (rule almost_everywhere_zeroI) simp
+  is "\<lambda>_. 0" by (rule MOST_I) simp
 
 instance ..
 
@@ -184,7 +148,7 @@
 
 lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>a p. case_nat a (coeff p)"
-  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_case_nat)
+  by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
 
 lemmas coeff_pCons = pCons.rep_eq
 
@@ -247,7 +211,8 @@
 proof
   show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
     by transfer
-      (simp add: Abs_poly_inverse almost_everywhere_zero_Suc fun_eq_iff split: nat.split)
+       (simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
+                 split: nat.split)
 qed
 
 lemma pCons_induct [case_names 0 pCons, induct type: poly]:
@@ -483,7 +448,7 @@
 
 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly"
   is "\<lambda>a m n. if m = n then a else 0"
-  by (auto intro!: almost_everywhere_zeroI)
+  by (simp add: MOST_iff_cofinite)
 
 lemma coeff_monom [simp]:
   "coeff (monom a m) n = (if m = n then a else 0)"
@@ -536,11 +501,9 @@
 
 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n + coeff q n"
-proof (rule almost_everywhere_zeroI) 
-  fix q p :: "'a poly" and i
-  assume "max (degree q) (degree p) < i"
-  then show "coeff p i + coeff q i = 0"
-    by (simp add: coeff_eq_0)
+proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n + coeff q n = 0"
+    by simp
 qed
 
 lemma coeff_add [simp]:
@@ -564,11 +527,9 @@
 
 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n - coeff q n"
-proof (rule almost_everywhere_zeroI) 
-  fix q p :: "'a poly" and i
-  assume "max (degree q) (degree p) < i"
-  then show "coeff p i - coeff q i = 0"
-    by (simp add: coeff_eq_0)
+proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n - coeff q n = 0"
+    by simp
 qed
 
 lemma coeff_diff [simp]:
@@ -590,11 +551,9 @@
 
 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p n. - coeff p n"
-proof (rule almost_everywhere_zeroI)
-  fix p :: "'a poly" and i
-  assume "degree p < i"
-  then show "- coeff p i = 0"
-    by (simp add: coeff_eq_0)
+proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
+  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
+    by simp
 qed
 
 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
@@ -748,7 +707,7 @@
 
 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>a p n. a * coeff p n"
-proof (rule almost_everywhere_zeroI)
+proof (intro MOST_nat[THEN iffD2] exI allI impI) 
   fix a :: 'a and p :: "'a poly" and i
   assume "degree p < i"
   then show "a * coeff p i = 0"

--- a/src/Pure/Isar/method.ML	Thu Apr 09 09:12:47 2015 +0200
+++ b/src/Pure/Isar/method.ML	Thu Apr 09 15:54:09 2015 +0200
@@ -70,15 +70,16 @@
   val evaluate: text -> Proof.context -> method
   type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
   val modifier: attribute -> Position.T -> modifier
-  val section: modifier parser list -> declaration context_parser
-  val sections: modifier parser list -> declaration list context_parser
+  val old_section_parser: bool Config.T
+  val sections: modifier parser list -> unit context_parser
   type text_range = text * Position.range
   val text: text_range option -> text option
   val position: text_range option -> Position.T
   val reports_of: text_range -> Position.report list
   val report: text_range -> unit
+  val parser': Proof.context -> int -> text_range parser
+  val parser: int -> text_range parser
   val parse: text_range parser
-  val parse_internal: Proof.context -> text_range parser
 end;
 
 structure Method: METHOD =
@@ -487,6 +488,26 @@
 
 (* sections *)
 
+val old_section_parser =
+  Config.bool (Config.declare ("Method.old_section_parser", @{here}) (K (Config.Bool false)));
+
+local
+
+fun thms ss =
+  Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
+
+fun app {init, attribute, pos = _} ths context =
+  fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context);
+
+fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
+  (fn (m, ths) => Scan.succeed (swap (app m ths context))));
+
+in
+
+fun old_sections ss = Scan.repeat (section ss) >> K ();
+
+end;
+
 local
 
 fun sect (modifier : modifier parser) = Scan.depend (fn context =>
@@ -522,8 +543,10 @@
 
 in
 
-val section = sect o Scan.first;
-val sections = Scan.repeat o section;
+fun sections ss =
+  Args.context :|-- (fn ctxt =>
+    if Config.get ctxt old_section_parser then old_sections ss
+    else Scan.repeat (sect (Scan.first ss)) >> K ());
 
 end;
 
@@ -574,7 +597,7 @@
 fun is_symid_meth s =
   s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
 
-fun parser check_ctxt low_pri =
+fun gen_parser check_ctxt pri =
   let
     val (meth_name, mk_src) =
       (case check_ctxt of
@@ -610,15 +633,17 @@
     and meth0 x =
       (Parse.enum1_positions "|" meth1
         >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
-  in
-    Scan.trace (if low_pri then meth0 else meth4)
-      >> (fn (m, toks) => (m, Token.range_of toks))
-  end;
+
+    val meth =
+      nth [meth0, meth1, meth2, meth3, meth4, meth5] pri
+        handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri);
+  in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end;
 
 in
 
-val parse = parser NONE false;
-fun parse_internal ctxt = parser (SOME ctxt) true;
+val parser' = gen_parser o SOME;
+val parser = gen_parser NONE;
+val parse = parser 4;
 
 end;
 
@@ -672,4 +697,3 @@
 val SIMPLE_METHOD = Method.SIMPLE_METHOD;
 val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
 val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
-