Skip to content

Commit 4874b68

Browse files
dnezamdnezam
authored
Use Theory syntax in examples (#1657)
* Use Theory in examples/acl2 * Use Theory in examples/AKS * Use Theory in examples/CCS * Use Theory in examples/Crypto * Use Theory in examples/Hoare-for-divergence * Use Theory in examples/HolBdd * Use Theory in examples/HolCheck * Use Theory in examples/MLsyntax * Use Theory in examples/PSL * Use Theory in examples/STE * Use Theory in examples/algebra * Use Theory in examples/algorithms * Use Theory in examples/arm * Use Theory in examples/axiomatic-developments * Use Theory in examples/balanced_bst * Use Theory in examples/bnf-datatypes * Use Theory in examples/category * Use Theory in examples/computability * Use Theory in examples/countchars * Use Theory in examples/cv_compute * Use Theory in examples/decidable_separationLogic * Use Theory in examples/dependability * Use Theory in examples/dev * Use Theory in examples/developers * Use Theory in examples/diningcryptos * Use Theory in examples/elliptic * Use Theory in examples/fermat * Use Theory in examples/finite-test-set * Use Theory in examples/formal-languages * Use Theory in examples/fun-op-sem * Use Theory in examples/generic_graphs * Use Theory in examples/hardware * Use Theory in examples/hfs * Use Theory in examples/imperative * Use Theory in examples/ind_def * Use Theory in examples/l3-machine-code * Use Theory in examples/lambda * Use Theory in examples/logic * Use Theory in examples/machine-code * Use Theory in examples/miller * Use Theory in examples/misc * Use Theory in examples/padics * Use Theory in examples/parity * Use Theory in examples/pgcl * Use Theory in examples/probability * Use Theory in examples/rings * Use Theory in examples/separationLogic * Use Theory in examples/simple_complexity * Use Theory in examples/theorem-prover * Use Theory in examples/vector * Use Theory in examples/zipper * Delete tempScript.sml With the Theory syntax it is outdated.
1 parent 1ae4ba8 commit 4874b68

File tree

882 files changed

+4725
-9795
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

882 files changed

+4725
-9795
lines changed

‎examples/AKS/compute/computeAKSScript.sml‎

Lines changed: 7 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -4,33 +4,18 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computeAKS";
7+
Theory computeAKS
8+
Ancestors
9+
pred_set list arithmetic number combinatorics divides gcd prime
10+
ring computeParam computeOrder computeBasic computeRing
11+
computePoly polyWeak polyRing polyMonic polyDivision
12+
Libs
13+
jcLib
1214

1315
(* ------------------------------------------------------------------------- *)
1416

1517
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
(* open dependent theories *)
19-
open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
20-
dividesTheory gcdTheory primeTheory;
21-
22-
open ringTheory;
23-
24-
(* Get dependent theories local *)
25-
open computeParamTheory computeOrderTheory;
26-
open computeBasicTheory;
27-
2818
(* val _ = load "computeRingTheory"; *)
29-
open computeRingTheory computePolyTheory;
30-
31-
open polyWeakTheory polyRingTheory;
32-
open polyMonicTheory polyDivisionTheory;
33-
3419
(* ------------------------------------------------------------------------- *)
3520
(* AKS Computations Documentation *)
3621
(* ------------------------------------------------------------------------- *)
@@ -455,8 +440,4 @@ val aks0_alt = store_thm(
455440
*)
456441

457442
(* ------------------------------------------------------------------------- *)
458-
459-
(* export theory at end *)
460-
val _ = export_theory();
461-
462443
(*===========================================================================*)

‎examples/AKS/compute/computeBasicScript.sml‎

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -4,23 +4,17 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computeBasic";
7+
Theory computeBasic
8+
Ancestors
9+
pred_set list arithmetic logroot divides gcd gcdset number
10+
combinatorics prime while
11+
Libs
12+
jcLib
1213

1314
(* ------------------------------------------------------------------------- *)
1415

1516
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory arithmeticTheory logrootTheory dividesTheory
19-
gcdTheory gcdsetTheory numberTheory combinatoricsTheory primeTheory;
20-
2117
(* val _ = load "whileTheory"; *)
22-
open whileTheory;
23-
2418
val _ = temp_overload_on("SQ", ``\n. n * n``);
2519
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
2620
val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
@@ -2080,8 +2074,4 @@ val phi_compute_eqn = store_thm(
20802074
count_coprime_eqn, coprimes_subset, SUBSET_INTER_ABSORPTION, LESS_EQ_REFL]);
20812075

20822076
(* ------------------------------------------------------------------------- *)
2083-
2084-
(* export theory at end *)
2085-
val _ = export_theory();
2086-
20872077
(*===========================================================================*)

‎examples/AKS/compute/computeOrderScript.sml‎

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -4,24 +4,16 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computeOrder";
7+
Theory computeOrder
8+
Ancestors
9+
pred_set list arithmetic number combinatorics divides gcd
10+
logroot prime group ring fieldInstances computeBasic
11+
Libs
12+
jcLib
1213

1314
(* ------------------------------------------------------------------------- *)
1415

1516
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
19-
dividesTheory gcdTheory logrootTheory primeTheory;
20-
21-
open groupTheory ringTheory fieldInstancesTheory;
22-
23-
open computeBasicTheory;
24-
2517
val _ = intLib.deprecate_int ();
2618

2719
(* ------------------------------------------------------------------------- *)
@@ -1457,8 +1449,4 @@ val ordz_fast_eqn = store_thm(
14571449
]);
14581450

14591451
(* ------------------------------------------------------------------------- *)
1460-
1461-
(* export theory at end *)
1462-
val _ = export_theory();
1463-
14641452
(*===========================================================================*)

‎examples/AKS/compute/computeParamScript.sml‎

Lines changed: 6 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -4,22 +4,13 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computeParam";
12-
137
(* ------------------------------------------------------------------------- *)
14-
15-
open jcLib;
16-
17-
open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory
18-
dividesTheory gcdTheory numberTheory combinatoricsTheory primeTheory;
19-
20-
(* Get dependent theories local *)
21-
open computeOrderTheory;
22-
open monoidTheory ringTheory;
8+
Theory computeParam
9+
Ancestors
10+
prim_rec pred_set list arithmetic logroot divides gcd number
11+
combinatorics prime computeOrder monoid ring
12+
Libs
13+
jcLib
2314

2415
val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
2516
val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
@@ -2620,8 +2611,4 @@ val param_good_range =
26202611

26212612

26222613
(* ------------------------------------------------------------------------- *)
2623-
2624-
(* export theory at end *)
2625-
val _ = export_theory();
2626-
26272614
(*===========================================================================*)

‎examples/AKS/compute/computePolyScript.sml‎

Lines changed: 8 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -4,29 +4,17 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computePoly";
12-
137
(* ------------------------------------------------------------------------- *)
8+
Theory computePoly
9+
Ancestors
10+
pred_set list rich_list arithmetic number combinatorics divides
11+
gcd logroot while ring polynomial polyWeak polyRing polyField
12+
polyMonic polyEval polyDivision polyFieldDivision
13+
polyFieldModulo polyBinomial computeBasic computeOrder
14+
Libs
15+
jcLib
1416

1517
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
19-
combinatoricsTheory dividesTheory gcdTheory logrootTheory whileTheory;
20-
21-
open ringTheory;
22-
23-
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
24-
open polyMonicTheory polyEvalTheory;
25-
open polyDivisionTheory polyFieldDivisionTheory polyFieldModuloTheory;
26-
open polyBinomialTheory;
27-
28-
open computeBasicTheory computeOrderTheory;
29-
3018
val _ = intLib.deprecate_int ();
3119

3220
val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
@@ -2528,8 +2516,4 @@ val old_unity_mod_length = store_thm(
25282516
rw[PAD_RIGHT_LENGTH, MAX_DEF]);
25292517

25302518
(* ------------------------------------------------------------------------- *)
2531-
2532-
(* export theory at end *)
2533-
val _ = export_theory();
2534-
25352519
(*===========================================================================*)

‎examples/AKS/compute/computeRingScript.sml‎

Lines changed: 9 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -4,29 +4,19 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "computeRing";
7+
Theory computeRing
8+
Ancestors
9+
pred_set list rich_list arithmetic number combinatorics divides
10+
gcd logroot ring polynomial polyWeak polyRing polyField
11+
polyMonic polyEval polyDivision polyFieldDivision
12+
polyFieldModulo polyBinomial computeBasic computeOrder
13+
computePoly
14+
Libs
15+
jcLib
1216

1317
(* ------------------------------------------------------------------------- *)
1418

1519
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
19-
combinatoricsTheory dividesTheory gcdTheory logrootTheory;
20-
21-
open ringTheory;
22-
23-
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
24-
open polyMonicTheory polyEvalTheory;
25-
open polyDivisionTheory polyFieldDivisionTheory polyFieldModuloTheory;
26-
open polyBinomialTheory;
27-
28-
open computeBasicTheory computeOrderTheory computePolyTheory;
29-
3020
val _ = intLib.deprecate_int ();
3121

3222
val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
@@ -743,8 +733,4 @@ val ZN_unity_mod_X_exp_n_add_c = store_thm(
743733

744734

745735
(* ------------------------------------------------------------------------- *)
746-
747-
(* export theory at end *)
748-
val _ = export_theory();
749-
750736
(*===========================================================================*)

‎examples/AKS/machine/countAKSScript.sml‎

Lines changed: 13 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -4,47 +4,24 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "countAKS";
12-
137
(* ------------------------------------------------------------------------- *)
8+
Theory countAKS
9+
Ancestors
10+
pred_set list arithmetic divides gcd rich_list listRange number
11+
combinatorics logroot pair option prime ring countMonad
12+
countMacro countModulo countOrder countParam countPower
13+
countPoly bitsize complexity loopIncrease loopDecrease
14+
loopDivide loopList computeParam computeAKS
15+
computeBasic (* for power_free_check_eqn *)
16+
computePoly (* for unity_mod_monomial *)
17+
(* Try: import computeRing rather than computePoly *)
18+
polynomial polyWeak
19+
Libs
20+
jcLib monadsyntax
1421

1522
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory
19-
rich_listTheory listRangeTheory numberTheory combinatoricsTheory
20-
logrootTheory pairTheory optionTheory primeTheory;
21-
22-
open ringTheory;
23-
24-
(* Get dependent theories local *)
25-
open countMonadTheory countMacroTheory;
26-
open countModuloTheory countOrderTheory;
27-
open countParamTheory;
28-
2923
(* val _ = load "countPowerTheory"; *)
30-
open countPowerTheory;
31-
3224
(* val _ = load "countPolyTheory"; *)
33-
open countPolyTheory;
34-
35-
open bitsizeTheory complexityTheory;
36-
open loopIncreaseTheory loopDecreaseTheory;
37-
open loopDivideTheory loopListTheory;
38-
39-
open monadsyntax;
40-
41-
open computeParamTheory computeAKSTheory;
42-
open computeBasicTheory; (* for power_free_check_eqn *)
43-
44-
open computePolyTheory; (* for unity_mod_monomial *)
45-
(* Try: import computeRing rather than computePoly *)
46-
47-
open polynomialTheory polyWeakTheory;
4825

4926
val _ = monadsyntax.enable_monadsyntax();
5027
val _ = monadsyntax.enable_monad "Count";
@@ -1370,8 +1347,4 @@ val aksM_thm = store_thm(
13701347
(* Note: aks0 n = aks n is proved in AKSclean: aks0_eq_aks *)
13711348

13721349
(* ------------------------------------------------------------------------- *)
1373-
1374-
(* export theory at end *)
1375-
val _ = export_theory();
1376-
13771350
(*===========================================================================*)

‎examples/AKS/machine/countBasicScript.sml‎

Lines changed: 8 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -4,31 +4,20 @@
44

55
(*===========================================================================*)
66

7-
(* add all dependent libraries for script *)
8-
open HolKernel boolLib bossLib Parse;
9-
10-
(* declare new theory at start *)
11-
val _ = new_theory "countBasic";
12-
137
(* ------------------------------------------------------------------------- *)
8+
Theory countBasic
9+
Ancestors
10+
pred_set list arithmetic number combinatorics divides gcd
11+
logroot pair option listRange prime countMonad countMacro
12+
bitsize complexity loopIncrease loopDecrease loopDivide
13+
loopMultiply (* for loop2_mul_rise_steps_le *)
14+
Libs
15+
jcLib monadsyntax
1416

1517
(* val _ = load "jcLib"; *)
16-
open jcLib;
17-
18-
open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
19-
dividesTheory gcdTheory logrootTheory pairTheory optionTheory
20-
listRangeTheory primeTheory;
21-
22-
open countMonadTheory countMacroTheory;
2318

24-
open bitsizeTheory complexityTheory;
25-
open loopIncreaseTheory loopDecreaseTheory;
26-
open loopDivideTheory;
27-
open loopMultiplyTheory; (* for loop2_mul_rise_steps_le *)
2819

2920
(* val _ = load "monadsyntax"; *)
30-
open monadsyntax;
31-
3221
val _ = monadsyntax.enable_monadsyntax();
3322
val _ = monadsyntax.enable_monad "Count";
3423

@@ -988,8 +977,4 @@ val ulogM_thm = store_thm(
988977
metis_tac[ulogM_value, ulogM_steps_big_O]);
989978

990979
(* ------------------------------------------------------------------------- *)
991-
992-
(* export theory at end *)
993-
val _ = export_theory();
994-
995980
(*===========================================================================*)

0 commit comments

Comments
 (0)