Permalink
Browse files

Merge branch 'features/case-const-argflip'.

Closes #97 (github issue number).
  • Loading branch information...
2 parents 257d4ee + c47c568 commit f1e3c53ef712a2aeed7f23f056093b3b7b73c71c @mn200 mn200 committed Dec 11, 2012
Showing with 468 additions and 360 deletions.
  1. +1 −1 Manual/Description/definitions.tex
  2. +4 −4 Manual/Description/theories.tex
  3. +81 −0 doc/kananaskis-9.release.html
  4. +1 −3 examples/ARM/v7/arm_stepScript.sml
  5. +6 −5 examples/lambda/barendregt/normal_orderScript.sml
  6. +20 −20 examples/miller/formalize/extra_pred_setScript.sml
  7. +12 −8 examples/miller/formalize/extra_realScript.sml
  8. +4 −4 examples/miller/formalize/measureScript.sml
  9. +1 −1 examples/miller/formalize/sequenceScript.sml
  10. +8 −8 examples/unification/triangular/nominal/ntermScript.sml
  11. +11 −7 src/1/Pmatch.sml
  12. +2 −0 src/1/Prim_rec.sig
  13. +30 −19 src/1/Prim_rec.sml
  14. +8 −4 src/1/TypeBasePure.sml
  15. +4 −4 src/1/boolSyntax.sml
  16. +11 −30 src/1/selftest.sml
  17. +13 −0 src/1/testutils.sig
  18. +47 −0 src/1/testutils.sml
  19. +1 −2 src/HolSmt/SmtLib.sml
  20. +7 −7 src/HolSmt/selftest.sml
  21. +4 −9 src/basicProof/BasicProvers.sml
  22. +24 −70 src/bool/boolScript.sml
  23. +1 −1 src/compute/src/computeLib.sml
  24. +1 −1 src/datatype/Datatype.sml
  25. +6 −5 src/datatype/EnumType.sml
  26. +1 −8 src/datatype/inftree/inftreeScript.sml
  27. +1 −1 src/list/src/listScript.sml
  28. +8 −4 src/list/src/listSyntax.sml
  29. +7 −6 src/llist/llistScript.sml
  30. +12 −2 src/n-bit/fcpScript.sml
  31. +9 −2 src/num/termination/Holmakefile
  32. +10 −0 src/num/termination/selftest.sml
  33. +2 −6 src/num/theories/arithmeticScript.sml
  34. +0 −1 src/num/theories/basicSize.sml
  35. +5 −5 src/num/theories/numSyntax.sml
  36. +17 −6 src/num/theories/selftest.sml
  37. +5 −10 src/one/oneScript.sml
  38. +2 −2 src/one/oneSyntax.sml
  39. +19 −30 src/option/optionScript.sml
  40. +3 −3 src/option/optionSyntax.sml
  41. +14 −10 src/pair/src/pairScript.sml
  42. +12 −20 src/pred_set/src/selftest.sml
  43. +10 −10 src/probability/measureScript.sml
  44. +4 −6 src/probability/util_probScript.sml
  45. +3 −1 src/proofman/Holmakefile
  46. +7 −4 src/string/stringSyntax.sml
  47. +2 −6 src/sum/sumScript.sml
  48. +5 −2 src/sum/sumSyntax.sml
  49. +2 −2 src/tfl/src/Defn.sml
@@ -386,7 +386,7 @@ \subsection{Theorems arising from a datatype definition}
(!a. (M' = Leaf a) ==> (f a = f' a)) /\
(!a0 a1. (M' = Node a0 a1) ==> (f1 a0 a1 = f1' a0 a1))
==>
- (case f f1 M = case f' f1' M')
+ (tree_CASE M f f1 M = tree_CASE M' f' f1')
\end{verbatim}
\end{hol}
%
@@ -2632,13 +2632,13 @@ \subsection{Lists}\label{avra_list}
\end{hol}
%
Such an expression is translated to
-$\konst{list\_case}\ e_2\ (\lambda h\; t.\ e_3)\ e_1$ where the constant
-{\small\verb+list_case+} is defined as follows:
+$\holtxt{list\_CASE}\ e_1\ e_2\ (\lambda h\; t.\ e_3)$ where the constant
+\holtxt{list\_CASE} is defined as follows:
\begin{hol}
\begin{verbatim}
list_case_def
- |- (!v f. list_case v f [] = v) /\
- (!v f a0 a1. list_case v f (a0::a1) = f a0 a1)
+ |- (!v f. list_CASE [] v f = v) /\
+ (!v f a0 a1. list_CASE (a0::a1) v f = f a0 a1)
\end{verbatim}
\end{hol}
@@ -0,0 +1,81 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
+<html>
+<head>
+<meta http-equiv="content-type"
+ content="text/html ; charset=UTF-8">
+<title>Release Notes for Kananaskis-9 version of HOL 4</title>
+<style type="text/css">
+<!--
+ body {color: #333333; background: #FFFFFF;
+ margin-left: 1em; margin-right: 1em }
+ code, pre {color: #660066; font-weight: bold; font-family: "Andale Mono", "Lucida Console", monospace; }
+-->
+</style>
+
+</head>
+
+<body>
+<h1>Notes on HOL 4, Kananaskis-9 release</h1>
+
+<p>We are pleased to announce the Kananaskis-9 release of HOL 4.</p>
+
+<h2 id="contents">Contents</h2>
+<ul>
+ <li> <a href="#new-features">New features</a> </li>
+ <li> <a href="#bugs-fixed">Bugs fixed</a> </li>
+ <li> <a href="#new-theories">New theories</a> </li>
+ <li> <a href="#new-tools">New tools</a> </li>
+ <li> <a href="#new-examples">New examples</a> </li>
+ <li> <a href="#incompatibilities">Incompatibilities</a> </li>
+</ul>
+
+<h2 id="new-features">New features:</h2>
+
+<h2 id="bugs-fixed">Bugs fixed:</h2>
+
+
+<h2 id="new-theories">New theories:</h2>
+
+<h2 id="new-tools">New tools:</h2>
+
+<h2 id="new-examples">New examples:</h2>
+
+<h2 id="incompatibilities">Incompatibilities:</h2>
+
+<ul>
+
+<li><p>The case-constants generated for algebraic data types now have different types.
+The value that is “switched on” is now the first argument of the constant rather than the last.
+The names of these constants have also changed, emphasising the change.
+For example, the old constant for natural numbers, <code>num_case</code> had type
+<pre>
+ α → (num → α) → num → α
+</pre>
+<p> Now the case constant for the natural numbers is called <code>num_CASE</code> and has type
+<pre>
+ num → α → (num → α) → α
+</pre>
+
+<p>This change is invisible if the “<code>case</code>-<code>of</code>” syntax is used.
+
+<p>This change makes more efficient evaluation (with <code>EVAL</code>) of expressions with case constants possible.
+
+<p>In addition, the <code>bool_case</code> constant has been deleted entirely: when the arguments are flipped as above it becomes identical to <code>COND</code> (<code>if</code>-<code>then</code>-<code>else</code>).
+This means that simple case-expressions over booleans will print as <code>if</code>-<code>then</code>-<code>else</code> forms.
+Thus
+<pre>
+ > ``case b of T => 1 | F => 3``;
+ val it = ``if b then 1 else 3``: term
+</pre>
+<p>More complicated case expressions involving booleans will still print with the <code>case</code> form:
+<pre>
+ > ``case p of (x,T) => 3 | (y,F) => y``;
+ val it =
+ ``case p of (x,T) => 3 | (x,F) => x``: term
+</pre>
+</ul>
+<hr>
+
+<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-9</a></em></p>
+
+</body> </html>
@@ -2662,9 +2662,7 @@ val compare_branch_instr = save_thm("compare_branch_instr",
val error_option_case_COND_RAND = Q.store_thm("error_option_case_COND_RAND",
`!c f f1 a0 a1 a2 a3.
- error_option_case f f1
- (if c then ValueState a0 a1
- else ValueState a2 a3) =
+ error_option_CASE (if c then ValueState a0 a1 else ValueState a2 a3) f f1 =
if c then
f a0 a1
else
@@ -527,12 +527,12 @@ val _ = overload_on ("upcons", ``λx y. pcons x () y``)
val pair_case_unit = prove(
- ``pair_case (f : unit -> 'a -> 'b) v = f () (SND v)``,
+ ``pair_CASE v (f : unit -> 'a -> 'b) = f () (SND v)``,
Cases_on `v` THEN SRW_TAC [][oneTheory.one]);
val option_case_unit = prove(
- ``option_case n (f : unit # 'a -> 'b) (OPTION_MAP ($, ()) x) =
- option_case n (λx. f ((), x)) x``,
+ ``option_CASE (OPTION_MAP ($, ()) x) n (f : unit # 'a -> 'b) =
+ option_CASE x n (λx. f ((), x))``,
Cases_on `x` THEN SRW_TAC [][]);
val nopath_def = new_specification(
@@ -556,7 +556,8 @@ val mem_nopath = Store_thm(
val mem_nopath_expanded = Store_thm(
"mem_nopath_expanded",
- ``mem M (option_case (stopped_at M) (λy. pcons M l (f y)) v)``,
+ ``mem M (case v of NONE => stopped_at M
+ | SOME y => pcons M l (f y))``,
Cases_on `v` THEN SRW_TAC [][]);
val nopath_okpath = store_thm(
@@ -572,7 +573,7 @@ val nopath_okpath = store_thm(
val option_case_CONG = store_thm(
"option_case_CONG",
- ``(x = x') ⇒ (option_case n f x = option_case n f x')``,
+ ``(x = x') ⇒ (option_CASE x n f = option_CASE x' n f)``,
SRW_TAC [][]);
val normstar_nopath = store_thm(
@@ -54,6 +54,19 @@ val Cond =
val countable_def = Define
`countable s = ?f. !x : 'a. x IN s ==> ?n : num. f n = x`;
+val pscountable_countable = store_thm(
+ "pscountable_countable",
+ ``pred_set$countable = extra_pred_set$countable``,
+ SRW_TAC [][countable_def, pred_setTheory.countable_def, FUN_EQ_THM] THEN
+ EQ_TAC THEN STRIP_TAC THEN1
+ (IMP_RES_TAC inj_surj THEN SRW_TAC [][] THEN METIS_TAC [SURJ_DEF]) THEN
+ Q.EXISTS_TAC `\x. @n. f n = x` THEN ASM_SIMP_TAC (srw_ss())[INJ_DEF] THEN
+ MAP_EVERY Q.X_GEN_TAC [`e1`, `e2`] THEN STRIP_TAC THEN
+ SELECT_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
+ Q.X_GEN_TAC `u` THEN STRIP_TAC THEN
+ SELECT_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
+ Q.X_GEN_TAC `v` THEN REPEAT STRIP_TAC THEN SRW_TAC [][]);
+
val enumerate_def = Define `enumerate s = @f : num -> 'a. BIJ f UNIV s`;
val schroeder_close_def = Define
@@ -1281,19 +1294,16 @@ val COUNTABLE_ENUM = store_thm
++ Q.EXISTS_TAC `K e`
++ RW_TAC std_ss [EXTENSION, IN_SING, IN_IMAGE, IN_UNIV, K_THM])
++ DISJ2_TAC
- ++ Q.EXISTS_TAC `num_case e f`
+ ++ Q.EXISTS_TAC `\n. num_CASE n e f`
++ RW_TAC std_ss [IN_INSERT, IN_IMAGE, EXTENSION, IN_UNIV]
++ EQ_TAC <<
[RW_TAC std_ss [] <<
[Q.EXISTS_TAC `0`
++ RW_TAC std_ss [num_case_def],
Q.EXISTS_TAC `SUC x'`
++ RW_TAC std_ss [num_case_def]],
- RW_TAC std_ss []
- ++ Cases_on `x'` <<
- [RW_TAC std_ss [num_case_def],
- RW_TAC std_ss [num_case_def]
- ++ PROVE_TAC []]]);
+ RW_TAC std_ss [] ++
+ METIS_TAC [num_case_def, TypeBase.nchotomy_of ``:num``]]);
val BIGUNION_IMAGE_UNIV = store_thm
("BIGUNION_IMAGE_UNIV",
@@ -1504,7 +1514,7 @@ val FINITE_DISJOINT_ENUM = store_thm
++ RW_TAC std_ss []
++ Q.PAT_ASSUM `f IN X` MP_TAC
++ RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INSERT]
- ++ Q.EXISTS_TAC `num_case e f`
+ ++ Q.EXISTS_TAC `\x. num_CASE x e f`
++ CONJ_TAC
>> (RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INSERT]
++ Cases_on `x`
@@ -1684,19 +1694,9 @@ val DISJOINT_ALT = store_thm
RW_TAC std_ss [IN_DISJOINT]
++ PROVE_TAC []);
-val COUNTABLE_INSERT = store_thm
- ("COUNTABLE_INSERT",
- ``!x xs. countable (x INSERT xs) = countable xs``,
- RW_TAC std_ss []
- ++ EQ_TAC >> PROVE_TAC [COUNTABLE_SUBSET, SUBSET_DEF, IN_INSERT]
- ++ RW_TAC std_ss [countable_def, IN_INSERT]
- ++ Q.EXISTS_TAC `num_case x f`
- ++ RW_TAC std_ss []
- >> (Q.EXISTS_TAC `0`
- ++ RW_TAC std_ss [num_case_def])
- ++ RES_TAC
- ++ Q.EXISTS_TAC `SUC n`
- ++ RW_TAC std_ss [num_case_def]);
+val COUNTABLE_INSERT = save_thm(
+ "COUNTABLE_INSERT",
+ REWRITE_RULE [pscountable_countable] pred_setTheory.countable_INSERT)
val COUNTABLE_COUNT = store_thm
("COUNTABLE_COUNT",
@@ -1275,14 +1275,16 @@ val SER_BIJ_COMPRESS1 = store_thm
++ RW_TAC std_ss [])
++ Know
`sum (0, N) f =
- sum (0, N) (sum_case f (K 0) o (\n. if n IN s then INL n else INR n))`
+ sum (0, N) ((\x. sum_CASE x f (K 0)) o
+ (\n. if n IN s then INL n else INR n))`
>> (MATCH_MP_TAC SUM_EQ
++ RW_TAC std_ss [sum_case_def, o_THM, K_DEF])
++ Rewr
++ Know
`sum (0, n) (f o h) =
sum (0, n + N)
- (sum_case f (K 0) o (\i. if i < n then INL (h i) else INR (i - n)))`
+ ((\x. sum_CASE x f (K 0)) o
+ (\i. if i < n then INL (h i) else INR (i - n)))`
>> (KILL_TAC
++ REVERSE (Induct_on `N`)
>> RW_TAC arith_ss [sum, o_THM, ADD_CLAUSES, K_THM, REAL_ADD_RID]
@@ -1292,10 +1294,10 @@ val SER_BIJ_COMPRESS1 = store_thm
++ Rewr
++ MATCH_MP_TAC SUM_REORDER_LE
++ Q.PAT_ASSUM `BIJ h X Y` MP_TAC
+ ++ ASM_SIMP_TAC (srw_ss()) [sumTheory.FORALL_SUM]
++ BasicProvers.NORM_TAC std_ss [SUBSET_DEF, IN_IMAGE, INJ_DEF, IN_UNIV,
IN_COUNT, INJ_DEF, BIJ_DEF, SURJ_DEF] <<
- [MATCH_ACCEPT_TAC REAL_LE_REFL,
- Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`)
+ [Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`)
++ RW_TAC std_ss []
++ Q.EXISTS_TAC `y`
++ RW_TAC std_ss []
@@ -1335,14 +1337,16 @@ val SER_BIJ_COMPRESS2 = store_thm
++ RW_TAC std_ss [o_THM])
++ Know
`sum (0, n) f =
- sum (0, n) (sum_case f (K 0) o (\n. if n IN s then INL n else INR n))`
+ sum (0, n) ((\x. sum_CASE x f (K 0)) o
+ (\n. if n IN s then INL n else INR n))`
>> (MATCH_MP_TAC SUM_EQ
++ RW_TAC std_ss [sum_case_def, o_THM, K_DEF])
++ Rewr
++ Know
`sum (0, N) (f o h) =
sum (0, N + n)
- (sum_case f (K 0) o (\i. if i < N then INL (h i) else INR (i - N)))`
+ ((\x. sum_CASE x f (K 0)) o
+ (\i. if i < N then INL (h i) else INR (i - N)))`
>> (KILL_TAC
++ REVERSE (Induct_on `n`)
>> RW_TAC arith_ss [sum, o_THM, ADD_CLAUSES, K_THM, REAL_ADD_RID]
@@ -1351,11 +1355,11 @@ val SER_BIJ_COMPRESS2 = store_thm
++ RW_TAC arith_ss [sum_case_def, o_THM])
++ Rewr
++ MATCH_MP_TAC SUM_REORDER_LE
+ ++ ASM_SIMP_TAC (srw_ss()) [sumTheory.FORALL_SUM]
++ Q.PAT_ASSUM `BIJ h X Y` MP_TAC
++ BasicProvers.NORM_TAC std_ss [SUBSET_DEF, IN_IMAGE, INJ_DEF, IN_UNIV,
IN_COUNT, INJ_DEF, BIJ_DEF, SURJ_DEF] <<
- [MATCH_ACCEPT_TAC REAL_LE_REFL,
- Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`)
+ [Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`)
++ RW_TAC std_ss []
++ Q.EXISTS_TAC `y`
++ Suff `y < N` >> RW_TAC arith_ss []
@@ -1686,7 +1686,7 @@ val SIGMA_PROPERTY_DISJOINT_LEMMA1 = store_thm
++ RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF],
Know
`s INTER BIGUNION (IMAGE f UNIV) =
- BIGUNION (IMAGE (num_case {} (\n. s INTER f n)) UNIV)`
+ BIGUNION (IMAGE (\x. case x of 0 => {} | SUC n => s INTER f n) UNIV)`
>> (KILL_TAC
++ PSET_TAC [EXTENSION]
++ (EQ_TAC ++ RW_TAC std_ss [NOT_IN_EMPTY]) <<
@@ -1786,7 +1786,7 @@ val SIGMA_PROPERTY_DISJOINT_LEMMA2 = store_thm
++ RW_TAC std_ss [SMALLEST_CLOSED_CDI, IN_FUNSET, SUBSET_DEF],
Know
`s INTER BIGUNION (IMAGE f UNIV) =
- BIGUNION (IMAGE (num_case {} (\n. s INTER f n)) UNIV)`
+ BIGUNION (IMAGE (\x. case x of 0 => {} | SUC n => s INTER f n) UNIV)`
>> (KILL_TAC
++ PSET_TAC [EXTENSION]
++ (EQ_TAC ++ RW_TAC std_ss [NOT_IN_EMPTY]) <<
@@ -2194,7 +2194,7 @@ val MONOTONE_CONVERGENCE = store_thm
RW_TAC std_ss [measure_space_def, IN_FUNSET, IN_UNIV]
++ (MP_TAC o
INST_TYPE [beta |-> ``:num``] o
- Q.SPECL [`m`, `BIGUNION (IMAGE f UNIV)`, `num_case {} f`])
+ Q.SPECL [`m`, `BIGUNION (IMAGE f UNIV)`, `\x. num_CASE x {} f`])
MEASURE_COUNTABLE_INCREASING
++ Cond
>> (RW_TAC std_ss [IN_FUNSET, IN_UNIV, num_case_def, measure_space_def] <<
@@ -2216,7 +2216,7 @@ val MONOTONE_CONVERGENCE = store_thm
++ RW_TAC std_ss [num_case_def]
++ PROVE_TAC []]])
++ RW_TAC std_ss []
- ++ Know `measure m o f = (\n. (measure m o (num_case {} f)) (SUC n))`
+ ++ Know `measure m o f = (\n. (measure m o (\x. num_CASE x {} f)) (SUC n))`
>> (FUN_EQ_TAC
++ RW_TAC std_ss [num_case_def, o_THM])
++ Rewr
@@ -57,7 +57,7 @@ val SHD_STL_ISO = store_thm
("SHD_STL_ISO",
``!h t. ?x. (shd x = h) /\ (stl x = t)``,
REPEAT STRIP_TAC
- ++ Q.EXISTS_TAC `num_case h t`
+ ++ Q.EXISTS_TAC `\x. num_CASE x h t`
++ RW_TAC arith_ss [shd_def]
++ MATCH_MP_TAC EQ_EXT
++ Cases >> RW_TAC std_ss [stl_def]
@@ -178,7 +178,7 @@ RWstore_thm("dest_nConst_thm", `dest_nConst (nConst a) = a`,
SRW_TAC [][dest_nConst_def]);
val nterm_case_def = Define`
- nterm_case Nf Sf Tf Pf Cf t =
+ nterm_CASE t Nf Sf Tf Pf Cf =
if is_Nom t then Nf (dest_Nom t) else
if is_Sus t then UNCURRY Sf (dest_Sus t) else
if is_Tie t then UNCURRY Tf (dest_Tie t) else
@@ -193,7 +193,7 @@ val nterm_case_cong = Q.store_thm(
(∀a t. (t' = Tie a t) ⇒ (Tf a t = Tf' a t)) ∧
(∀t1 t2. (t' = nPair t1 t2) ⇒ (Pf t1 t2 = Pf' t1 t2)) ∧
(∀c. (t' = nConst c) ⇒ (Cf c = Cf' c)) ⇒
- (nterm_case Nf Sf Tf Pf Cf t = nterm_case Nf' Sf' Tf' Pf' Cf' t')`,
+ (nterm_CASE t Nf Sf Tf Pf Cf = nterm_CASE t' Nf' Sf' Tf' Pf' Cf')`,
REPEAT GEN_TAC THEN
Q.SPEC_THEN `t'` STRUCT_CASES_TAC nterm_nchotomy THEN
SIMP_TAC (srw_ss())
@@ -205,23 +205,23 @@ METIS_TAC [permeq_refl]);
val nterm_case_rewrites = RWstore_thm(
"nterm_case_rewrites",
-`(nterm_case Nf Sf Tf Pf Cf (Nom a) = Nf a) ∧
- (nterm_case Nf Sf Tf Pf Cf (Tie a t) = Tf a t) ∧
- (nterm_case Nf Sf Tf Pf Cf (nPair t1 t2) = Pf t1 t2) ∧
- (nterm_case Nf Sf Tf Pf Cf (nConst c) = Cf c)`,
+`(nterm_CASE (Nom a) Nf Sf Tf Pf Cf = Nf a) ∧
+ (nterm_CASE (Tie a t) Nf Sf Tf Pf Cf = Tf a t) ∧
+ (nterm_CASE (nPair t1 t2) Nf Sf Tf Pf Cf = Pf t1 t2) ∧
+ (nterm_CASE (nConst c) Nf Sf Tf Pf Cf = Cf c)`,
SIMP_TAC (srw_ss()) [nterm_case_def]);
val Sus_case1 = Q.store_thm(
"Sus_case1",
-`nterm_case Nf Sf Tf Pf Cf (Sus p v) = Sf (@p'. p' == p) v`,
+`nterm_CASE (Sus p v) Nf Sf Tf Pf Cf = Sf (@p'. p' == p) v`,
SRW_TAC [] [nterm_case_def]);
(* Unfortunately this theorem is wasted when using Define, since only
Sus_case1 goes into the case theorem given to the TypeBase *)
val Sus_case2 = Q.store_thm(
"Sus_case2",
`(∀p1 p2. (p1 == p2) ⇒ (Sf p1 v = Sf p2 v)) ⇒
- (nterm_case Nf Sf Tf Pf Cf (Sus p v) = Sf p v)`,
+ (nterm_CASE (Sus p v) Nf Sf Tf Pf Cf = Sf p v)`,
SRW_TAC [] [nterm_case_def] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
SELECT_ELIM_TAC THEN SRW_TAC [][]);
Oops, something went wrong.

0 comments on commit f1e3c53

Please sign in to comment.