Merge remote-tracking branch 'origin/develop' into thibault-wip

Manual/LaTeX/commands.tex

@@ -34,6 +34,8 @@
 \newcommand{\fholquote}[1]{\fldq#1\frdq}
 \newcommand{\ldquo}{\mbox{\textrm{``}}}
 \newcommand{\rdquo}{\mbox{\textrm{''}}}
+\newcommand{\lsquo}{\mbox{\textrm{`}}}
+\newcommand{\rsquo}{\mbox{\textrm{'}}}
 
 %These macros were included by slind:
 

Manual/Tools/expected1

@@ -112,3 +112,6 @@ AND_CLAUSES
   \(\!\!\!{\turn}\!\!\!\!\) \(\forall\)t.
          (T \(\land\) t \({\iff}\) t) \(\land\) (t \(\land\) T \({\iff}\) t) \(\land\) (F \(\land\) t \({\iff}\) F) \(\land\)
          (t \(\land\) F \({\iff}\) F) \(\land\) (t \(\land\) t \({\iff}\) t)
+
+<<HOL message: Initialising SRW simpset ... done>>
+val foo = \(\!\!\!{\turn}\!\!\!\!\) x < x + 1: thm

Manual/Tools/polyscripter.sml

@@ -406,8 +406,8 @@ in
     end
   else if String.isPrefix ">>-" line then
     let
-      val firstline = String.extract(line, 3, NONE)
-      val (input, blankstr) = getRest 3 [firstline]
+      val (firstline,d) = poss_space_extract 3 line
+      val (input, blankstr) = getRest d [firstline]
       val raw_output = compile (lnumdie (linenum lbuf)) (String.concat input)
     in
       ("", transformOutput umap ws raw_output ^ blankstr)

Manual/Tools/testinput1

@@ -71,3 +71,8 @@ bar
 ##thm AND_CLAUSES
 
 ##thm50 AND_CLAUSES
+
+>>- Theorem foo:
+      x < x + 1n
+    Proof simp[]
+    QED

examples/AKS/compute/computeParamScript.sml

@@ -267,8 +267,7 @@ open triangleTheory; (* for list_lcm_pos *)
 
    AKS parameter search simplified:
    param_seek_def      |- !n m k c. param_seek m c n k =
-                                      if k = 0 then bad
-                                      else if c <= k then bad
+                                      if c <= k then bad
                                       else if n MOD k = 0 then nice k
                                       else if m <= ordz k n then good k
                                       else param_seek m c n (k + 1)
@@ -330,7 +329,7 @@ open triangleTheory; (* for list_lcm_pos *)
    Of course, being the smallest value, k must be prime.
 *)
 
-        (* Still More Theory:
+(* Still More Theory:
    When found, k divides (n ** j - 1)  with j > m.
    Say k = 13, the smallest value not a factor of P = PROD (0 < j <= m) (n ** j - 1)
    Since k is the smallest, this must be due to:
@@ -2488,6 +2487,7 @@ val aks_param_def = Define `
    (3) Skip m <= k, which is an optimisation by ZN_order_le: ordz k n <= k when 0 < k.
 *)
 (* Define the parameter seek loop *)
+(*
 val param_seek_def = tDefine "param_seek" `
   param_seek m c n k =
        if k = 0 then bad
@@ -2496,6 +2496,15 @@ val param_seek_def = tDefine "param_seek" `
   else if m <= ordz k n then good k
   else param_seek m c n (k + 1)
 `(WF_REL_TAC `measure (\(m,c,n,k). c - k)`);
+*)
+(* Skip k = 0 check, as caller uses k = 2 *)
+val param_seek_def = tDefine "param_seek" `
+  param_seek m c n k =
+       if c <= k then bad
+  else if n MOD k = 0 then nice k (* same as k divides n when k <> 0 *)
+  else if m <= ordz k n then good k
+  else param_seek m c n (k + 1)
+`(WF_REL_TAC `measure (\(m,c,n,k). c - k)`);
 
 (* Define the caller to parameter seek loop *)
 val param_def = Define`

examples/AKS/compute/computeRingScript.sml

@@ -109,7 +109,7 @@ open rich_listTheory; (* for FRONT and LAST *)
    ZN_poly_add_zero_zero   |- !n. [] +z [] = []
    ZN_poly_add_alt         |- !n p q. zweak p /\ zweak q /\ (LENGTH p = LENGTH q) ==> (p +z q = p zwadd q)
    ZN_poly_add_length      |- !n p q. (LENGTH p = LENGTH q) ==> (LENGTH (p +z q) = LENGTH q)
-   ZN_poly_cmult_alt       |- !n p c. zweak p /\ c < n ==> (c oz p = c zcmult p)
+   ZN_poly_cmult_alt       |- !n p c. zweak p ==> (c oz p = c zcmult p)
    ZN_poly_cmult_length    |- !n p c. LENGTH (c oz p) = LENGTH p
    ZN_slide_alt            |- !n q p1 p2. 0 < n /\ zweak p1 /\ zweak p2 /\ zweak q /\ (LENGTH p1 = LENGTH p2) ==>
                                           (ZN_slide n p1 p2 q = poly_slide (ZN n) p1 p2 q)
@@ -317,18 +317,16 @@ val ZN_poly_add_length = store_thm(
 
 (* Theorem: zweak p /\ c < n ==> (c oz p = c zcmult p) *)
 (* Proof:
-   Note c < n ==> c IN (ZN n).carrier        by ZN_property
    By ZN_poly_cmult_def, weak_cmult_map, this is to show:
-      zweak p /\ c < m ==> MAP (\x. (c * x) MOD n) p = MAP (\x. (ZN n).prod.op c x) p
+      zweak p ==> MAP (\x. (c * x) MOD n) p = MAP (\x. (ZN n).prod.op c x) p
    Note MEM x p ==> x IN (ZN n).carrier      by weak_every_mem
     ==> (ZN n).prod.op c x = (c * x) MOD n   by ZN_property
    Thus the maps are equal                   by MAP_CONG
 *)
 val ZN_poly_cmult_alt = store_thm(
   "ZN_poly_cmult_alt",
-  ``!(n:num) p c. zweak p /\ c < n ==> (c oz p = c zcmult p)``,
+  ``!(n:num) p c. zweak p ==> (c oz p = c zcmult p)``,
   rpt strip_tac >>
-  `c IN (ZN n).carrier` by rw[ZN_property] >>
   rw[ZN_poly_cmult_def, weak_cmult_map] >>
   (irule MAP_CONG >> simp[]) >>
   metis_tac[weak_every_mem, ZN_property]);
@@ -359,8 +357,7 @@ val ZN_poly_cmult_length = store_thm(
         and LENGTH (h oz p2) = LENGTH p2          by ZN_poly_cmult_length
         and LENGTH (h oz p2 +z p1) = LENGTH p1    by ZN_poly_add_length
         and LENGTH (turn p2) = LENGTH p2          by turn_length
-       Note h < n                                 by ZN_property, h IN (ZN n).carrier
-        Now h oz p2 = h zcmult p2                 by ZN_poly_cmult_alt, h < n
+       Note h oz p2 = h zcmult p2                 by ZN_poly_cmult_alt
         ==> zweak (h oz p2)                       by weak_cmult_weak, Ring (ZN n)
        Also h oz p2 +z p1 = (h zcmult p2) zwadd p1   by ZN_poly_add_alt, [1]
         ==> zweak (h oz p2 +z p1)                 by weak_add_weak
@@ -384,7 +381,7 @@ val ZN_slide_alt = store_thm(
   `LENGTH (h oz p2 +z p1) = LENGTH p1` by rw_tac std_ss[ZN_poly_add_length] >>
   `LENGTH (turn p2) = LENGTH p2` by rw_tac std_ss[turn_length] >>
   `Ring (ZN n)` by rw_tac std_ss[ZN_ring] >>
-  `h oz p2 = h zcmult p2` by rw_tac std_ss[ZN_poly_cmult_alt, GSYM ZN_property] >>
+  `h oz p2 = h zcmult p2` by rw_tac std_ss[ZN_poly_cmult_alt] >>
   `zweak (h oz p2)` by rw_tac std_ss[weak_cmult_weak] >>
   `h oz p2 +z p1 = (h zcmult p2) zwadd p1` by rw_tac std_ss[ZN_poly_add_alt] >>
   `zweak (h oz p2 +z p1)` by metis_tac[weak_add_weak] >>
@@ -606,7 +603,7 @@ val ZN_poly_exp_length = store_thm(
       = PAD_RIGHT 0 k
             (c MOD n::PAD_LEFT 0 (m MOD k) [1])  by ZN_poly_special_def
       = PAD_RIGHT (ZN n).sum.id k
-            ((ZN n).sum.exp 1 c::PAD_LEFT (ZN n).sum.id (m MOD k) [(ZN m).prod.id])  by above
+            ((ZN n).sum.exp 1 c::PAD_LEFT (ZN n).sum.id (m MOD k) [(ZN n).prod.id])  by above
       = unity_mod_special (ZN n) k m c           by unity_mod_special_def
 *)
 val ZN_poly_special_alt = store_thm(

examples/AKS/machine/countAKSScript.sml

@@ -179,6 +179,10 @@ val _ = monadsyntax.enable_monad "Count";
                          |- !n k c. 0 < n ==>
                                     stepsOf (poly_introM n k c) <=
                                     160 * MAX 1 k ** 2 * size k * size c * size n ** 4
+   poly_introM_steps_bound_alt
+                         |- !n k c. 1 < n /\ 1 < k ==>
+                                    stepsOf (poly_introM n k c) <=
+                                    160 * k ** 2 * size k * size c * size n ** 4
    poly_intro_rangeM_steps_thm
                          |- !n k c. stepsOf (poly_intro_rangeM n k c) =
                                     size c +
@@ -202,6 +206,10 @@ val _ = monadsyntax.enable_monad "Count";
                          |- !n k c. 0 < n ==>
                                     stepsOf (poly_intro_rangeM n k c) <=
                                     163 * MAX 1 c * MAX 1 k ** 2 * size k * size c * size n ** 4
+   poly_intro_rangeM_steps_bound_alt
+                         |- !n k c. 1 < n /\ 1 < k ==>
+                                    stepsOf (poly_intro_rangeM n k c) <=
+                                    163 * MAX 1 c * k ** 2 * size k * size c * size n ** 4
    poly_intro_rangeM_steps_bound_thm
                          |- !n k c. c <= k /\ k < n ==>
                                     stepsOf (poly_intro_rangeM n k c) <= 163 * MAX 1 k ** 3 * size n ** 6
@@ -232,9 +240,9 @@ val _ = monadsyntax.enable_monad "Count";
                             else 0
    aksM_steps_base   |- stepsOf (aksM 0) = 2 /\ stepsOf (aksM 1) = 12
    aksM_steps_upper  |- !n. stepsOf (aksM n) <=
-                                207 * size n ** 9 + 1418157969 * size n ** 20 +
+                                207 * size n ** 9 + 1348980357 * size n ** 20 +
                                 4075 * size n ** 21
-   aksM_steps_bound  |- !n. stepsOf (aksM n) <= 1418162251 * size n ** 21
+   aksM_steps_bound  |- !n. stepsOf (aksM n) <= 1348984639 * size n ** 21
    aksM_steps_O_poly |- stepsOf o aksM IN O_poly 21
    aksM_steps_big_O  |- stepsOf o aksM IN big_O (\n. ulog n ** 21)
    aksM_thm          |- !n. (valueOf (aksM n) <=> aks0 n) /\
@@ -774,7 +782,7 @@ val poly_introM_steps_thm = store_thm(
    <= 34 * MAX 1 k * size k * size c * size n ** 2 +              by poly_X_addM_steps_bound
       83 * MAX 1 k ** 2 * size n ** 2 * size n ** 2 +             by poly_expM_steps_bound
       34 * MAX 1 k * size k * size n * size c * size n ** 2 +     by poly_X_exp_addM_steps_bound
-      9 * MAX 1 k * size n                                        by poly_eqM_steps_bound, cases on n = 1
+      9 * MAX 1 k * size n                                        by poly_eqM_steps_thm, poly_eqM_steps_bound, cases on n = 1
    <= 9 * MAX 1 k * size n +
       34 * MAX 1 k * size k * size c * size n ** 2 +
       34 * MAX 1 k * size k * size c * size n ** 3 +
@@ -858,6 +866,17 @@ val poly_introM_steps_bound = store_thm(
   decide_tac) >>
   decide_tac);
 
+(* The following is just to match conditions in AKSclean.poly_introM_value_alt *)
+
+(* Theorem: 1 < n /\ 1 < k ==>
+           stepsOf (poly_introM n k c) <= 160 * k ** 2 * size k * size c * size n ** 4 *)
+(* Proof: poly_introM_steps_bound, MAX_1_POS *)
+val poly_introM_steps_bound_alt = store_thm(
+  "poly_introM_steps_bound_alt",
+  ``!n k c. 1 < n /\ 1 < k ==>
+           stepsOf (poly_introM n k c) <= 160 * k ** 2 * size k * size c * size n ** 4``,
+  metis_tac[poly_introM_steps_bound, MAX_1_POS, DECIDE``1 < n ==> 0 < n``]);
+
 (* Theorem: stepsOf (poly_intro_rangeM n k c) =
            size c +
            if c = 0 then 0
@@ -1008,6 +1027,19 @@ val poly_intro_rangeM_steps_bound = store_thm(
   decide_tac) >>
   decide_tac);
 
+(* The following is just to match conditions in AKSclean.poly_intro_rangeM_value_alt *)
+
+(* Theorem: 1 < n /\ 1 < k ==>
+           stepsOf (poly_intro_rangeM n k c) <=
+           163 * MAX 1 c * k ** 2 * size k * size c * size n ** 4 *)
+(* Proof: poly_intro_rangeM_steps_bound, MAX_1_POS *)
+val poly_intro_rangeM_steps_bound_alt = store_thm(
+  "poly_intro_rangeM_steps_bound_alt",
+  ``!n k c. 1 < n /\ 1 < k ==>
+           stepsOf (poly_intro_rangeM n k c) <=
+           163 * MAX 1 c * k ** 2 * size k * size c * size n ** 4``,
+  metis_tac[poly_intro_rangeM_steps_bound, MAX_1_POS, DECIDE``1 < n ==> 0 < n``]);
+
 (* Theorem: c <= k /\ k < n ==>
            stepsOf (poly_intro_rangeM n k c) <= 163 * MAX 1 k ** 3 * size n ** 6 *)
 (* Proof:
@@ -1178,7 +1210,7 @@ val aksM_steps_base = store_thm(
     and stepsOf (power_freeM n)
      <= 207 * size n ** 9                by power_freeM_steps_bound
     and stepsOf (paramM n)
-     <= 1418157969 * size n ** 20        by paramM_steps_bound
+     <= 1348980357 * size n ** 20        by paramM_steps_bound
 
    Note 1 < n                            by power_free_gt_1
    If ~power_free n, true                by first and second term.
@@ -1233,16 +1265,16 @@ val aksM_steps_base = store_thm(
 
    Overall,
       stepsOf (aksM n)
-   <= 207 * size n ** 9 + 1418157969 * size n ** 20 + 4075 * size n ** 21
+   <= 207 * size n ** 9 + 1348980357 * size n ** 20 + 4075 * size n ** 21
 *)
 val aksM_steps_upper = store_thm(
   "aksM_steps_upper",
   ``!n. stepsOf (aksM n) <=
-       207 * size n ** 9 + 1418157969 * size n ** 20 + 4075 * size n ** 21``,
+       207 * size n ** 9 + 1348980357 * size n ** 20 + 4075 * size n ** 21``,
   rpt strip_tac >>
   qabbrev_tac `c = 1 + HALF (ulog n ** 5)` >>
   `stepsOf (power_freeM n) <= 207 * size n ** 9` by rw[power_freeM_steps_bound] >>
-  `stepsOf (paramM n) <= 1418157969 * size n ** 20` by rw[paramM_steps_bound] >>
+  `stepsOf (paramM n) <= 1348980357 * size n ** 20` by rw[paramM_steps_bound] >>
   rw[aksM_steps_thm] >>
   `1 < n` by rw[power_free_gt_1] >>
   `c <= size n ** 5` by
@@ -1295,17 +1327,17 @@ val aksM_steps_upper = store_thm(
     decide_tac
   ]);
 
-(* Theorem: stepsOf (aksM n) <= 1418162251 * size n ** 21 *)
+(* Theorem: stepsOf (aksM n) <= 1348984639 * size n ** 21 *)
 (* Proof:
      stepsOf (aksM n)
-   <= 207 * size n ** 9 + 1418157969 * size n ** 20 + 4075 * size n ** 21
+   <= 207 * size n ** 9 + 1348980357 * size n ** 20 + 4075 * size n ** 21
                                                       by aksM_steps_upper
-   <= (207 + 1418157969 + 4075) * size n ** 21        by dominant term
-    = 1418162251 * size n ** 21
+   <= (207 + 1348980357 + 4075) * size n ** 21        by dominant term
+    = 1348984639 * size n ** 21
 *)
 val aksM_steps_bound = store_thm(
   "aksM_steps_bound",
-  ``!n. stepsOf (aksM n) <= 1418162251 * size n ** 21``,
+  ``!n. stepsOf (aksM n) <= 1348984639 * size n ** 21``,
   rpt strip_tac >>
   assume_tac aksM_steps_upper >>
   first_x_assum (qspec_then `n` strip_assume_tac) >>
@@ -1320,8 +1352,8 @@ val aksM_steps_bound = store_thm(
 (* Proof:
    By O_poly_thm, this is to show:
       ?h k. !n. h < n ==> stepsOf (aksM n) <= k * size n ** 21
-   Note stepsOf (aksM n) <= 1418162251 * size n ** 21  by aksM_steps_bound
-   Take any h, put k = 1418162251, the result follows.
+   Note stepsOf (aksM n) <= 1348984639 * size n ** 21  by aksM_steps_bound
+   Take any h, put k = 1348984639, the result follows.
 *)
 val aksM_steps_O_poly = store_thm(
   "aksM_steps_O_poly",
@@ -1332,8 +1364,8 @@ val aksM_steps_O_poly = store_thm(
 (* Proof:
    Note (stepsOf o aksM) IN O_poly 21     by aksM_steps_O_poly
     and O_poly 21
-      = big_O (POLY 21 o ulog)                 by O_poly_eq_O_poly_ulog
-      = (\n. ulog n ** 21)                     by POLY_def, FUN_EQ_THM
+      = big_O (POLY 21 o ulog)            by O_poly_eq_O_poly_ulog
+      = (\n. ulog n ** 21)                by POLY_def, FUN_EQ_THM
    The result follows.
 *)
 val aksM_steps_big_O = store_thm(

examples/AKS/machine/countMacroScript.sml

@@ -114,10 +114,8 @@ val _ = monadsyntax.enable_monad "Count";
    addM_def      |- !x y. addM x y = do tick (MAX (size x) (size y)); unit (x + y) od
    subM_def      |- !x y. subM x y = do tick (MAX (size x) (size y)); unit (x - y) od
    mulM_def      |- !x y. mulM x y = do tick (size x * size y); unit (x * y) od
-   divM_def      |- !x y. divM x y = if y = 0 then unit (x DIV 0)
-                                     else do tick (size x * size y); unit (x DIV y) od
-   modM_def      |- !x y. modM x y = if y = 0 then unit (x MOD 0)
-                                     else do tick (size x * size y); unit (x MOD y) od
+   divM_def      |- !x y. divM x y = do tick (size x * size y); unit (x DIV y) od
+   modM_def      |- !x y. modM x y = do tick (size x * size y); unit (x MOD y) od
 
 #  addM_value    |- !x y. valueOf (addM x y) = x + y
 #  subM_value    |- !x y. valueOf (subM x y) = x - y
@@ -127,9 +125,9 @@ val _ = monadsyntax.enable_monad "Count";
 
 #  addM_steps    |- !x y. stepsOf (addM x y) = MAX (size x) (size y)
 #  subM_steps    |- !x y. stepsOf (subM x y) = MAX (size x) (size y)
-#  mulM_steps    |- !x y. stepsOf (mulM x y) = size x * size y:
-#  divM_steps    |- !x y. stepsOf (divM x y) = if y = 0 then 0 else size x * size y
-#  modM_steps    |- !x y. stepsOf (modM x y) = if y = 0 then 0 else size x * size y
+#  mulM_steps    |- !x y. stepsOf (mulM x y) = size x * size y
+#  divM_steps    |- !x y. stepsOf (divM x y) = size x * size y
+#  modM_steps    |- !x y. stepsOf (modM x y) = size x * size y
 
    Basic List:
    nullM_def     |- !ls. nullM ls = do tick 1; unit (ls = []) od
@@ -392,15 +390,13 @@ val _ = overload_on ("mul_", ``app2 mulM``);
 
 (* DIV monad *)
 val divM_def = Define`
-  divM x y = if y = 0 then return (x DIV 0) else
-                do tick (size x * size y); return (x DIV y); od
+  divM x y = do tick (size x * size y); return (x DIV y); od
 `;
 val _ = overload_on ("div_", ``app2 divM``);
 
 (* MOD monad *)
 val modM_def = Define`
-  modM x y = if y = 0 then return (x MOD 0) else
-        do tick (size x * size y);  return (x MOD y); od
+  modM x y = do tick (size x * size y);  return (x MOD y); od
 `;
 val _ = overload_on ("mod_", ``app2 modM``);
 
@@ -420,10 +416,8 @@ val modM_value = store_thm("modM_value[simp]", ``!x y. valueOf (modM x y) = x MO
 val addM_steps = store_thm("addM_steps[simp]", ``!x y. stepsOf (addM x y) = MAX (size x) (size y)``, rw[addM_def]);
 val subM_steps = store_thm("subM_steps[simp]", ``!x y. stepsOf (subM x y) = MAX (size x) (size y)``, rw[subM_def]);
 val mulM_steps = store_thm("mulM_steps[simp]", ``!x y. stepsOf (mulM x y) = (size x) * (size y)``, rw[mulM_def]);
-val divM_steps = store_thm("divM_steps[simp]", ``!x y. stepsOf (divM x y) = if y = 0 then 0 else (size x) * (size y)``, rw[divM_def]);
-val modM_steps = store_thm("modM_steps[simp]", ``!x y. stepsOf (modM x y) = if y = 0 then 0 else (size x) * (size y)``, rw[modM_def]);
-
-(* Complexity Class of basic arithmetic *)
+val divM_steps = store_thm("divM_steps[simp]", ``!x y. stepsOf (divM x y) = (size x) * (size y)``, rw[divM_def]);
+val modM_steps = store_thm("modM_steps[simp]", ``!x y. stepsOf (modM x y) = (size x) * (size y)``, rw[modM_def]);
 
 (* ------------------------------------------------------------------------- *)
 (* Basic List                                                                *)