From d9c43039ffbc18492acec03e554caabc07f737c4 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Mon, 22 Apr 2024 03:45:18 +1000 Subject: [PATCH] Changes of examples/{AKS|fermat|simple_complexity} after src/algebra/monoidThoery --- examples/AKS/compute/Holmakefile | 4 +- examples/AKS/compute/computeAKSScript.sml | 24 +- examples/AKS/compute/computeBasicScript.sml | 30 +- examples/AKS/compute/computeOrderScript.sml | 32 +- examples/AKS/compute/computeParamScript.sml | 26 +- examples/AKS/compute/computePolyScript.sml | 29 +- examples/AKS/compute/computeRingScript.sml | 33 +- examples/AKS/machine/Holmakefile | 4 +- examples/AKS/machine/countAKSScript.sml | 27 +- examples/AKS/machine/countBasicScript.sml | 26 +- examples/AKS/machine/countMacroScript.sml | 31 +- examples/AKS/machine/countModuloScript.sml | 34 +- examples/AKS/machine/countMonadScript.sml | 11 +- examples/AKS/machine/countOrderScript.sml | 28 +- examples/AKS/machine/countParamScript.sml | 27 +- examples/AKS/machine/countPolyScript.sml | 30 +- examples/AKS/machine/countPowerScript.sml | 33 +- examples/AKS/machine/countPrimeScript.sml | 29 +- examples/AKS/theories/AKScleanScript.sml | 20 +- examples/AKS/theories/AKSimprovedScript.sml | 25 +- examples/AKS/theories/AKSintroScript.sml | 31 +- examples/AKS/theories/AKSmapsScript.sml | 20 +- examples/AKS/theories/AKSrevisedScript.sml | 23 +- examples/AKS/theories/AKSsetsScript.sml | 26 +- examples/AKS/theories/AKSshiftScript.sml | 41 +- examples/AKS/theories/AKStheoremScript.sml | 23 +- examples/AKS/theories/Holmakefile | 4 +- examples/fermat/count/Holmakefile | 4 +- examples/fermat/count/combinatoricsScript.sml | 2809 ----------------- examples/fermat/count/helperCountScript.sml | 531 ---- examples/fermat/count/mapCountScript.sml | 20 +- examples/fermat/count/permutationScript.sml | 17 +- examples/fermat/count/symmetryScript.sml | 16 +- examples/fermat/little/FLTactionScript.sml | 15 +- examples/fermat/little/FLTbinomialScript.sml | 69 +- examples/fermat/little/FLTeulerScript.sml | 64 +- .../fermat/little/FLTfixedpointScript.sml | 9 +- examples/fermat/little/FLTgroupScript.sml | 43 +- examples/fermat/little/FLTnecklaceScript.sml | 14 +- examples/fermat/little/FLTnumberScript.sml | 14 +- examples/fermat/little/FLTpetersenScript.sml | 11 +- examples/fermat/little/Holmakefile | 4 +- examples/fermat/little/cycleScript.sml | 9 +- examples/fermat/little/necklaceScript.sml | 1033 ------ examples/fermat/little/patternScript.sml | 10 +- examples/fermat/twosq/Holmakefile | 4 +- examples/fermat/twosq/cornerScript.sml | 16 +- examples/fermat/twosq/helperTwosqScript.sml | 17 +- examples/fermat/twosq/hoppingScript.sml | 23 +- .../fermat/twosq/involuteActionScript.sml | 10 +- examples/fermat/twosq/involuteFixScript.sml | 9 +- examples/fermat/twosq/involuteScript.sml | 13 +- .../fermat/twosq/iterateComposeScript.sml | 15 +- .../fermat/twosq/iterateComputeScript.sml | 28 +- examples/fermat/twosq/iterationScript.sml | 13 +- examples/fermat/twosq/quarityScript.sml | 31 +- examples/fermat/twosq/twoSquaresScript.sml | 26 +- examples/fermat/twosq/windmillScript.sml | 19 +- examples/simple_complexity/lib/Holmakefile | 2 +- .../simple_complexity/lib/bitsizeScript.sml | 18 +- .../lib/complexityScript.sml | 19 +- examples/simple_complexity/loop/Holmakefile | 2 +- .../loop/loopDecreaseScript.sml | 17 +- .../loop/loopDivideScript.sml | 22 +- .../loop/loopIncreaseScript.sml | 16 +- .../simple_complexity/loop/loopListScript.sml | 13 +- .../loop/loopMultiplyScript.sml | 17 +- .../simple_complexity/loop/loopScript.sml | 15 +- 68 files changed, 273 insertions(+), 5455 deletions(-) delete mode 100644 examples/fermat/count/combinatoricsScript.sml delete mode 100644 examples/fermat/count/helperCountScript.sml delete mode 100644 examples/fermat/little/necklaceScript.sml diff --git a/examples/AKS/compute/Holmakefile b/examples/AKS/compute/Holmakefile index 58e20303cf..5fd92ae750 100644 --- a/examples/AKS/compute/Holmakefile +++ b/examples/AKS/compute/Holmakefile @@ -1,4 +1,2 @@ -PRE_INCLUDES = ../../algebra/ring - -ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield +ALGEBRA_INCLUDES = group ring field polynomial finitefield INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) diff --git a/examples/AKS/compute/computeAKSScript.sml b/examples/AKS/compute/computeAKSScript.sml index 529d5de288..3d51a99bd8 100644 --- a/examples/AKS/compute/computeAKSScript.sml +++ b/examples/AKS/compute/computeAKSScript.sml @@ -12,11 +12,12 @@ val _ = new_theory "computeAKS"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +(* open dependent theories *) +open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory + dividesTheory gcdTheory primeTheory; (* Get dependent theories local *) (* val _ = load "computeParamTheory"; *) @@ -29,27 +30,8 @@ open computeRingTheory computePolyTheory; open polyWeakTheory polyRingTheory; open polyMonicTheory polyDivisionTheory; -(* -open helperFunctionTheory; (* for SQRT_LE *) -open logPowerTheory; (* for ulog *) -open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *) -open monoidOrderTheory; -*) open ringInstancesTheory; (* for ZN_ring *) -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory; - -(* open dependent theories *) -open pred_setTheory listTheory arithmeticTheory; -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; -open logPowerTheory; - - (* ------------------------------------------------------------------------- *) (* AKS Computations Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/compute/computeBasicScript.sml b/examples/AKS/compute/computeBasicScript.sml index fbc1e860b3..193d942810 100644 --- a/examples/AKS/compute/computeBasicScript.sml +++ b/examples/AKS/compute/computeBasicScript.sml @@ -12,38 +12,18 @@ val _ = new_theory "computeBasic"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) - -(* Get dependent theories local *) - -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *) -(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *) -(* val _ = load "logPowerTheory"; *) -open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; -open pred_setTheory listTheory arithmeticTheory; - -open logPowerTheory; (* for LOG2, SQRT, and Perfect Power, Power Free *) -open logrootTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* val _ = load "GaussTheory"; *) -open EulerTheory; -open GaussTheory; +open pred_setTheory listTheory arithmeticTheory logrootTheory dividesTheory + gcdTheory gcdsetTheory numberTheory combinatoricsTheory primeTheory; (* val _ = load "whileTheory"; *) open whileTheory; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Basic Computations Documentation *) diff --git a/examples/AKS/compute/computeOrderScript.sml b/examples/AKS/compute/computeOrderScript.sml index 74b17b5396..0f464af2f2 100644 --- a/examples/AKS/compute/computeOrderScript.sml +++ b/examples/AKS/compute/computeOrderScript.sml @@ -12,46 +12,18 @@ val _ = new_theory "computeOrder"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) - -(* Get dependent theories local *) - -(* open dependent theories *) -(* val _ = load "fieldInstancesTheory"; *) +open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory + dividesTheory gcdTheory logrootTheory primeTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *) -(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *) -open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; -open pred_setTheory listTheory arithmeticTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* val _ = load "fieldInstancesTheory"; *) -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; open groupOrderTheory; -open monoidOrderTheory; -(* val _ = load "GaussTheory"; *) -open EulerTheory; -open GaussTheory; - -(* val _ = load "computeBasicTheory"; *) open computeBasicTheory; -open logrootTheory logPowerTheory; - (* ------------------------------------------------------------------------- *) (* Order Computations Documentation *) diff --git a/examples/AKS/compute/computeParamScript.sml b/examples/AKS/compute/computeParamScript.sml index 0db2386213..6ed5e66079 100644 --- a/examples/AKS/compute/computeParamScript.sml +++ b/examples/AKS/compute/computeParamScript.sml @@ -14,26 +14,17 @@ val _ = new_theory "computeParam"; open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory + dividesTheory gcdTheory numberTheory combinatoricsTheory primeTheory; (* Get dependent theories local *) open computeOrderTheory; -open helperFunctionTheory; (* for SQRT_LE *) -open logPowerTheory; (* for ulog *) open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *) -open monoidOrderTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory; - -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -open GaussTheory; (* for phi_pos *) -open EulerTheory; (* for residue_def *) -open triangleTheory; (* for list_lcm_pos *) +open monoidTheory; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* AKS Parameter Documentation *) @@ -67,7 +58,6 @@ open triangleTheory; (* for list_lcm_pos *) coprime_candidates_ne_1 |- !n m. 1 < m ==> 1 NOTIN coprime_candidates n m ZN_order_good_enough |- !n m. 1 < n /\ 1 < m ==> ?k. 1 < k /\ coprime k n /\ m <= ordz k n - Smallest Candidate least_prime_candidates_property |- !n m. 1 < n /\ 0 < m ==> !h. prime h /\ coprime h n /\ h < MIN_SET (prime_candidates n m) ==> @@ -278,10 +268,6 @@ open triangleTheory; (* for list_lcm_pos *) param_good_range |- !n k. (param n = good k) ==> 1 < n /\ 1 < k /\ k < n *) -(* ------------------------------------------------------------------------- *) -(* Helper Theorems *) -(* ------------------------------------------------------------------------- *) - (* ------------------------------------------------------------------------- *) (* AKS Parameter *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/compute/computePolyScript.sml b/examples/AKS/compute/computePolyScript.sml index 85e912fb15..29d2fa8f8b 100644 --- a/examples/AKS/compute/computePolyScript.sml +++ b/examples/AKS/compute/computePolyScript.sml @@ -12,27 +12,11 @@ val _ = new_theory "computePoly"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) - -(* Get dependent theories local *) - -(* open dependent theories *) -(* val _ = load "fieldInstancesTheory"; *) - -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open pred_setTheory listTheory arithmeticTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; +open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory + combinatoricsTheory dividesTheory gcdTheory logrootTheory whileTheory; (* val _ = load "polyFieldModuloTheory"; *) open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory; @@ -46,13 +30,10 @@ open ringBinomialTheory; (* val _ = load "computeOrderTheory"; *) open computeBasicTheory computeOrderTheory; -open logrootTheory logPowerTheory; - -(* val _ = load "whileTheory"; *) -open whileTheory; - -open rich_listTheory; (* for FRONT and LAST *) +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Polynomial Computations Documentation *) diff --git a/examples/AKS/compute/computeRingScript.sml b/examples/AKS/compute/computeRingScript.sml index 38c6e73ad6..55dca4fd1f 100644 --- a/examples/AKS/compute/computeRingScript.sml +++ b/examples/AKS/compute/computeRingScript.sml @@ -12,34 +12,11 @@ val _ = new_theory "computeRing"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) - -(* Get dependent theories local *) - -(* open dependent theories *) -(* val _ = load "fieldInstancesTheory"; *) - -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open pred_setTheory listTheory arithmeticTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* -polyBinomial.hol polyEval.hol polyGCD.hol polyRing.hol -polyDerivative.hol polyField.hol polyIrreducible.hol polyRoot.hol -polyDivides.hol polyFieldDivision.hol polyMonic.hol polyWeak.hol -polyDivision.hol polyFieldModulo.hol polyProduct.hol polynomial.hol -*) +open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory + combinatoricsTheory dividesTheory gcdTheory logrootTheory; (* val _ = load "polyFieldModuloTheory"; *) open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory; @@ -53,11 +30,11 @@ open ringBinomialTheory; (* val _ = load "computePolyTheory"; *) open computeBasicTheory computeOrderTheory computePolyTheory; -open logrootTheory logPowerTheory; - open ringInstancesTheory; -open rich_listTheory; (* for FRONT and LAST *) +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Modulo Polynomial Computations in (ZN n) Ring Documentation *) diff --git a/examples/AKS/machine/Holmakefile b/examples/AKS/machine/Holmakefile index 869daf0102..8ad1f406f8 100644 --- a/examples/AKS/machine/Holmakefile +++ b/examples/AKS/machine/Holmakefile @@ -1,6 +1,4 @@ -PRE_INCLUDES = ../../algebra/ring - -ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield +ALGEBRA_INCLUDES = group ring field polynomial finitefield INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) \ ../../simple_complexity/lib ../../simple_complexity/loop ../compute \ $(HOLDIR)/src/monad/more_monads diff --git a/examples/AKS/machine/countAKSScript.sml b/examples/AKS/machine/countAKSScript.sml index cca6b11a1e..93ae6be990 100644 --- a/examples/AKS/machine/countAKSScript.sml +++ b/examples/AKS/machine/countAKSScript.sml @@ -12,12 +12,12 @@ val _ = new_theory "countAKS"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + rich_listTheory listRangeTheory numberTheory combinatoricsTheory + logrootTheory pairTheory optionTheory primeTheory; (* Get dependent theories local *) (* val _ = load "countParamTheory"; *) @@ -35,29 +35,11 @@ open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory loopListTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; -open rich_listTheory listRangeTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - -(* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; (* val _ = load "ringInstancesTheory"; *) open ringInstancesTheory; (* for ZN order *) -(* val _ = load "computeAKSTheory"; *) open computeParamTheory computeAKSTheory; open computeBasicTheory; (* for power_free_check_eqn *) @@ -70,6 +52,9 @@ open polynomialTheory polyWeakTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* AKS computations in monadic style Documentation *) diff --git a/examples/AKS/machine/countBasicScript.sml b/examples/AKS/machine/countBasicScript.sml index e508654b7b..70c41b43f6 100644 --- a/examples/AKS/machine/countBasicScript.sml +++ b/examples/AKS/machine/countBasicScript.sml @@ -12,15 +12,13 @@ val _ = new_theory "countBasic"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory + dividesTheory gcdTheory logrootTheory pairTheory optionTheory + listRangeTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "countMacroTheory"; *) open countMonadTheory countMacroTheory; open bitsizeTheory complexityTheory; @@ -28,27 +26,15 @@ open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory; open loopMultiplyTheory; (* for loop2_mul_rise_steps_le *) -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open pred_setTheory listTheory arithmeticTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* val _ = load "logPowerTheory"; *) -open logrootTheory logPowerTheory; - (* val _ = load "monadsyntax"; *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Basic Computations with Count Monad Documentation *) diff --git a/examples/AKS/machine/countMacroScript.sml b/examples/AKS/machine/countMacroScript.sml index a1979d3218..caba76d540 100644 --- a/examples/AKS/machine/countMacroScript.sml +++ b/examples/AKS/machine/countMacroScript.sml @@ -12,48 +12,29 @@ val _ = new_theory "countMacro"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory rich_listTheory arithmeticTheory dividesTheory + gcdTheory numberTheory combinatoricsTheory pairTheory optionTheory + listRangeTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "complexityTheory"; *) open bitsizeTheory complexityTheory; -(* val _ = load "loopIncreaseTheory"; *) -(* val _ = load "loopDecreaseTheory"; *) -(* val _ = load "loopDivideTheory"; *) -(* val _ = load "loopMultiplyTheory"; *) -(* val _ = load "loopListTheory"; *) -(* pre-load and open here for other count scripts. *) open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory loopMultiplyTheory loopListTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open pred_setTheory listTheory arithmeticTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* val _ = load "countMonadTheory"; *) open countMonadTheory; (* val _ = load "monadsyntax"; *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; -open logPowerTheory; (* for halves *) val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Macros of Count Monad Documentation *) diff --git a/examples/AKS/machine/countModuloScript.sml b/examples/AKS/machine/countModuloScript.sml index 6703b7ddb0..63b2b1517d 100644 --- a/examples/AKS/machine/countModuloScript.sml +++ b/examples/AKS/machine/countModuloScript.sml @@ -12,48 +12,30 @@ val _ = new_theory "countModulo"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + logrootTheory numberTheory combinatoricsTheory pairTheory optionTheory + listRangeTheory; -(* Get dependent theories local *) -(* val _ = load "countMacroTheory"; *) open countMonadTheory countMacroTheory; open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory loopMultiplyTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - -(* -(* val _ = load "computeBasicTheory"; *) -open computeBasicTheory; (* for exp_mod_eqn *) -*) - (* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Modulo Computations with Count Monad Documentation *) diff --git a/examples/AKS/machine/countMonadScript.sml b/examples/AKS/machine/countMonadScript.sml index 10f5e9dcde..56c63cc56c 100644 --- a/examples/AKS/machine/countMonadScript.sml +++ b/examples/AKS/machine/countMonadScript.sml @@ -12,31 +12,22 @@ val _ = new_theory "countMonad"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) - -(* Get dependent theories local *) - -(* Get dependent theories in lib *) -open pred_setTheory listTheory arithmeticTheory; +open pred_setTheory listTheory arithmeticTheory pairTheory optionTheory; (* val _ = load "errorStateMonadTheory"; *) open errorStateMonadTheory; (* val _ = load "monadsyntax"; *) open monadsyntax; -open pairTheory optionTheory; val _ = set_grammar_ancestry ["pair", "option", "arithmetic"]; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "errorState"; - (* ------------------------------------------------------------------------- *) (* Count Monad Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/machine/countOrderScript.sml b/examples/AKS/machine/countOrderScript.sml index bc22f89360..01a0472001 100644 --- a/examples/AKS/machine/countOrderScript.sml +++ b/examples/AKS/machine/countOrderScript.sml @@ -12,47 +12,31 @@ val _ = new_theory "countOrder"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + numberTheory combinatoricsTheory logrootTheory pairTheory optionTheory + listRangeTheory; -(* Get dependent theories local *) -(* val _ = load "countModuloTheory"; *) open countMonadTheory countMacroTheory; open countModuloTheory; open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - -(* val _ = load "computeOrderTheory"; *) open computeOrderTheory; (* for ordz_seek and ordz_simple *) open ringInstancesTheory; (* for ZN_order_mod_1, ZN_order_mod *) (* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Order Computations with Count Monad Documentation *) diff --git a/examples/AKS/machine/countParamScript.sml b/examples/AKS/machine/countParamScript.sml index ecb2adef39..b7cd0e0af8 100644 --- a/examples/AKS/machine/countParamScript.sml +++ b/examples/AKS/machine/countParamScript.sml @@ -12,15 +12,13 @@ val _ = new_theory "countParam"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + logrootTheory pairTheory optionTheory listRangeTheory numberTheory + combinatoricsTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "countPowerTheory"; *) open countMonadTheory countMacroTheory; open countBasicTheory countPowerTheory; @@ -30,27 +28,11 @@ open countOrderTheory; open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - (* val _ = load "computeParamTheory"; *) open computeParamTheory; (* for param_search_result *) (* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; (* val _ = load "ringInstancesTheory"; *) open ringInstancesTheory; (* for ZN order *) @@ -58,6 +40,9 @@ open ringInstancesTheory; (* for ZN order *) val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* AKS parameter with Count Monad Documentation *) diff --git a/examples/AKS/machine/countPolyScript.sml b/examples/AKS/machine/countPolyScript.sml index 6073439434..ec1c1dca8f 100644 --- a/examples/AKS/machine/countPolyScript.sml +++ b/examples/AKS/machine/countPolyScript.sml @@ -12,15 +12,13 @@ val _ = new_theory "countPoly"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + rich_listTheory listRangeTheory logrootTheory numberTheory + combinatoricsTheory pairTheory optionTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "countModuloTheory"; *) open countMonadTheory countMacroTheory; open countModuloTheory; @@ -28,24 +26,8 @@ open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory loopListTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; -open rich_listTheory listRangeTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - (* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; (* val _ = load "ringInstancesTheory"; *) open ringInstancesTheory; (* for ZN order *) @@ -59,6 +41,12 @@ open polynomialTheory polyWeakTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +(* Overload sublist by infix operator *) +val _ = temp_overload_on ("<=", ``sublist``); + +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Polynomial computations in monadic style Documentation *) diff --git a/examples/AKS/machine/countPowerScript.sml b/examples/AKS/machine/countPowerScript.sml index 7264ca42e1..31cc594edb 100644 --- a/examples/AKS/machine/countPowerScript.sml +++ b/examples/AKS/machine/countPowerScript.sml @@ -12,15 +12,13 @@ val _ = new_theory "countPower"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + numberTheory combinatoricsTheory logrootTheory pairTheory optionTheory + listRangeTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "countBasicTheory"; *) open countMonadTheory countMacroTheory; open countBasicTheory; @@ -28,31 +26,16 @@ open bitsizeTheory complexityTheory; open loopIncreaseTheory loopDecreaseTheory; open loopDivideTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - -(* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; -open listRangeTheory; - -(* (* val _ = load "sublistTheory"; -- from recurrence theory *) *) -open sublistTheory; (* for MAP_SUBLIST, SUM_SUBLIST, listRangeINC_sublist *) val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Power Computations with Count Monad Documentation *) diff --git a/examples/AKS/machine/countPrimeScript.sml b/examples/AKS/machine/countPrimeScript.sml index 57d6fb9745..9f27f0a09c 100644 --- a/examples/AKS/machine/countPrimeScript.sml +++ b/examples/AKS/machine/countPrimeScript.sml @@ -12,46 +12,27 @@ val _ = new_theory "countPrime"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +open pred_setTheory listTheory arithmeticTheory dividesTheory numberTheory + combinatoricsTheory logrootTheory pairTheory optionTheory primeTheory; -(* Get dependent theories local *) -(* val _ = load "countPowerTheory"; *) open countMonadTheory countMacroTheory; open countBasicTheory countPowerTheory; open bitsizeTheory complexityTheory; open loopIncreaseTheory; -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open pred_setTheory listTheory arithmeticTheory; -open dividesTheory; -(* open rich_listTheory listRangeTheory; *) - -(* (* val _ = load "logPowerTheory"; *) *) -open logrootTheory logPowerTheory; - -(* val _ = load "primesTheory"; *) -open primesTheory; - (* (* val _ = load "monadsyntax"; *) *) open monadsyntax; -open pairTheory optionTheory; val _ = monadsyntax.enable_monadsyntax(); val _ = monadsyntax.enable_monad "Count"; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Primality Test in monadic style Documentation *) diff --git a/examples/AKS/theories/AKScleanScript.sml b/examples/AKS/theories/AKScleanScript.sml index 144e649d65..0053ad642a 100644 --- a/examples/AKS/theories/AKScleanScript.sml +++ b/examples/AKS/theories/AKScleanScript.sml @@ -14,6 +14,10 @@ val _ = new_theory "AKSclean"; open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory + numberTheory combinatoricsTheory dividesTheory gcdTheory primeTheory; + (* Get dependent theories local *) open AKSimprovedTheory; open AKSrevisedTheory; @@ -25,16 +29,6 @@ open AKSshiftTheory; open countAKSTheory; (* for aks0_eq_aks *) -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -open dividesTheory gcdTheory; -open logPowerTheory; - open fieldInstancesTheory; open ringInstancesTheory; open groupInstancesTheory; (* for Estar_group *) @@ -53,9 +47,9 @@ open computeRingTheory; open computeParamTheory; open computeAKSTheory; -open GaussTheory; (* for phi_le *) - - +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* AKS Clean Presentation Documentation *) diff --git a/examples/AKS/theories/AKSimprovedScript.sml b/examples/AKS/theories/AKSimprovedScript.sml index 714b0dca08..3f06990199 100644 --- a/examples/AKS/theories/AKSimprovedScript.sml +++ b/examples/AKS/theories/AKSimprovedScript.sml @@ -14,6 +14,10 @@ val _ = new_theory "AKSimproved"; open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory + numberTheory combinatoricsTheory dividesTheory gcdTheory primeTheory; + (* Get dependent theories local *) open AKSrevisedTheory; open AKStheoremTheory; @@ -43,31 +47,16 @@ open monoidTheory groupTheory ringTheory fieldTheory; open subgroupTheory; open groupOrderTheory; -open monoidOrderTheory; open fieldMapTheory; open ringUnitTheory; -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -open dividesTheory gcdTheory; - -open triangleTheory; -open binomialTheory; - open ringBinomialTheory; open ringDividesTheory; -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; open groupOrderTheory; -open monoidOrderTheory; open groupCyclicTheory; @@ -79,7 +68,6 @@ open fieldOrderTheory; open fieldProductTheory; -open logPowerTheory; open computeBasicTheory; open computeOrderTheory; open computePolyTheory; @@ -99,11 +87,6 @@ open ffConjugateTheory; open ffMasterTheory; open ffMinimalTheory; -(* (* val _ = load "GaussTheory"; *) *) -open EulerTheory; -open GaussTheory; - - (* ------------------------------------------------------------------------- *) (* AKS Bounds Improvement Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/theories/AKSintroScript.sml b/examples/AKS/theories/AKSintroScript.sml index 2348e58740..13a63cf9c6 100644 --- a/examples/AKS/theories/AKSintroScript.sml +++ b/examples/AKS/theories/AKSintroScript.sml @@ -7,12 +7,15 @@ (* add all dependent libraries for script *) open HolKernel boolLib bossLib Parse; +(* open dependent theories *) +open pred_setTheory listTheory arithmeticTheory listRangeTheory dividesTheory + gcdTheory numberTheory combinatoricsTheory; + (* declare new theory at start *) val _ = new_theory "AKSintro"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; @@ -25,11 +28,6 @@ open ffUnityTheory; open ffConjugateTheory; open ffExistTheory; -(* Get polynomial theory of Ring *) -(* (* val _ = load "polyWeakTheory"; *) *) -(* (* val _ = load "polyRingTheory"; *) *) -(* (* val _ = load "polyDivisionTheory"; *) *) -(* (* val _ = load "polyMapTheory"; *) *) open polynomialTheory polyWeakTheory polyRingTheory polyDivisionTheory; open polyBinomialTheory polyEvalTheory; @@ -44,19 +42,11 @@ open polyRingModuloTheory; open polyMapTheory; open polyIrreducibleTheory; -(* Get dependent theories local *) -(* (* val _ = load "monoidTheory"; *) *) -(* (* val _ = load "groupTheory"; *) *) -(* (* val _ = load "ringTheory"; *) *) -(* (* val _ = load "ringUnitTheory"; *) *) -(* (* val _ = load "integralDomainTheory"; *) *) -(* (* val _ = load "fieldTheory"; *) *) open monoidTheory groupTheory ringTheory ringUnitTheory; open fieldTheory fieldMapTheory; (* (* val _ = load "ringBinomialTheory"; *) *) open ringBinomialTheory; -open binomialTheory; (* (* val _ = load "ringInstancesTheory"; *) *) open ringInstancesTheory; @@ -64,19 +54,6 @@ open ringInstancesTheory; (* val _ = load "computeRingTheory"; *) open computeRingTheory; (* for overloads on x^, x+^, x^+, x^- *) -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperFunctionTheory; -open helperListTheory; (* for listRangeINC_EVERY *) - -(* open dependent theories *) -open pred_setTheory listTheory arithmeticTheory; -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - - (* ------------------------------------------------------------------------- *) (* Introspective Relation for AKS Theorem Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/theories/AKSmapsScript.sml b/examples/AKS/theories/AKSmapsScript.sml index 551a5f1bca..3c0a3ddffd 100644 --- a/examples/AKS/theories/AKSmapsScript.sml +++ b/examples/AKS/theories/AKSmapsScript.sml @@ -14,13 +14,14 @@ val _ = new_theory "AKSmaps"; open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory numberTheory + logrootTheory combinatoricsTheory dividesTheory gcdTheory primeTheory; + (* Get dependent theories local *) open AKSsetsTheory; open AKSintroTheory; -(* For SQRT n and LOG2 n *) -open logPowerTheory; - open monoidTheory groupTheory ringTheory ringUnitTheory; open fieldTheory; @@ -46,20 +47,8 @@ open polyIrreducibleTheory; open subgroupTheory; open groupOrderTheory; -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory helperFunctionTheory; - -open dividesTheory gcdTheory; - -open GaussTheory; (* for phi_eq_0 *) - -open binomialTheory; open ringBinomialTheory; -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; @@ -69,7 +58,6 @@ open ffAdvancedTheory; open ffPolyTheory; open ffUnityTheory; - (* ------------------------------------------------------------------------- *) (* Mappings for Introspective Sets Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/theories/AKSrevisedScript.sml b/examples/AKS/theories/AKSrevisedScript.sml index f6cf0b1423..9eee32a6d0 100644 --- a/examples/AKS/theories/AKSrevisedScript.sml +++ b/examples/AKS/theories/AKSrevisedScript.sml @@ -14,13 +14,16 @@ val _ = new_theory "AKSrevised"; open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory numberTheory + combinatoricsTheory dividesTheory gcdTheory primeTheory; + (* Get dependent theories local *) open AKStheoremTheory; open AKSmapsTheory; open AKSsetsTheory; open AKSintroTheory; open AKSshiftTheory; -open logPowerTheory; open computeParamTheory; (* Get polynomial theory of Ring *) @@ -37,31 +40,16 @@ open polyDividesTheory; open monoidTheory groupTheory ringTheory fieldTheory; open subgroupTheory; open groupOrderTheory; -open monoidOrderTheory; open fieldMapTheory; open ringUnitTheory; -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory helperListTheory; -open helperFunctionTheory; - -open dividesTheory gcdTheory; - -open triangleTheory; -open binomialTheory; - open ringBinomialTheory; open ringDividesTheory; -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; open groupOrderTheory; -open monoidOrderTheory; open groupCyclicTheory; @@ -84,9 +72,6 @@ open ffConjugateTheory; open ffMasterTheory; open ffMinimalTheory; -open GaussTheory; - - (* ------------------------------------------------------------------------- *) (* AKS parameter k revised (not required to be prime) Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/theories/AKSsetsScript.sml b/examples/AKS/theories/AKSsetsScript.sml index d78a4f0d23..be9f71e3f4 100644 --- a/examples/AKS/theories/AKSsetsScript.sml +++ b/examples/AKS/theories/AKSsetsScript.sml @@ -12,12 +12,15 @@ val _ = new_theory "AKSsets"; (* ------------------------------------------------------------------------- *) - open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory dividesTheory + gcdTheory gcdsetTheory logrootTheory numberTheory combinatoricsTheory + primeTheory; + (* Get dependent theories local *) open AKSintroTheory; -open logPowerTheory; (* for perfect_power_condition *) open monoidTheory groupTheory ringTheory ringUnitTheory; @@ -38,27 +41,14 @@ open polyRootTheory; open polyProductTheory; open subgroupTheory; -open monoidOrderTheory groupOrderTheory; - -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory helperFunctionTheory; - -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -open binomialTheory; +open groupOrderTheory; open ringBinomialTheory; -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; -open GaussTheory; - - (* ------------------------------------------------------------------------- *) (* Introspective Sets Documentation *) (* ------------------------------------------------------------------------- *) @@ -1095,7 +1085,7 @@ val reduceP_subset_setP = store_thm( Then PM SUBSET {p | poly p /\ ((p = []) \/ deg p < n)} by SUBSET_DEF which is BIJ with {p | weak p /\ (LENGTH p = n)} by weak_poly_poly_bij Since FINITE {p | weak p /\ (LENGTH p = n)} by weak_poly_finite - so FINITE {p | poly p /\ ((p = []) \/ deg p < n)} by FINITE_BIJ_PROPERTY + so FINITE {p | poly p /\ ((p = []) \/ deg p < n)} by FINITE_BIJ Hence FINITE PM by SUBSET_FINITE *) val reduceP_finite = store_thm( @@ -1106,7 +1096,7 @@ val reduceP_finite = store_thm( `PM SUBSET {p | poly p /\ ((p = []) \/ deg p < n)}` by rw[SUBSET_DEF, reduceP_element, setP_element] >> `BIJ chop {p | weak p /\ (LENGTH p = n)} {p | poly p /\ ((p = []) \/ deg p < n)}` by rw[weak_poly_poly_bij] >> `FINITE {p | weak p /\ (LENGTH p = n)}` by rw[weak_poly_finite] >> - `FINITE {p | poly p /\ ((p = []) \/ deg p < n)}` by metis_tac[FINITE_BIJ_PROPERTY] >> + `FINITE {p | poly p /\ ((p = []) \/ deg p < n)}` by metis_tac[FINITE_BIJ] >> metis_tac[SUBSET_FINITE]); (* Theorem: 1 < k ==> |0| IN PM *) diff --git a/examples/AKS/theories/AKSshiftScript.sml b/examples/AKS/theories/AKSshiftScript.sml index 72488bd071..77d3fea338 100644 --- a/examples/AKS/theories/AKSshiftScript.sml +++ b/examples/AKS/theories/AKSshiftScript.sml @@ -12,23 +12,16 @@ val _ = new_theory "AKSshift"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) +(* open dependent theories *) +open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory + numberTheory combinatoricsTheory; -(* Get dependent theories local *) -(* val _ = load "AKSintroTheory"; *) open AKSintroTheory; open computeRingTheory; (* for overloads on x^, x+^, x^+, x^- *) -(* Get polynomial theory of Ring *) -(* (* val _ = load "polyWeakTheory"; *) *) -(* (* val _ = load "polyRingTheory"; *) *) -(* (* val _ = load "polyDivisionTheory"; *) *) -(* (* val _ = load "polyBinomialTheory"; *) *) -(* (* val _ = load "polyMapTheory"; *) *) open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory; open polyBinomialTheory polyDivisionTheory polyEvalTheory; @@ -36,46 +29,21 @@ open polyBinomialTheory polyDivisionTheory polyEvalTheory; open polyDividesTheory; open polyMonicTheory; -(* (* val _ = load "polyFieldTheory"; *) *) -(* (* val _ = load "polyFieldDivisionTheory"; *) *) -(* (* val _ = load "polyFieldModuloTheory"; *) *) open polyFieldDivisionTheory; open polyFieldModuloTheory; open polyRingModuloTheory; open polyMapTheory; -(* (* val _ = load "monoidTheory"; *) *) -(* (* val _ = load "groupTheory"; *) *) -(* (* val _ = load "ringTheory"; *) *) -(* (* val _ = load "ringUnitTheory"; *) *) -(* (* val _ = load "integralDomainTheory"; *) *) open monoidTheory groupTheory ringTheory fieldTheory; open subgroupTheory; open groupOrderTheory; -open monoidMapTheory groupMapTheory ringMapTheory; -(* open ringUnitTheory; *) - -(* Get dependent theories in lib *) -(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) -(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) -open helperNumTheory helperSetTheory helperListTheory; - -(* open dependent theories *) -open pred_setTheory listTheory arithmeticTheory; -(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) -(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) -open dividesTheory gcdTheory; - -(* (* val _ = load "binomialTheory"; *) *) -open binomialTheory; +open groupMapTheory ringMapTheory; (* (* val _ = load "ringBinomialTheory"; *) *) open ringBinomialTheory; open ringDividesTheory; -(* (* val _ = load "fieldInstancesTheory"; *) *) -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; @@ -86,7 +54,6 @@ open ffAdvancedTheory; open ffPolyTheory; open ffUnityTheory; - (* ------------------------------------------------------------------------- *) (* Introspective Shifting Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/AKS/theories/AKStheoremScript.sml b/examples/AKS/theories/AKStheoremScript.sml index 39c23fdc97..cd444d1053 100644 --- a/examples/AKS/theories/AKStheoremScript.sml +++ b/examples/AKS/theories/AKStheoremScript.sml @@ -14,18 +14,19 @@ val _ = new_theory "AKStheorem"; open jcLib; +(* open dependent theories *) +open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory + dividesTheory gcdTheory numberTheory listRangeTheory combinatoricsTheory + primeTheory; + (* Get dependent theories local *) open AKSmapsTheory; open AKSsetsTheory; open AKSintroTheory; - open AKSshiftTheory; -open logPowerTheory; open computeRingTheory; open computeParamTheory; -open EulerTheory; -open helperFunctionTheory; open monoidTheory groupTheory ringTheory ringUnitTheory; @@ -46,20 +47,9 @@ open polyCyclicTheory; open subgroupTheory; open groupOrderTheory; -(* Get dependent theories in lib *) -open helperNumTheory helperSetTheory; - -(* open dependent theories *) -open prim_recTheory pred_setTheory listTheory arithmeticTheory; -open dividesTheory gcdTheory; - -open binomialTheory; -open GaussTheory; (* for phi *) - open ringBinomialTheory; open ringDividesTheory; -open monoidInstancesTheory; open groupInstancesTheory; open ringInstancesTheory; open fieldInstancesTheory; @@ -70,6 +60,9 @@ open ffPolyTheory; open ffUnityTheory; open ffExistTheory; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* AKS Main Theorem Documentation *) diff --git a/examples/AKS/theories/Holmakefile b/examples/AKS/theories/Holmakefile index ded442cc1f..328269682f 100644 --- a/examples/AKS/theories/Holmakefile +++ b/examples/AKS/theories/Holmakefile @@ -1,5 +1,3 @@ -PRE_INCLUDES = ../../algebra/ring - -ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield +ALGEBRA_INCLUDES = group field ring polynomial finitefield INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) \ ../../simple_complexity/lib ../compute ../machine diff --git a/examples/fermat/count/Holmakefile b/examples/fermat/count/Holmakefile index 2d3e2e7bb3..ca5b666e1b 100644 --- a/examples/fermat/count/Holmakefile +++ b/examples/fermat/count/Holmakefile @@ -1,8 +1,6 @@ # prefix to HOL examples LOC_PREFIX = $(HOLDIR)/examples -PRE_INCLUDES = $(LOC_PREFIX)/algebra/ring - -ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield +ALGEBRA_INCLUDES = ring group field polynomial finitefield INCLUDES = $(patsubst %,$(LOC_PREFIX)/algebra/%,$(ALGEBRA_INCLUDES)) \ ../little ../twosq diff --git a/examples/fermat/count/combinatoricsScript.sml b/examples/fermat/count/combinatoricsScript.sml deleted file mode 100644 index c99c97514a..0000000000 --- a/examples/fermat/count/combinatoricsScript.sml +++ /dev/null @@ -1,2809 +0,0 @@ -(* ------------------------------------------------------------------------- *) -(* Combinatorics: combinations, permutations and arrangements. *) -(* ------------------------------------------------------------------------- *) - -(*===========================================================================*) - -(* add all dependent libraries for script *) -open HolKernel boolLib bossLib Parse; - -(* declare new theory at start *) -val _ = new_theory "combinatorics"; - -(* ------------------------------------------------------------------------- *) - - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - -(* val _ = load "helperCountTheory"; *) -open helperCountTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) -open EulerTheory; (* for upto_delete *) - -(* for later computation *) -open listTheory; -open rich_listTheory; -open helperListTheory; -open listRangeTheory; - -(* (* val _ = load "binomialTheory"; *) *) -open binomialTheory; (* for binomial_iff, binomial_n_n, binomial_formula2 *) - -(* (* val _ = load "necklaceTheory"; *) *) -open necklaceTheory; (* for necklace_def, necklace_finite *) - - -(* ------------------------------------------------------------------------- *) -(* Combinatorics Documentation *) -(* ------------------------------------------------------------------------- *) -(* Overloading (# is temporary): -*) -(* Definitions and Theorems (# are exported, ! are in compute): - - Counting number of combinations: - sub_count_def |- !n k. sub_count n k = {s | s SUBSET count n /\ CARD s = k} - choose_def |- !n k. n choose k = CARD (sub_count n k) - sub_count_element |- !n k s. s IN sub_count n k <=> s SUBSET count n /\ CARD s = k - sub_count_subset |- !n k. sub_count n k SUBSET POW (count n) - sub_count_finite |- !n k. FINITE (sub_count n k) - sub_count_element_no_self - |- !n k s. s IN sub_count n k ==> n NOTIN s - sub_count_element_finite - |- !n k s. s IN sub_count n k ==> FINITE s - sub_count_n_0 |- !n. sub_count n 0 = {{}} - sub_count_0_n |- !n. sub_count 0 n = if n = 0 then {{}} else {} - sub_count_n_1 |- !n. sub_count n 1 = {{j} | j < n} - sub_count_n_n |- !n. sub_count n n = {count n} - sub_count_eq_empty |- !n k. sub_count n k = {} <=> n < k - sub_count_union |- !n k. sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION - sub_count n (k + 1) - sub_count_disjoint |- !n k. DISJOINT (IMAGE (\s. n INSERT s) (sub_count n k)) - (sub_count n (k + 1)) - sub_count_insert |- !n k s. s IN sub_count n k ==> - n INSERT s IN sub_count (n + 1) (k + 1) - sub_count_insert_card - |- !n k. CARD (IMAGE (\s. n INSERT s) (sub_count n k)) = - n choose k - sub_count_alt |- !n k. sub_count n 0 = {{}} /\ sub_count 0 (k + 1) = {} /\ - sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION - sub_count n (k + 1) -! sub_count_eqn |- !n k. sub_count n k = - if k = 0 then {{}} - else if n = 0 then {} - else IMAGE (\s. n - 1 INSERT s) (sub_count (n - 1) (k - 1)) UNION - sub_count (n - 1) k - choose_n_0 |- !n. n choose 0 = 1 - choose_n_1 |- !n. n choose 1 = n - choose_eq_0 |- !n k. n choose k = 0 <=> n < k - choose_0_n |- !n. 0 choose n = if n = 0 then 1 else 0 - choose_1_n |- !n. 1 choose n = if 1 < n then 0 else 1 - choose_n_n |- !n. n choose n = 1 - choose_recurrence |- !n k. (n + 1) choose (k + 1) = n choose k + n choose (k + 1) - choose_alt |- !n k. n choose 0 = 1 /\ 0 choose (k + 1) = 0 /\ - (n + 1) choose (k + 1) = n choose k + n choose (k + 1) -! choose_eqn |- !n k. n choose k = binomial n k - - Partition of the set of subsets by bijective equivalence: - sub_sets_def |- !P k. sub_sets P k = {s | s SUBSET P /\ CARD s = k} - sub_sets_sub_count |- !n k. sub_sets (count n) k = sub_count n k - sub_sets_equiv_class|- !s t. FINITE t /\ s SUBSET t ==> - sub_sets t (CARD s) = equiv_class $=b= (POW t) s - sub_count_equiv_class - |- !n k. k <= n ==> - sub_count n k = - equiv_class $=b= (POW (count n)) (count k) - count_power_partition |- !n. partition $=b= (POW (count n)) = - IMAGE (sub_count n) (upto n) - sub_count_count_inj |- !n m. INJ (sub_count n) (upto n) - univ(:(num -> bool) -> bool) - choose_sum_over_count |- !n. SIGMA ($choose n) (upto n) = 2 ** n - choose_sum_over_all |- !n. SUM (MAP ($choose n) [0 .. n]) = 2 ** n - - Counting number of permutations: - perm_count_def |- !n. perm_count n = {ls | ALL_DISTINCT ls /\ set ls = count n} - perm_def |- !n. perm n = CARD (perm_count n) - perm_count_element |- !ls n. ls IN perm_count n <=> ALL_DISTINCT ls /\ set ls = count n - perm_count_element_no_self - |- !ls n. ls IN perm_count n ==> ~MEM n ls - perm_count_element_length - |- !ls n. ls IN perm_count n ==> LENGTH ls = n - perm_count_subset |- !n. perm_count n SUBSET necklace n n - perm_count_finite |- !n. FINITE (perm_count n) - perm_count_0 |- perm_count 0 = {[]} - perm_count_1 |- perm_count 1 = {[0]} - interleave_def |- !x ls. x interleave ls = - IMAGE (\k. TAKE k ls ++ x::DROP k ls) (upto (LENGTH ls)) - interleave_alt |- !ls x. x interleave ls = - {TAKE k ls ++ x::DROP k ls | k | k <= LENGTH ls} - interleave_element |- !ls x y. y IN x interleave ls <=> - ?k. k <= LENGTH ls /\ y = TAKE k ls ++ x::DROP k ls - interleave_nil |- !x. x interleave [] = {[x]} - interleave_length |- !ls x y. y IN x interleave ls ==> LENGTH y = 1 + LENGTH ls - interleave_distinct |- !ls x y. ALL_DISTINCT (x::ls) /\ y IN x interleave ls ==> - ALL_DISTINCT y - interleave_distinct_alt - |- !ls x y. ALL_DISTINCT ls /\ ~MEM x ls /\ - y IN x interleave ls ==> ALL_DISTINCT y - interleave_set |- !ls x y. y IN x interleave ls ==> set y = set (x::ls) - interleave_set_alt |- !ls x y. y IN x interleave ls ==> set y = x INSERT set ls - interleave_has_cons |- !ls x. x::ls IN x interleave ls - interleave_not_empty|- !ls x. x interleave ls <> {} - interleave_eq |- !n x y. ~MEM n x /\ ~MEM n y ==> - (n interleave x = n interleave y <=> x = y) - interleave_disjoint |- !l1 l2 x. ~MEM x l1 /\ l1 <> l2 ==> - DISJOINT (x interleave l1) (x interleave l2) - interleave_finite |- !ls x. FINITE (x interleave ls) - interleave_count_inj|- !ls x. ~MEM x ls ==> - INJ (\k. TAKE k ls ++ x::DROP k ls) - (upto (LENGTH ls)) univ(:'a list) - interleave_card |- !ls x. ~MEM x ls ==> CARD (x interleave ls) = 1 + LENGTH ls - interleave_revert |- !ls h. ALL_DISTINCT ls /\ MEM h ls ==> - ?t. ALL_DISTINCT t /\ ls IN h interleave t /\ - set t = set ls DELETE h - interleave_revert_count - |- !ls n. ALL_DISTINCT ls /\ set ls = upto n ==> - ?t. ALL_DISTINCT t /\ ls IN n interleave t /\ - set t = count n - perm_count_suc |- !n. perm_count (SUC n) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) - perm_count_suc_alt |- !n. perm_count (n + 1) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) -! perm_count_eqn |- !n. perm_count n = - if n = 0 then {[]} - else BIGUNION (IMAGE ($interleave (n - 1)) (perm_count (n - 1))) - perm_0 |- perm 0 = 1 - perm_1 |- perm 1 = 1 - perm_count_interleave_finite - |- !n e. e IN IMAGE ($interleave n) (perm_count n) ==> FINITE e - perm_count_interleave_card - |- !n e. e IN IMAGE ($interleave n) (perm_count n) ==> CARD e = n + 1 - perm_count_interleave_disjoint - |- !n e s t. s IN IMAGE ($interleave n) (perm_count n) /\ - t IN IMAGE ($interleave n) (perm_count n) /\ s <> t ==> - DISJOINT s t - perm_count_interleave_inj - |- !n. INJ ($interleave n) (perm_count n) univ(:num list -> bool) - perm_suc |- !n. perm (SUC n) = SUC n * perm n - perm_suc_alt |- !n. perm (n + 1) = (n + 1) * perm n -! perm_eq_fact |- !n. perm n = FACT n - - Permutations of a set: - perm_set_def |- !s. perm_set s = {ls | ALL_DISTINCT ls /\ set ls = s} - perm_set_element |- !ls s. ls IN perm_set s <=> ALL_DISTINCT ls /\ set ls = s - perm_set_perm_count |- !n. perm_set (count n) = perm_count n - perm_set_empty |- perm_set {} = {[]} - perm_set_sing |- !x. perm_set {x} = {[x]} - perm_set_eq_empty_sing - |- !s. perm_set s = {[]} <=> s = {} - perm_set_has_self_list - |- !s. FINITE s ==> SET_TO_LIST s IN perm_set s - perm_set_not_empty |- !s. FINITE s ==> perm_set s <> {} - perm_set_list_not_empty - |- !ls. perm_set (set ls) <> {} - perm_set_map_element|- !ls f s n. ls IN perm_set s /\ BIJ f s (count n) ==> - MAP f ls IN perm_count n - perm_set_map_inj |- !f s n. BIJ f s (count n) ==> INJ (MAP f) (perm_set s) (perm_count n) - perm_set_map_surj |- !f s n. BIJ f s (count n) ==> SURJ (MAP f) (perm_set s) (perm_count n) - perm_set_map_bij |- !f s n. BIJ f s (count n) ==> BIJ (MAP f) (perm_set s) (perm_count n) - perm_set_bij_eq_perm_count - |- !s. FINITE s ==> perm_set s =b= perm_count (CARD s) - perm_set_finite |- !s. FINITE s ==> FINITE (perm_set s) - perm_set_card |- !s. FINITE s ==> CARD (perm_set s) = perm (CARD s) - perm_set_card_alt |- !s. FINITE s ==> CARD (perm_set s) = FACT (CARD s) - - Counting number of arrangements: - list_count_def |- !n k. list_count n k = - {ls | ALL_DISTINCT ls /\ - set ls SUBSET count n /\ LENGTH ls = k} - arrange_def |- !n k. n arrange k = CARD (list_count n k) - list_count_alt |- !n k. list_count n k = - {ls | ALL_DISTINCT ls /\ - set ls SUBSET count n /\ CARD (set ls) = k} - list_count_element |- !ls n k. ls IN list_count n k <=> - ALL_DISTINCT ls /\ set ls SUBSET count n /\ LENGTH ls = k - list_count_element_alt - |- !ls n k. ls IN list_count n k <=> - ALL_DISTINCT ls /\ set ls SUBSET count n /\ CARD (set ls) = k - list_count_element_set_card - |- !ls n k. ls IN list_count n k ==> CARD (set ls) = k - list_count_subset |- !n k. list_count n k SUBSET necklace k n - list_count_finite |- !n k. FINITE (list_count n k) - list_count_n_0 |- !n. list_count n 0 = {[]} - list_count_0_n |- !n. 0 < n ==> list_count 0 n = {} - list_count_n_n |- !n. list_count n n = perm_count n - list_count_eq_empty |- !n k. list_count n k = {} <=> n < k - list_count_by_image |- !n k. 0 < k ==> - list_count n k = - IMAGE (\ls. if ALL_DISTINCT ls then ls else []) - (necklace k n) DELETE [] -! list_count_eqn |- !n k. list_count n k = - if k = 0 then {[]} - else IMAGE (\ls. if ALL_DISTINCT ls then ls else []) - (necklace k n) DELETE [] - feq_set_equiv |- !s. feq set equiv_on s - list_count_set_eq_class - |- !ls n k. ls IN list_count n k ==> - equiv_class (feq set) (list_count n k) ls = perm_set (set ls) - list_count_set_eq_class_card - |- !ls n k. ls IN list_count n k ==> - CARD (equiv_class (feq set) (list_count n k) ls) = perm k - list_count_set_partititon_element_card - |- !n k e. e IN partition (feq set) (list_count n k) ==> CARD e = perm k - list_count_element_perm_set_not_empty - |- !ls n k. ls IN list_count n k ==> perm_set (set ls) <> {} - list_count_set_map_element - |- !s n k. s IN partition (feq set) (list_count n k) ==> - (set o CHOICE) s IN sub_count n k - list_count_set_map_inj - |- !n k. INJ (set o CHOICE) - (partition (feq set) (list_count n k)) - (sub_count n k) - list_count_set_map_surj - |- !n k. SURJ (set o CHOICE) - (partition (feq set) (list_count n k)) - (sub_count n k) - list_count_set_map_bij - |- !n k. BIJ (set o CHOICE) - (partition (feq set) (list_count n k)) - (sub_count n k) -! arrange_eqn |- !n k. n arrange k = (n choose k) * perm k - arrange_alt |- !n k. n arrange k = (n choose k) * FACT k - arrange_formula |- !n k. n arrange k = binomial n k * FACT k - arrange_formula2 |- !n k. k <= n ==> n arrange k = FACT n DIV FACT (n - k) - arrange_n_0 |- !n. n arrange 0 = 1 - arrange_0_n |- !n. 0 < n ==> 0 arrange n = 0 - arrange_n_n |- !n. n arrange n = perm n - arrange_n_n_alt |- !n. n arrange n = FACT n - arrange_eq_0 |- !n k. n arrange k = 0 <=> n < k -*) - -(* ------------------------------------------------------------------------- *) -(* Counting number of combinations. *) -(* ------------------------------------------------------------------------- *) - -(* The strategy: -This is to show, ultimately, C(n,k) = binomial n k. - -Conceptually, -C(n,k) = number of ways to choose k elements from a set of n elements. -Each choice gives a k-subset. - -Define C(n,k) = number of k-subsets of an n-set. -Prove that C(n,k) = binomial n k: -(1) C(0,0) = 1 -(2) C(0,1) = 0 -(3) C(SUC n, SUC k) = C(n,k) + C(n,SUC k) -show that any such C's is just the binomial function. - -binomial_alt -|- !n k. binomial n 0 = 1 /\ binomial 0 (k + 1) = 0 /\ - binomial (n + 1) (k + 1) = binomial n k + binomial n (k + 1) - -Moreover, bij_eq is an equivalence relation, and partitions the power set -of (count n) into equivalence classes of k-subsets for k = 0 to n. Thus - -SUM (GENLIST (choose n) (SUC n)) = CARD (POW (count n)) = 2 ** n - -the counterpart of binomial_sum |- !n. SUM (GENLIST (binomial n) (SUC n)) = 2 ** n -*) - -(* Define the set of choices of k-subsets of (count n). *) -Definition sub_count_def[nocompute]: - sub_count n k = { (s:num -> bool) | s SUBSET (count n) /\ CARD s = k} -End -(* use [nocompute] as this is not effective for evalutaion. *) - -(* Define the number of choices of k-subsets of (count n). *) -Definition choose_def[nocompute]: - choose n k = CARD (sub_count n k) -End -(* use [nocompute] as this is not effective for evalutaion. *) -(* make this an infix operator *) -val _ = set_fixity "choose" (Infix(NONASSOC, 550)); (* higher than arithmetic op 500. *) -(* val choose_def = |- !n k. n choose k = CARD (sub_count n k): thm *) - -(* Theorem: s IN sub_count n k <=> s SUBSET count n /\ CARD s = k *) -(* Proof: by sub_count_def. *) -Theorem sub_count_element: - !n k s. s IN sub_count n k <=> s SUBSET count n /\ CARD s = k -Proof - simp[sub_count_def] -QED - -(* Theorem: (sub_count n k) SUBSET (POW (count n)) *) -(* Proof: - s IN sub_count n k - ==> s SUBSET (count n) by sub_count_def - ==> s IN POW (count n) by POW_DEF - Thus (sub_count n k) SUBSET (POW (count n)) by SUBSET_DEF -*) -Theorem sub_count_subset: - !n k. (sub_count n k) SUBSET (POW (count n)) -Proof - simp[sub_count_def, POW_DEF, SUBSET_DEF] -QED - -(* Theorem: FINITE (sub_count n k) *) -(* Proof: - Note (sub_count n k) SUBSET (POW (count n)) by sub_count_subset - and FINITE (count n) by FINITE_COUNT - so FINITE (POW (count n)) by FINITE_POW - Thus FINITE (sub_count n k) by SUBSET_FINITE -*) -Theorem sub_count_finite: - !n k. FINITE (sub_count n k) -Proof - metis_tac[sub_count_subset, FINITE_COUNT, FINITE_POW, SUBSET_FINITE] -QED - -(* Theorem: s IN sub_count n k ==> n NOTIN s *) -(* Proof: - Note s SUBSET (count n) by sub_count_element - and n NOTIN (count n) by COUNT_NOT_SELF - so n NOTIN s by SUBSET_DEF -*) -Theorem sub_count_element_no_self: - !n k s. s IN sub_count n k ==> n NOTIN s -Proof - metis_tac[sub_count_element, SUBSET_DEF, COUNT_NOT_SELF] -QED - -(* Theorem: s IN sub_count n k ==> FINITE s *) -(* Proof: - Note s SUBSET (count n) by sub_count_element - and FINITE (count n) by FINITE_COUNT - so FINITE s by SUBSET_FINITE -*) -Theorem sub_count_element_finite: - !n k s. s IN sub_count n k ==> FINITE s -Proof - metis_tac[sub_count_element, FINITE_COUNT, SUBSET_FINITE] -QED - -(* Theorem: sub_count n 0 = { EMPTY } *) -(* Proof: - By EXTENSION, IN_SING, this is to show: - (1) x IN sub_count n 0 ==> x = {} - x IN sub_count n 0 - <=> x SUBSET count n /\ CARD x = 0 by sub_count_def - ==> FINITE x /\ CARD x = 0 by SUBSET_FINITE, FINITE_COUNT - ==> x = {} by CARD_EQ_0 - (2) {} IN sub_count n 0 - {} IN sub_count n 0 - <=> {} SUBSET count n /\ CARD {} = 0 by sub_count_def - <=> T /\ CARD {} = 0 by EMPTY_SUBSET - <=> T /\ T by CARD_EMPTY - <=> T -*) -Theorem sub_count_n_0: - !n. sub_count n 0 = { EMPTY } -Proof - rewrite_tac[EXTENSION, EQ_IMP_THM] >> - rw[IN_SING] >| [ - fs[sub_count_def] >> - metis_tac[CARD_EQ_0, SUBSET_FINITE, FINITE_COUNT], - rw[sub_count_def] - ] -QED - -(* Theorem: sub_count 0 n = if n = 0 then { EMPTY } else EMPTY *) -(* Proof: - If n = 0, - then sub_count 0 n = { EMPTY } by sub_count_n_0 - If n <> 0, - s IN sub_count 0 n - <=> s SUBSET count 0 /\ CARD s = n by sub_count_def - <=> s SUBSET {} /\ CARD s = n by COUNT_0 - <=> CARD {} = n by SUBSET_EMPTY - <=> 0 = n by CARD_EMPTY - <=> F by n <> 0 - Thus sub_count 0 n = {} by MEMBER_NOT_EMPTY -*) -Theorem sub_count_0_n: - !n. sub_count 0 n = if n = 0 then { EMPTY } else EMPTY -Proof - rw[sub_count_n_0] >> - rw[sub_count_def, EXTENSION] >> - spose_not_then strip_assume_tac >> - `x = {}` by metis_tac[MEMBER_NOT_EMPTY] >> - fs[] -QED - -(* Theorem: sub_count n 1 = {{j} | j < n } *) -(* Proof: - By sub_count_def, EXTENSION, this is to show: - x SUBSET count n /\ CARD x = 1 <=> - ?j. (!x'. x' IN x <=> x' = j) /\ j < n - If part: - Note FINITE x by SUBSET_FINITE, FINITE_COUNT - so ?j. x = {j} by CARD_EQ_1, SING_DEF - Take this j. - Then !x'. x' IN x <=> x' = j - by IN_SING - and x SUBSET (count n) ==> j < n - by SUBSET_DEF, IN_COUNT - Only-if part: - Note j IN x, so x <> {} by MEMBER_NOT_EMPTY - The given shows x = {j} by ONE_ELEMENT_SING - and j < n ==> x SUBSET (count n) - by SUBSET_DEF, IN_COUNT - and CARD x = 1 by CARD_SING -*) -Theorem sub_count_n_1: - !n. sub_count n 1 = {{j} | j < n } -Proof - rw[sub_count_def, EXTENSION] >> - rw[EQ_IMP_THM] >| [ - `FINITE x` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> - `?j. x = {j}` by metis_tac[CARD_EQ_1, SING_DEF] >> - metis_tac[SUBSET_DEF, IN_SING, IN_COUNT], - rw[SUBSET_DEF], - metis_tac[ONE_ELEMENT_SING, MEMBER_NOT_EMPTY, CARD_SING] - ] -QED - -(* Theorem: sub_count n n = {count n} *) -(* Proof: - s IN sub_count n n - <=> s SUBSET count n /\ CARD s = n by sub_count_def - <=> s SUBSET count n /\ CARD s = CARD (count n) - by CARD_COUNT - <=> s SUBSET count n /\ s = count n by SUBSET_CARD_EQ - <=> T /\ s = count n by SUBSET_REFL - Thus sub_count n n = {count n} by EXTENSION -*) -Theorem sub_count_n_n: - !n. sub_count n n = {count n} -Proof - rw_tac bool_ss[EXTENSION] >> - `FINITE (count n) /\ CARD (count n) = n` by rw[] >> - metis_tac[sub_count_element, SUBSET_CARD_EQ, SUBSET_REFL, IN_SING] -QED - -(* Theorem: sub_count n k = EMPTY <=> n < k *) -(* Proof: - If part: sub_count n k = {} ==> n < k - By contradiction, suppose k <= n. - Then (count k) SUBSET (count n) by COUNT_SUBSET, k <= n - and CARD (count k) = k by CARD_COUNT - so (count k) IN sub_count n k by sub_count_element - Thus sub_count n k <> {} by MEMBER_NOT_EMPTY - which is a contradiction. - Only-if part: n < k ==> sub_count n k = {} - By contradiction, suppose sub_count n k <> {}. - Then ?s. s IN sub_count n k by MEMBER_NOT_EMPTY - ==> s SUBSET count n /\ CARD s = k - by sub_count_element - Note FINITE (count n) by FINITE_COUNT - so CARD s <= CARD (count n) by CARD_SUBSET - ==> k <= n by CARD_COUNT - This contradicts n < k. -*) -Theorem sub_count_eq_empty: - !n k. sub_count n k = EMPTY <=> n < k -Proof - rw[EQ_IMP_THM] >| [ - spose_not_then strip_assume_tac >> - `(count k) SUBSET (count n)` by rw[COUNT_SUBSET] >> - `CARD (count k) = k` by rw[] >> - metis_tac[sub_count_element, MEMBER_NOT_EMPTY], - spose_not_then strip_assume_tac >> - `?s. s IN sub_count n k` by rw[MEMBER_NOT_EMPTY] >> - fs[sub_count_element] >> - `FINITE (count n)` by rw[] >> - `CARD s <= n` by metis_tac[CARD_SUBSET, CARD_COUNT] >> - decide_tac - ] -QED - -(* Theorem: sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION sub_count n (k + 1) *) -(* Proof: - By sub_count_def, EXTENSION, this is to show: - (1) x SUBSET count (n + 1) /\ CARD x = k + 1 ==> - ?s. (!y. y IN x <=> y = n \/ y IN s) /\ - s SUBSET count n /\ CARD s = k) \/ x SUBSET count n - Suppose ~(x SUBSET count n), - Then n IN x by SUBSET_DEF - Take s = x DELETE n. - Then y IN x <=> - y = n \/ y IN s by EXTENSION - and s SUBSET x by DELETE_SUBSET - so s SUBSET (count (n + 1) DELETE n) - by SUBSET_DELETE_BOTH - or s SUBSET (count n) by count_def - Note FINITE x by SUBSET_FINITE, FINITE_COUNT - so CARD s = k by CARD_DELETE, CARD_COUNT - (2) s SUBSET count n /\ x = n INSERT s ==> x SUBSET count (n + 1) - Note x SUBSET (n INSERT count n) by SUBSET_INSERT_BOTH - so x INSERT count (n + 1) by count_def, or count_add1 - (3) s SUBSET count n /\ x = n INSERT s ==> CARD x = CARD s + 1 - Note n NOTIN s by SUBSET_DEF, COUNT_NOT_SELF - and FINITE s by SUBSET_FINITE, FINITE_COUNT - so CARD x - = SUC (CARD s) by CARD_INSERT - = CARD s + 1 by ADD1 - (4) x SUBSET count n ==> x SUBSET count (n + 1) - Note (count n) SUBSET count (n + 1) by COUNT_SUBSET, n <= n + 1 - so x SUBSET count (n + 1) by SUBSET_TRANS -*) -Theorem sub_count_union: - !n k. sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION sub_count n (k + 1) -Proof - rw[sub_count_def, EXTENSION, Once EQ_IMP_THM] >> simp[] >| [ - rename [‘x ⊆ count (n + 1)’, ‘CARD x = k + 1’] >> - Cases_on `x SUBSET count n` >> simp[] >> - `n IN x` by - (fs[SUBSET_DEF] >> rename [‘m ∈ x’, ‘¬(m < n)’] >> - `m < n + 1` by simp[] >> - `m = n` by decide_tac >> - fs[]) >> - qexists_tac `x DELETE n` >> - `FINITE x` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> - rw[] >- (rw[EQ_IMP_THM] >> simp[]) >> - `x DELETE n SUBSET (count (n + 1)) DELETE n` by rw[SUBSET_DELETE_BOTH] >> - `count (n + 1) DELETE n = count n` by rw[EXTENSION] >> - fs[], - - rename [‘s ⊆ count n’, ‘x ⊆ count (n + 1)’] >> - `x = n INSERT s` by fs[EXTENSION] >> - `x SUBSET (n INSERT count n)` by rw[SUBSET_INSERT_BOTH] >> - rfs[count_add1], - - rename [‘s ⊆ count n’, ‘CARD x = CARD s + 1’] >> - `x = n INSERT s` by fs[EXTENSION] >> - `n NOTIN s` by metis_tac[SUBSET_DEF, COUNT_NOT_SELF] >> - `FINITE s` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> - rw[], - - metis_tac[COUNT_SUBSET, SUBSET_TRANS, DECIDE “n ≤ n + 1”] - ] -QED - -(* Theorem: DISJOINT (IMAGE (\s. n INSERT s) (sub_count n k)) (sub_count n (k + 1)) *) -(* Proof: - Let s = IMAGE (\s. n INSERT s) (sub_count n k), - t = sub_count n (k + 1). - By DISJOINT_DEF and contradiction, suppose s INTER t <> {}. - Then ?x. x IN s /\ x IN t by IN_INTER, MEMBER_NOT_EMPTY - Note n IN x by IN_IMAGE, IN_INSERT - but n NOTIN x by sub_count_element_no_self - This is a contradiction. -*) -Theorem sub_count_disjoint: - !n k. DISJOINT (IMAGE (\s. n INSERT s) (sub_count n k)) (sub_count n (k + 1)) -Proof - rw[DISJOINT_DEF, EXTENSION] >> - spose_not_then strip_assume_tac >> - rename [‘s ∈ sub_count n k’, ‘x ∈ sub_count n (k + 1)’] >> - `x = n INSERT s` by fs[EXTENSION] >> - `n IN x` by fs[] >> - metis_tac[sub_count_element_no_self] -QED - -(* Theorem: s IN sub_count n k ==> (n INSERT s) IN sub_count (n + 1) (k + 1) *) -(* Proof: - Note s SUBSET count n /\ CARD s = k by sub_count_element - and n NOTIN s by sub_count_element_no_self - and FINITE s by sub_count_element_finite - Now (n INSERT s) SUBSET (n INSERT count n) - by SUBSET_INSERT_BOTH - and n INSERT count n = count (n + 1) by count_add1 - and CARD (n INSERT s) = CARD s + 1 by CARD_INSERT - = k + 1 by given - Thus (n INSERT s) IN sub_count (n + 1) (k + 1) - by sub_count_element -*) -Theorem sub_count_insert: - !n k s. s IN sub_count n k ==> (n INSERT s) IN sub_count (n + 1) (k + 1) -Proof - rw[sub_count_def] >| [ - `!x. x < n ==> x < n + 1` by decide_tac >> - metis_tac[SUBSET_DEF, IN_COUNT], - `n NOTIN s` by metis_tac[SUBSET_DEF, COUNT_NOT_SELF] >> - `FINITE s` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> - rw[] - ] -QED - -(* Theorem: CARD (IMAGE (\s. n INSERT s) (sub_count n k)) = n choose k *) -(* Proof: - Let f = \s. n INSERT s. - By choose_def, INJ_CARD_IMAGE, this is to show: - (1) FINITE (sub_count n k), true by sub_count_finite - (2) ?t. INJ f (sub_count n k) t - Let t = sub_count (n + 1) (k + 1). - By INJ_DEF, this is to show: - (1) s IN sub_count n k ==> n INSERT s IN sub_count (n + 1) (k + 1) - This is true by sub_count_insert - (2) s' IN sub_count n k /\ s IN sub_count n k /\ - n INSERT s' = n INSERT s ==> s' = s - Note n NOTIN s by sub_count_element_no_self - and n NOTIN s' by sub_count_element_no_self - s' - = s' DELETE n by DELETE_NON_ELEMENT - = (n INSERT s') DELETE n by DELETE_INSERT - = (n INSERT s) DELETE n by given - = s DELETE n by DELETE_INSERT - = s by DELETE_NON_ELEMENT -*) -Theorem sub_count_insert_card: - !n k. CARD (IMAGE (\s. n INSERT s) (sub_count n k)) = n choose k -Proof - rw[choose_def] >> - qabbrev_tac `f = \s. n INSERT s` >> - irule INJ_CARD_IMAGE >> - rpt strip_tac >- - rw[sub_count_finite] >> - qexists_tac `sub_count (n + 1) (k + 1)` >> - rw[INJ_DEF, Abbr`f`] >- - rw[sub_count_insert] >> - rename [‘n INSERT s1 = n INSERT s2’] >> - `n NOTIN s1 /\ n NOTIN s2` by metis_tac[sub_count_element_no_self] >> - metis_tac[DELETE_INSERT, DELETE_NON_ELEMENT] -QED - -(* Theorem: sub_count n 0 = { EMPTY } /\ - sub_count 0 (k + 1) = {} /\ - sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION sub_count n (k + 1) *) -(* Proof: by sub_count_n_0, sub_count_0_n, sub_count_union. *) -Theorem sub_count_alt: - !n k. sub_count n 0 = { EMPTY } /\ - sub_count 0 (k + 1) = {} /\ - sub_count (n + 1) (k + 1) = - IMAGE (\s. n INSERT s) (sub_count n k) UNION sub_count n (k + 1) -Proof - simp[sub_count_n_0, sub_count_0_n, sub_count_union] -QED - -(* Theorem: sub_count n k = - if k = 0 then { EMPTY } - else if n = 0 then {} - else IMAGE (\s. (n - 1) INSERT s) (sub_count (n - 1) (k - 1)) UNION - sub_count (n - 1) k *) -(* Proof: by sub_count_n_0, sub_count_0_n, sub_count_union. *) -Theorem sub_count_eqn[compute]: - !n k. sub_count n k = - if k = 0 then { EMPTY } - else if n = 0 then {} - else IMAGE (\s. (n - 1) INSERT s) (sub_count (n - 1) (k - 1)) UNION - sub_count (n - 1) k -Proof - rw[sub_count_n_0, sub_count_0_n] >> - metis_tac[sub_count_union, num_CASES, SUC_SUB1, ADD1] -QED - -(* -> EVAL ``sub_count 3 2``; -val it = |- sub_count 3 2 = {{2; 1}; {2; 0}; {1; 0}}: thm -> EVAL ``sub_count 4 2``; -val it = |- sub_count 4 2 = {{3; 2}; {3; 1}; {3; 0}; {2; 1}; {2; 0}; {1; 0}}: thm -> EVAL ``sub_count 3 3``; -val it = |- sub_count 3 3 = {{2; 1; 0}}: thm -*) - -(* Theorem: n choose 0 = 1 *) -(* Proof: - n choose 0 - = CARD (sub_count n 0) by choose_def - = CARD {{}} by sub_count_n_0 - = 1 by CARD_SING -*) -Theorem choose_n_0: - !n. n choose 0 = 1 -Proof - simp[choose_def, sub_count_n_0] -QED - -(* Theorem: n choose 1 = n *) -(* Proof: - Let s = {{j} | j < n}, - f = \j. {j}. - Then s = IMAGE f (count n) by EXTENSION - Note FINITE (count n) - and INJ f (count n) (POW (count n)) - Thus n choose 1 - = CARD (sub_count n 1) by choose_def - = CARD s by sub_count_n_1 - = CARD (count n) by INJ_CARD_IMAGE - = n by CARD_COUNT -*) -Theorem choose_n_1: - !n. n choose 1 = n -Proof - rw[choose_def, sub_count_n_1] >> - qabbrev_tac `s = {{j} | j < n}` >> - qabbrev_tac `f = \j:num. {j}` >> - `s = IMAGE f (count n)` by fs[EXTENSION, Abbr`f`, Abbr`s`] >> - `CARD (IMAGE f (count n)) = CARD (count n)` suffices_by fs[] >> - irule INJ_CARD_IMAGE >> - rw[] >> - qexists_tac `POW (count n)` >> - rw[INJ_DEF, Abbr`f`] >> - rw[POW_DEF] -QED - -(* Theorem: n choose k = 0 <=> n < k *) -(* Proof: - Note FINITE (sub_count n k) by sub_count_finite - n choose k = 0 - <=> CARD (sub_count n k) = 0 by choose_def - <=> sub_count n k = {} by CARD_EQ_0 - <=> n < k by sub_count_eq_empty -*) -Theorem choose_eq_0: - !n k. n choose k = 0 <=> n < k -Proof - metis_tac[choose_def, sub_count_eq_empty, sub_count_finite, CARD_EQ_0] -QED - -(* Theorem: 0 choose n = if n = 0 then 1 else 0 *) -(* Proof: - 0 choose n - = CARD (sub_count 0 n) by choose_def - = CARD (if n = 0 then {{}} else {}) - by sub_count_0_n - = if n = 0 then 1 else 0 by CARD_SING, CARD_EMPTY -*) -Theorem choose_0_n: - !n. 0 choose n = if n = 0 then 1 else 0 -Proof - rw[choose_def, sub_count_0_n] -QED - -(* Theorem: 1 choose n = if 1 < n then 0 else 1 *) -(* Proof: - If n = 0, 1 choose 0 = 1 by choose_n_0 - If n = 1, 1 choose 1 = 1 by choose_n_1 - Otherwise, 1 choose n = 0 by choose_eq_0, 1 < n -*) -Theorem choose_1_n: - !n. 1 choose n = if 1 < n then 0 else 1 -Proof - rw[choose_eq_0] >> - `n = 0 \/ n = 1` by decide_tac >- - simp[choose_n_0] >> - simp[choose_n_1] -QED - -(* Theorem: n choose n = 1 *) -(* Proof: - n choose n - = CARD (sub_count n n) by choose_def - = CARD {count n} by sub_count_n_n - = 1 by CARD_SING -*) -Theorem choose_n_n: - !n. n choose n = 1 -Proof - simp[choose_def, sub_count_n_n] -QED - -(* Theorem: (n + 1) choose (k + 1) = n choose k + n choose (k + 1) *) -(* Proof: - Let s = sub_count (n + 1) (k + 1), - u = sub_count n k, - v = sub_count n (k + 1), - t = IMAGE (\s. n INSERT s) u. - Then s = t UNION v by sub_count_union - and DISJOINT t v by sub_count_disjoint - and FINITE u /\ FINITE v by sub_count_finite - and FINITE t by IMAGE_FINITE - Thus CARD s = CARD t + CARD v by CARD_UNION_DISJOINT - = CARD u + CARD v by sub_count_insert_card, choose_def -*) -Theorem choose_recurrence: - !n k. (n + 1) choose (k + 1) = n choose k + n choose (k + 1) -Proof - rw[choose_def] >> - qabbrev_tac `s = sub_count (n + 1) (k + 1)` >> - qabbrev_tac `u = sub_count n k` >> - qabbrev_tac `v = sub_count n (k + 1)` >> - qabbrev_tac `t = IMAGE (\s. n INSERT s) u` >> - `s = t UNION v` by rw[sub_count_union, Abbr`s`, Abbr`t`, Abbr`v`] >> - `DISJOINT t v` by metis_tac[sub_count_disjoint] >> - `FINITE u /\ FINITE v` by rw[sub_count_finite, Abbr`u`, Abbr`v`] >> - `FINITE t` by rw[Abbr`t`] >> - `CARD s = CARD t + CARD v` by rw[CARD_UNION_DISJOINT] >> - metis_tac[sub_count_insert_card, choose_def] -QED - -(* This is Pascal's identity: C(n+1,k+1) = C(n,k) + C(n,k+1). *) -(* This corresponds to the 'sum of parents' rule of Pascal's triangle. *) - -(* Theorem: n choose 0 = 1 /\ 0 choose (k + 1) = 0 /\ - (n + 1) choose (k + 1) = n choose k + n choose (k + 1) *) -(* Proof: by choose_n_0, choose_0_n, choose_recurrence. *) -Theorem choose_alt: - !n k. n choose 0 = 1 /\ 0 choose (k + 1) = 0 /\ - (n + 1) choose (k + 1) = n choose k + n choose (k + 1) -Proof - simp[choose_n_0, choose_0_n, choose_recurrence] -QED - -(* Theorem: n choose k = binomial n k *) -(* Proof: by binomial_iff, choose_alt. *) -Theorem choose_eqn[compute]: - !n k. n choose k = binomial n k -Proof - prove_tac[binomial_iff, choose_alt] -QED - -(* -> EVAL ``5 choose 3``; -val it = |- 5 choose 3 = 10: thm -> EVAL ``MAP ($choose 5) [0 .. 5]``; -val it = |- MAP ($choose 5) [0 .. 5] = [1; 5; 10; 10; 5; 1]: thm -*) - -(* ------------------------------------------------------------------------- *) -(* Partition of the set of subsets by bijective equivalence. *) -(* ------------------------------------------------------------------------- *) - -(* Define the set of k-subsets of a set. *) -Definition sub_sets_def[nocompute]: - sub_sets P k = { s | s SUBSET P /\ CARD s = k} -End -(* use [nocompute] as this is not effective for evalutaion. *) - -(* Theorem: s IN sub_sets P k <=> s SUBSET P /\ CARD s = k *) -(* Proof: by sub_sets_def. *) -Theorem sub_sets_element: - !P k s. s IN sub_sets P k <=> s SUBSET P /\ CARD s = k -Proof - simp[sub_sets_def] -QED - -(* Theorem: sub_sets (count n) k = sub_count n k *) -(* Proof: - sub_sets (count n) k - = {s | s SUBSET (count n) /\ CARD s = k} by sub_sets_def - = sub_count n k by sub_count_def -*) -Theorem sub_sets_sub_count: - !n k. sub_sets (count n) k = sub_count n k -Proof - simp[sub_sets_def, sub_count_def] -QED - -(* Theorem: FINITE t /\ s SUBSET t ==> - sub_sets t (CARD s) = equiv_class $=b= (POW t) s *) -(* Proof: - x IN sub_sets t (CARD s) - <=> x SUBSET t /\ CARD s = CARD x by sub_sets_element - <=> x SUBSET t /\ s =b= x by bij_eq_card_eq, SUBSET_FINITE - <=> x IN POW t /\ s =b= x by IN_POW - <=> x IN equiv_class $=b= (POW t) s by equiv_class_element -*) -Theorem sub_sets_equiv_class: - !s t. FINITE t /\ s SUBSET t ==> - sub_sets t (CARD s) = equiv_class $=b= (POW t) s -Proof - rw[sub_sets_def, IN_POW, EXTENSION] >> - metis_tac[bij_eq_card_eq, SUBSET_FINITE] -QED - -(* Theorem: s SUBSET (count n) ==> - sub_count n (CARD s) = equiv_class $=b= (POW (count n)) s *) -(* Proof: - Note FINITE (count n) by FINITE_COUNT - sub_count n (CARD s) - = sub_sets (count n) (CARD s) by sub_sets_sub_count - = equiv_class $=b= (POW t) s by sub_sets_equiv_class -*) -Theorem sub_count_equiv_class: - !n s. s SUBSET (count n) ==> - sub_count n (CARD s) = equiv_class $=b= (POW (count n)) s -Proof - simp[sub_sets_equiv_class, GSYM sub_sets_sub_count] -QED - -(* Theorem: partition $=b= (POW (count n)) = IMAGE (sub_count n) (upto n) *) -(* Proof: - Let R = $=b=, t = count n. - Note CARD t = n by CARD_COUNT - By EXTENSION and LESS_EQ_IFF_LESS_SUC, this is to show: - (1) x IN partition R (POW t) ==> ?k. x = sub_count n k /\ k <= n - Note ?s. s IN POW t /\ - x = equiv_class R (POW t) s by partition_element - Note FINITE t by SUBSET_FINITE - and s SUBSET t by IN_POW - so CARD s <= CARD t = n by CARD_SUBSET - Take k = CARD s. - Then k <= n /\ x = sub_count n k by sub_count_equiv_class - (2) k <= n ==> sub_count n k IN partition R (POW t) - Let s = count k - Then CARD s = k by CARD_COUNT - and s SUBSET t by COUNT_SUBSET, k <= n - so s IN POW t by IN_POW - Now sub_count n k - = equiv_class R (POW t) s by sub_count_equiv_class - ==> sub_count n k IN partition R (POW t) - by partition_element -*) -Theorem count_power_partition: - !n. partition $=b= (POW (count n)) = IMAGE (sub_count n) (upto n) -Proof - rpt strip_tac >> - qabbrev_tac `R = \(s:num -> bool) (t:num -> bool). s =b= t` >> - qabbrev_tac `t = count n` >> - rw[Once EXTENSION, partition_element, GSYM LESS_EQ_IFF_LESS_SUC, EQ_IMP_THM] >| [ - `FINITE t` by rw[Abbr`t`] >> - `x' SUBSET t` by fs[IN_POW] >> - `CARD x' <= n` by metis_tac[CARD_SUBSET, CARD_COUNT] >> - qexists_tac `CARD x'` >> - simp[sub_count_equiv_class, Abbr`R`, Abbr`t`], - qexists_tac `count x'` >> - `(count x') SUBSET t /\ (count x') IN POW t` by metis_tac[COUNT_SUBSET, IN_POW] >> - simp[] >> - qabbrev_tac `s = count x'` >> - `sub_count n (CARD s) = equiv_class R (POW t) s` suffices_by simp[Abbr`s`] >> - simp[sub_count_equiv_class, Abbr`R`, Abbr`t`] - ] -QED - -(* Theorem: INJ (sub_count n) (upto n) univ(:(num -> bool) -> bool) *) -(* Proof: - By INJ_DEF, this is to show: - !x y. x < SUC n /\ y < SUC n /\ sub_count n x = sub_count n y ==> x = y - Let s = count x. - Note x < SUC n <=> x <= n by arithmetic - ==> s SUBSET (count n) by COUNT_SUBSET, x <= n - and CARD s = x by CARD_COUNT - so s IN sub_count n x by sub_count_element - Thus s IN sub_count n y by given, sub_count n x = sub_count n y - ==> CARD s = x = y -*) -Theorem sub_count_count_inj: - !n m. INJ (sub_count n) (upto n) univ(:(num -> bool) -> bool) -Proof - rw[sub_count_def, EXTENSION, INJ_DEF] >> - `(count x) SUBSET (count n)` by rw[COUNT_SUBSET] >> - metis_tac[CARD_COUNT] -QED - -(* Idea: the sum of sizes of equivalence classes gives size of power set. *) - -(* Theorem: SIGMA ($choose n) (upto n) = 2 ** n *) -(* Proof: - Let R = $=b=, t = count n. - Then R equiv_on (POW t) by bij_eq_equiv_on - and FINITE t by FINITE_COUNT - so FINITE (POW t) by FINITE_POW - Thus CARD (POW t) = SIGMA CARD (partition R (POW t)) - by partition_CARD - LHS = CARD (POW t) - = 2 ** CARD t by CARD_POW - = 2 ** n by CARD_COUNT - Note INJ (sub_count n) (upto n) univ by sub_count_count_inj - RHS = SIGMA CARD (partition R (POW t)) - = SIGMA CARD (IMAGE (sub_count n) (upto n)) by count_power_partition - = SIGMA (CARD o sub_count n) (upto n) by SUM_IMAGE_INJ_o - = SIGMA ($choose n) (upto n) by FUN_EQ_THM, choose_def -*) -Theorem choose_sum_over_count: - !n. SIGMA ($choose n) (upto n) = 2 ** n -Proof - rpt strip_tac >> - qabbrev_tac `R = \(s:num -> bool) (t:num -> bool). s =b= t` >> - qabbrev_tac `t = count n` >> - `R equiv_on (POW t)` by rw[bij_eq_equiv_on, Abbr`R`] >> - `FINITE (POW t)` by rw[FINITE_POW, Abbr`t`] >> - imp_res_tac partition_CARD >> - `FINITE (upto n)` by rw[] >> - `SIGMA CARD (partition R (POW t)) = SIGMA CARD (IMAGE (sub_count n) (upto n))` by fs[count_power_partition, Abbr`R`, Abbr`t`] >> - `_ = SIGMA (CARD o (sub_count n)) (upto n)` by rw[SUM_IMAGE_INJ_o, sub_count_count_inj] >> - `_ = SIGMA ($choose n) (upto n)` by rw[choose_def, FUN_EQ_THM, SIGMA_CONG] >> - fs[CARD_POW, Abbr`t`] -QED - -(* This corresponds to: -> binomial_sum; -val it = |- !n. SUM (GENLIST (binomial n) (SUC n)) = 2 ** n: thm -*) - -(* Theorem: SUM (MAP ($choose n) [0 .. n]) = 2 ** n *) -(* Proof: - SUM (MAP ($choose n) [0 .. n]) - = SIGMA ($choose n) (upto n) by SUM_IMAGE_upto - = 2 ** n by choose_sum_over_count -*) -Theorem choose_sum_over_all: - !n. SUM (MAP ($choose n) [0 .. n]) = 2 ** n -Proof - simp[GSYM SUM_IMAGE_upto, choose_sum_over_count] -QED - -(* A better representation of: -> binomial_sum; -val it = |- !n. SUM (GENLIST (binomial n) (SUC n)) = 2 ** n: thm -*) - -(* ------------------------------------------------------------------------- *) -(* Counting number of permutations. *) -(* ------------------------------------------------------------------------- *) - -(* Define the set of permutation tuples of (count n). *) -Definition perm_count_def[nocompute]: - perm_count n = { ls | ALL_DISTINCT ls /\ set ls = count n} -End -(* use [nocompute] as this is not effective for evalutaion. *) - -(* Define the number of choices of k-tuples of (count n). *) -Definition perm_def[nocompute]: - perm n = CARD (perm_count n) -End -(* use [nocompute] as this is not effective for evalutaion. *) - -(* Theorem: ls IN perm_count n <=> ALL_DISTINCT ls /\ set ls = count n *) -(* Proof: by perm_count_def. *) -Theorem perm_count_element: - !ls n. ls IN perm_count n <=> ALL_DISTINCT ls /\ set ls = count n -Proof - simp[perm_count_def] -QED - -(* Theorem: ls IN perm_count n ==> ~MEM n ls *) -(* Proof: - ls IN perm_count n - <=> ALL_DISTINCT ls /\ set ls = count n by perm_count_element - ==> ~MEM n ls by COUNT_NOT_SELF -*) -Theorem perm_count_element_no_self: - !ls n. ls IN perm_count n ==> ~MEM n ls -Proof - simp[perm_count_element] -QED - -(* Theorem: ls IN perm_count n ==> LENGTH ls = n *) -(* Proof: - ls IN perm_count n - <=> ALL_DISTINCT ls /\ set ls = count n by perm_count_element - LENGTH ls = CARD (set ls) by ALL_DISTINCT_CARD_LIST_TO_SET - = CARD (count n) by set ls = count n - = n by CARD_COUNT -*) -Theorem perm_count_element_length: - !ls n. ls IN perm_count n ==> LENGTH ls = n -Proof - metis_tac[perm_count_element, ALL_DISTINCT_CARD_LIST_TO_SET, CARD_COUNT] -QED - -(* Theorem: perm_count n SUBSET necklace n n *) -(* Proof: - ls IN perm_count n - <=> ALL_DISTINCT ls /\ set ls = count n by perm_count_element - Thus set ls SUBSET (count n) by SUBSET_REFL - and LENGTH ls = n by perm_count_element_length - Therefore ls IN necklace n n by necklace_element -*) -Theorem perm_count_subset: - !n. perm_count n SUBSET necklace n n -Proof - rw[perm_count_def, necklace_def, perm_count_element_length, SUBSET_DEF] -QED - -(* Theorem: FINITE (perm_count n) *) -(* Proof: - Note perm_count n SUBSET necklace n n by perm_count_subset - and FINITE (necklace n n) by necklace_finite - Thus FINITE (perm_count n) by SUBSET_FINITE -*) -Theorem perm_count_finite: - !n. FINITE (perm_count n) -Proof - metis_tac[perm_count_subset, necklace_finite, SUBSET_FINITE] -QED - -(* Theorem: perm_count 0 = {[]} *) -(* Proof: - ls IN perm_count 0 - <=> ALL_DISTINCT ls /\ set ls = count 0 by perm_count_element - <=> ALL_DISTINCT ls /\ set ls = {} by COUNT_0 - <=> ALL_DISTINCT ls /\ ls = [] by LIST_TO_SET_EQ_EMPTY - <=> ls = [] by ALL_DISTINCT - Thus perm_count 0 = {[]} by EXTENSION -*) -Theorem perm_count_0: - perm_count 0 = {[]} -Proof - rw[perm_count_def, EXTENSION, EQ_IMP_THM] >> - metis_tac[MEM, list_CASES] -QED - -(* Theorem: perm_count 1 = {[0]} *) -(* Proof: - ls IN perm_count 1 - <=> ALL_DISTINCT ls /\ set ls = count 1 by perm_count_element - <=> ALL_DISTINCT ls /\ set ls = {0} by COUNT_1 - <=> ls = [0] by DISTINCT_LIST_TO_SET_EQ_SING - Thus perm_count 1 = {[0]} by EXTENSION -*) -Theorem perm_count_1: - perm_count 1 = {[0]} -Proof - simp[perm_count_def, COUNT_1, DISTINCT_LIST_TO_SET_EQ_SING] -QED - -(* Define the interleave operation on a list. *) -Definition interleave_def: - interleave x ls = IMAGE (\k. TAKE k ls ++ x::DROP k ls) (upto (LENGTH ls)) -End -(* make this an infix operator *) -val _ = set_fixity "interleave" (Infix(NONASSOC, 550)); (* higher than arithmetic op 500. *) -(* interleave_def; -val it = |- !x ls. x interleave ls = - IMAGE (\k. TAKE k ls ++ x::DROP k ls) (upto (LENGTH ls)): thm *) - -(* -> EVAL ``2 interleave [0; 1]``; -val it = |- 2 interleave [0; 1] = {[0; 1; 2]; [0; 2; 1]; [2; 0; 1]}: thm -*) - -(* Theorem: x interleave ls = {TAKE k ls ++ x::DROP k ls | k | k <= LENGTH ls} *) -(* Proof: by interleave_def, EXTENSION. *) -Theorem interleave_alt: - !ls x. x interleave ls = {TAKE k ls ++ x::DROP k ls | k | k <= LENGTH ls} -Proof - simp[interleave_def, EXTENSION] >> - metis_tac[LESS_EQ_IFF_LESS_SUC] -QED - -(* Theorem: y IN x interleave ls <=> - ?k. k <= LENGTH ls /\ y = TAKE k ls ++ x::DROP k ls *) -(* Proof: by interleave_alt, IN_IMAGE. *) -Theorem interleave_element: - !ls x y. y IN x interleave ls <=> - ?k. k <= LENGTH ls /\ y = TAKE k ls ++ x::DROP k ls -Proof - simp[interleave_alt] >> - metis_tac[] -QED - -(* Theorem: x interleave [] = {[x]} *) -(* Proof: - x interleave [] - = IMAGE (\k. TAKE k [] ++ x::DROP k []) (upto (LENGTH [])) - by interleave_def - = IMAGE (\k. [] ++ x::[]) (upto 0) by TAKE_nil, DROP_nil, LENGTH - = IMAGE (\k. [x]) (count 1) by APPEND, notation of upto - = IMAGE (\k. [x]) {0} by COUNT_1 - = [x] by IMAGE_DEF -*) -Theorem interleave_nil: - !x. x interleave [] = {[x]} -Proof - rw[interleave_def, EXTENSION] >> - metis_tac[DECIDE``0 < 1``] -QED - -(* Theorem: y IN (x interleave ls) ==> LENGTH y = 1 + LENGTH ls *) -(* Proof: - LENGTH y - = LENGTH (TAKE k ls ++ x::DROP k ls) by interleave_element, for some k - = LENGTH (TAKE k ls) + LENGTH (x::DROP k ls) by LENGTH_APPEND - = k + LENGTH (x :: DROP k ls) by LENGTH_TAKE, k <= LENGTH ls - = k + (1 + LENGTH (DROP k ls)) by LENGTH - = k + (1 + (LENGTH ls - k)) by LENGTH_DROP - = 1 + LENGTH ls by arithmetic, k <= LENGTH ls -*) -Theorem interleave_length: - !ls x y. y IN (x interleave ls) ==> LENGTH y = 1 + LENGTH ls -Proof - rw_tac bool_ss[interleave_element] >> - simp[] -QED - -(* Theorem: ALL_DISTINCT (x::ls) /\ y IN (x interleave ls) ==> ALL_DISTINCT y *) -(* Proof: - By interleave_def, IN_IMAGE, this is to show; - ALL_DISTINCT (TAKE k ls ++ x::DROP k ls) - To apply ALL_DISTINCT_APPEND, need to show: - (1) ~MEM x ls /\ MEM e (TAKE k ls) /\ MEM e (x::DROP k ls) ==> F - MEM e (x::DROP k ls) - <=> e = x \/ MEM e (DROP k ls) by MEM - MEM e (TAKE k ls) - ==> MEM e ls by MEM_TAKE - If e = x, - this contradicts ~MEM x ls. - If MEM e (DROP k ls), - with MEM e (TAKE k ls) - and ALL_DISTINCT ls gives F by ALL_DISTINCT_TAKE_DROP - (2) ALL_DISTINCT (TAKE k ls), true by ALL_DISTINCT_TAKE - (3) ~MEM x ls ==> ALL_DISTINCT (x::DROP k ls) - ALL_DISTINCT (x::DROP k ls) - <=> ~MEM x (DROP k ls) /\ - ALL_DISTINCT (DROP k ls) by ALL_DISTINCT - <=> ~MEM x (DROP k ls) /\ T by ALL_DISTINCT_DROP - ==> ~MEM x ls /\ T by MEM_DROP_IMP - ==> T /\ T = T -*) -Theorem interleave_distinct: - !ls x y. ALL_DISTINCT (x::ls) /\ y IN (x interleave ls) ==> ALL_DISTINCT y -Proof - rw_tac bool_ss[interleave_def, IN_IMAGE] >> - irule (ALL_DISTINCT_APPEND |> SPEC_ALL |> #2 o EQ_IMP_RULE) >> - rpt strip_tac >| [ - fs[] >- - metis_tac[MEM_TAKE] >> - metis_tac[ALL_DISTINCT_TAKE_DROP], - fs[ALL_DISTINCT_TAKE], - fs[ALL_DISTINCT_DROP] >> - metis_tac[MEM_DROP_IMP] - ] -QED - -(* Theorem: ALL_DISTINCT ls /\ ~(MEM x ls) /\ - y IN (x interleave ls) ==> ALL_DISTINCT y *) -(* Proof: by interleave_distinct, ALL_DISTINCT. *) -Theorem interleave_distinct_alt: - !ls x y. ALL_DISTINCT ls /\ ~(MEM x ls) /\ - y IN (x interleave ls) ==> ALL_DISTINCT y -Proof - metis_tac[interleave_distinct, ALL_DISTINCT] -QED - -(* Theorem: y IN x interleave ls ==> set y = set (x::ls) *) -(* Proof: - Note y = TAKE k ls ++ x::DROP k ls by interleave_element, for some k - Let u = TAKE k ls, v = DROP k ls. - set y - = set (u ++ x::v) by above - = set u UNION set (x::v) by LIST_TO_SET_APPEND - = set u UNION (x INSERT set v) by LIST_TO_SET - = (x INSERT set v) UNION set u by UNION_COMM - = x INSERT (set v UNION set u) by INSERT_UNION_EQ - = x INSERT (set u UNION set v) by UNION_COMM - = x INSERT (set (u ++ v)) by LIST_TO_SET_APPEND - = x INSERT set ls by TAKE_DROP - = set (x::ls) by LIST_TO_SET -*) -Theorem interleave_set: - !ls x y. y IN x interleave ls ==> set y = set (x::ls) -Proof - rw_tac bool_ss[interleave_element] >> - qabbrev_tac `u = TAKE k ls` >> - qabbrev_tac `v = DROP k ls` >> - `set (u ++ x::v) = set u UNION set (x::v)` by rw[] >> - `_ = set u UNION (x INSERT set v)` by rw[] >> - `_ = (x INSERT set v) UNION set u` by rw[UNION_COMM] >> - `_ = x INSERT (set v UNION set u)` by rw[INSERT_UNION_EQ] >> - `_ = x INSERT (set u UNION set v)` by rw[UNION_COMM] >> - `_ = x INSERT (set (u ++ v))` by rw[] >> - `_ = x INSERT set ls` by metis_tac[TAKE_DROP] >> - simp[] -QED - -(* Theorem: y IN x interleave ls ==> set y = x INSERT set ls *) -(* Proof: - Note set y = set (x::ls) by interleave_set - = x INSERT set ls by LIST_TO_SET -*) -Theorem interleave_set_alt: - !ls x y. y IN x interleave ls ==> set y = x INSERT set ls -Proof - metis_tac[interleave_set, LIST_TO_SET] -QED - -(* Theorem: (x::ls) IN x interleave ls *) -(* Proof: - (x::ls) IN x interleave ls - <=> ?k. x::ls = TAKE k ls ++ [x] ++ DROP k ls /\ k < SUC (LENGTH ls) - by interleave_def - Take k = 0. - Then 0 < SUC (LENGTH ls) by SUC_POS - and TAKE 0 ls ++ [x] ++ DROP 0 ls - = [] ++ [x] ++ ls by TAKE_0, DROP_0 - = x::ls by APPEND -*) -Theorem interleave_has_cons: - !ls x. (x::ls) IN x interleave ls -Proof - rw[interleave_def] >> - qexists_tac `0` >> - simp[] -QED - -(* Theorem: x interleave ls <> EMPTY *) -(* Proof: - Note (x::ls) IN x interleave ls by interleave_has_cons - Thus x interleave ls <> {} by MEMBER_NOT_EMPTY -*) -Theorem interleave_not_empty: - !ls x. x interleave ls <> EMPTY -Proof - metis_tac[interleave_has_cons, MEMBER_NOT_EMPTY] -QED - -(* -MEM_APPEND_lemma -|- !a b c d x. a ++ [x] ++ b = c ++ [x] ++ d /\ ~MEM x b /\ ~MEM x a ==> - a = c /\ b = d -*) - -(* Theorem: ~MEM n x /\ ~MEM n y ==> (n interleave x = n interleave y <=> x = y) *) -(* Proof: - Let f = (\k. TAKE k x ++ n::DROP k x), - g = (\k. TAKE k y ++ n::DROP k y). - By interleave_def, this is to show: - IMAGE f (upto (LENGTH x)) = IMAGE g (upto (LENGTH y)) <=> x = y - Only-part part is trivial. - For the if part, - Note 0 IN (upto (LENGTH x) by SUC_POS, IN_COUNT - so f 0 IN IMAGE f (upto (LENGTH x)) - thus ?k. k < SUC (LENGTH y) /\ f 0 = g k by IN_IMAGE, IN_COUNT - so n::x = TAKE k y ++ [n] ++ DROP k y by notation of f 0 - but n::x = TAKE 0 x ++ [n] ++ DROP 0 x by TAKE_0, DROP_0 - and ~MEM n (TAKE 0 x) /\ ~MEM n (DROP 0 x) by TAKE_0, DROP_0 - so TAKE 0 x = TAKE k y /\ - DROP 0 x = DROP k y by MEM_APPEND_lemma - or x = y by TAKE_DROP -*) -Theorem interleave_eq: - !n x y. ~MEM n x /\ ~MEM n y ==> (n interleave x = n interleave y <=> x = y) -Proof - rw[interleave_def, EQ_IMP_THM] >> - qabbrev_tac `f = \k. TAKE k x ++ n::DROP k x` >> - qabbrev_tac `g = \k. TAKE k y ++ n::DROP k y` >> - `f 0 IN IMAGE f (upto (LENGTH x))` by fs[] >> - `?k. k < SUC (LENGTH y) /\ f 0 = g k` by metis_tac[IN_IMAGE, IN_COUNT] >> - fs[Abbr`f`, Abbr`g`] >> - `n::x = TAKE 0 x ++ [n] ++ DROP 0 x` by rw[] >> - `~MEM n (TAKE 0 x) /\ ~MEM n (DROP 0 x)` by rw[] >> - metis_tac[MEM_APPEND_lemma, TAKE_DROP] -QED - -(* Theorem: ~MEM x l1 /\ l1 <> l2 ==> DISJOINT (x interleave l1) (x interleave l2) *) -(* Proof: - Use DISJOINT_DEF, by contradiction, suppose y is in both. - Then ?k h. k <= LENGTH l1 and h <= LENGTH l2 - with y = TAKE k l1 ++ [x] ++ DROP k l1 by interleave_element - and y = TAKE h l2 ++ [x] ++ DROP h l2 by interleave_element - Now ~MEM x (TAKE k l1) by MEM_TAKE - and ~MEM x (DROP k l1) by MEM_DROP_IMP - Thus TAKE k l1 = TAKE h l2 /\ - DROP k l1 = DROP h l2 by MEM_APPEND_lemma - or l1 = l2 by TAKE_DROP - but this contradicts l1 <> l2. -*) -Theorem interleave_disjoint: - !l1 l2 x. ~MEM x l1 /\ l1 <> l2 ==> DISJOINT (x interleave l1) (x interleave l2) -Proof - rw[interleave_def, DISJOINT_DEF, EXTENSION] >> - spose_not_then strip_assume_tac >> - `~MEM x (TAKE k l1) /\ ~MEM x (DROP k l1)` by metis_tac[MEM_TAKE, MEM_DROP_IMP] >> - metis_tac[MEM_APPEND_lemma, TAKE_DROP] -QED - -(* Theorem: FINITE (x interleave ls) *) -(* Proof: - Let f = (\k. TAKE k ls ++ x::DROP k ls), - n = LENGTH ls. - FINITE (x interleave ls) - <=> FINITE (IMAGE f (upto n)) by interleave_def - <=> T by IMAGE_FINITE, FINITE_COUNT -*) -Theorem interleave_finite: - !ls x. FINITE (x interleave ls) -Proof - simp[interleave_def, IMAGE_FINITE] -QED - -(* Theorem: ~MEM x ls ==> - INJ (\k. TAKE k ls ++ x::DROP k ls) (upto (LENGTH ls)) univ(:'a list) *) -(* Proof: - Let n = LENGTH ls, - s = upto n, - f = (\k. TAKE k ls ++ x::DROP k ls). - By INJ_DEF, this is to show: - (1) k IN s ==> f k IN univ(:'a list), true by types. - (2) k IN s /\ h IN s /\ f k = f h ==> k = h. - Note k <= LENGTH ls by IN_COUNT, k IN s - and h <= LENGTH ls by IN_COUNT, h IN s - and ls = TAKE k ls ++ DROP k ls by TAKE_DROP - so ~MEM x (TAKE k ls) /\ - ~MEM x (DROP k ls) by MEM_APPEND, ~MEM x ls - Thus TAKE k ls = TAKE h ls by MEM_APPEND_lemma - ==> k = h by LENGTH_TAKE - -MEM_APPEND_lemma -|- !a b c d x. a ++ [x] ++ b = c ++ [x] ++ d /\ - ~MEM x b /\ ~MEM x a ==> a = c /\ b = d -*) -Theorem interleave_count_inj: - !ls x. ~MEM x ls ==> - INJ (\k. TAKE k ls ++ x::DROP k ls) (upto (LENGTH ls)) univ(:'a list) -Proof - rw[INJ_DEF] >> - `k <= LENGTH ls /\ k' <= LENGTH ls` by fs[] >> - `~MEM x (TAKE k ls) /\ ~MEM x (DROP k ls)` by metis_tac[TAKE_DROP, MEM_APPEND] >> - metis_tac[MEM_APPEND_lemma, LENGTH_TAKE] -QED - -(* Theorem: ~MEM x ls ==> CARD (x interleave ls) = 1 + LENGTH ls *) -(* Proof: - Let f = (\k. TAKE k ls ++ x::DROP k ls), - n = LENGTH ls. - Note FINITE (upto n) by FINITE_COUNT - and INJ f (upto n) univ(:'a list) - by interleave_count_inj, ~MEM x ls - CARD (x interleave ls) - = CARD (IMAGE f (upto n)) by interleave_def - = CARD (upto n) by INJ_CARD_IMAGE - = SUC n = 1 + n by CARD_COUNT, ADD1 -*) -Theorem interleave_card: - !ls x. ~MEM x ls ==> CARD (x interleave ls) = 1 + LENGTH ls -Proof - rw[interleave_def] >> - imp_res_tac interleave_count_inj >> - qabbrev_tac `n = LENGTH ls` >> - qabbrev_tac `s = upto n` >> - qabbrev_tac `f = (\k. TAKE k ls ++ x::DROP k ls)` >> - `FINITE s` by rw[Abbr`s`] >> - metis_tac[INJ_CARD_IMAGE, CARD_COUNT, ADD1] -QED - -(* Note: - interleave_distinct, interleave_length, and interleave_set - are effects after interleave. Now we need a kind of inverse: - deduce the effects before interleave. -*) - -(* Idea: a member h in a distinct list is the interleave of h with a smaller one. *) - -(* Theorem: ALL_DISTINCT ls /\ h IN set ls ==> - ?t. ALL_DISTINCT t /\ ls IN h interleave t /\ set t = (set ls) DELETE h *) -(* Proof: - By induction on ls. - Base: ALL_DISTINCT [] /\ MEM h [] ==> ?t. ... - Since MEM h [] = F, this is true by MEM - Step: (ALL_DISTINCT ls /\ MEM h ls ==> - ?t. ALL_DISTINCT t /\ ls IN h interleave t /\ set t = set ls DELETE h) ==> - !h'. ALL_DISTINCT (h'::ls) /\ MEM h (h'::ls) ==> - ?t. ALL_DISTINCT t /\ h'::ls IN h interleave t /\ set t = set (h'::ls) DELETE h - If h' = h, - Note ~MEM h ls /\ ALL_DISTINCT ls by ALL_DISTINCT - Take this ls, - Then set (h::ls) DELETE h - = (h INSERT set ls) DELETE h by LIST_TO_SET - = set ls by INSERT_DELETE_NON_ELEMENT - and h::ls IN h interleave ls by interleave_element, take k = 0. - If h' <> h, - Note ~MEM h' ls /\ ALL_DISTINCT ls by ALL_DISTINCT - and MEM h ls by MEM, h <> h' - Thus ?t. ALL_DISTINCT t /\ - ls IN h interleave t /\ - set t = set ls DELETE h by induction hypothesis - Note ~MEM h' t by set t = set ls DELETE h, ~MEM h' ls - Take this (h'::t), - Then ALL_DISTINCT (h'::t) by ALL_DISTINCT, ~MEM h' t - and set (h'::ls) DELETE h - = (h' INSERT set ls) DELETE h by LIST_TO_SET - = h' INSERT (set ls DELETE h) by DELETE_INSERT, h' <> h - = h' INSERT set t by above - = set (h'::t) - and h'::ls IN h interleave t by interleave_element, - take k = SUC k from ls IN h interleave t -*) -Theorem interleave_revert: - !ls h. ALL_DISTINCT ls /\ h IN set ls ==> - ?t. ALL_DISTINCT t /\ ls IN h interleave t /\ set t = (set ls) DELETE h -Proof - rpt strip_tac >> - Induct_on `ls` >- - simp[] >> - rpt strip_tac >> - Cases_on `h' = h` >| [ - fs[] >> - qexists_tac `ls` >> - simp[INSERT_DELETE_NON_ELEMENT] >> - simp[interleave_element] >> - qexists_tac `0` >> - simp[], - fs[] >> - `~MEM h' t` by fs[] >> - qexists_tac `h'::t` >> - simp[DELETE_INSERT] >> - fs[interleave_element] >> - qexists_tac `SUC k` >> - simp[] - ] -QED - -(* A useful corollary for set s = count n. *) - -(* Theorem: ALL_DISTINCT ls /\ set ls = upto n ==> - ?t. ALL_DISTINCT t /\ ls IN n interleave t /\ set t = count n *) -(* Proof: - Note MEM n ls by set ls = upto n - so ?t. ALL_DISTINCT t /\ - ls IN n interleave t /\ - set t = set ls DELETE n by interleave_revert - = (upto n) DELETE n by given - = count n by upto_delete -*) -Theorem interleave_revert_count: - !ls n. ALL_DISTINCT ls /\ set ls = upto n ==> - ?t. ALL_DISTINCT t /\ ls IN n interleave t /\ set t = count n -Proof - rpt strip_tac >> - `MEM n ls` by fs[] >> - drule_then strip_assume_tac interleave_revert >> - first_x_assum (qspec_then `n` strip_assume_tac) >> - metis_tac[upto_delete] -QED - -(* Theorem: perm_count (SUC n) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) *) -(* Proof: - By induction on n. - Base: perm_count (SUC 0) = - BIGUNION (IMAGE ($interleave 0) (perm_count 0)) - LHS = perm_count (SUC 0) - = perm_count 1 by ONE - = {[0]} by perm_count_1 - RHS = BIGUNION (IMAGE ($interleave 0) (perm_count 0)) - = BIGUNION (IMAGE ($interleave 0) {[]} by perm_count_0 - = BIGUNION {0 interleave []} by IMAGE_SING - = BIGUNION {{[0]}} by interleave_nil - = {[0]} = LHS by BIGUNION_SING - Step: perm_count (SUC n) = BIGUNION (IMAGE ($interleave n) (perm_count n)) ==> - perm_count (SUC (SUC n)) = - BIGUNION (IMAGE ($interleave (SUC n)) (perm_count (SUC n))) - Let f = $interleave (SUC n), - s = perm_count n, t = perm_count (SUC n). - y IN BIGUNION (IMAGE f t) - <=> ?x. x IN t /\ y IN f x by IN_BIGUNION_IMAGE - <=> ?x. (?z. z IN s /\ x IN n interleave z) /\ y IN (SUC n) interleave x - by IN_BIGUNION_IMAGE, induction hypothesis - <=> ?x z. ALL_DISTINCT z /\ set z = count n /\ - x IN n interleave z /\ - y IN (SUC n) interleave x by perm_count_element - If part: y IN perm_count (SUC (SUC n)) ==> ?x and z. - Note ALL_DISTINCT y /\ - set y = count (SUC (SUC n)) by perm_count_element - Then ?x. ALL_DISTINCT x /\ y IN (SUC n) interleave x /\ set x = upto n - by interleave_revert_count - so ?z. ALL_DISTINCT z /\ x IN n interleave z /\ set z = count n - by interleave_revert_count - Take these x and z. - Only-if part: ?x and z ==> y IN perm_count (SUC (SUC n)) - Note ~MEM n z by set z = count n, COUNT_NOT_SELF - ==> ALL_DISTINCT x /\ by interleave_distinct_alt - set x = upto n by interleave_set_alt, COUNT_SUC - Note ~MEM (SUC n) x by set x = upto n, COUNT_NOT_SELF - ==> ALL_DISTINCT y /\ by interleave_distinct_alt - set y = count (SUC (SUC n)) by interleave_set_alt, COUNT_SUC - ==> y IN perm_count (SUC (SUC n)) by perm_count_element -*) -Theorem perm_count_suc: - !n. perm_count (SUC n) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) -Proof - Induct >| [ - rw[perm_count_0, perm_count_1] >> - simp[interleave_nil], - rw[IN_BIGUNION_IMAGE, EXTENSION, EQ_IMP_THM] >| [ - imp_res_tac perm_count_element >> - `?y. ALL_DISTINCT y /\ x IN (SUC n) interleave y /\ set y = upto n` by rw[interleave_revert_count] >> - `?t. ALL_DISTINCT t /\ y IN n interleave t /\ set t = count n` by rw[interleave_revert_count] >> - (qexists_tac `y` >> simp[]) >> - (qexists_tac `t` >> simp[]) >> - simp[perm_count_element], - fs[perm_count_element] >> - `~MEM n x''` by fs[] >> - `ALL_DISTINCT x' /\ set x' = upto n` by metis_tac[interleave_distinct_alt, interleave_set_alt, COUNT_SUC] >> - `~MEM (SUC n) x'` by fs[] >> - metis_tac[interleave_distinct_alt, interleave_set_alt, COUNT_SUC] - ] - ] -QED - -(* Theorem: perm_count (n + 1) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) *) -(* Proof: by perm_count_suc, GSYM ADD1. *) -Theorem perm_count_suc_alt: - !n. perm_count (n + 1) = - BIGUNION (IMAGE ($interleave n) (perm_count n)) -Proof - simp[perm_count_suc, GSYM ADD1] -QED - -(* Theorem: perm_count n = - if n = 0 then {[]} - else BIGUNION (IMAGE ($interleave (n - 1)) (perm_count (n - 1))) *) -(* Proof: by perm_count_0, perm_count_suc. *) -Theorem perm_count_eqn[compute]: - !n. perm_count n = - if n = 0 then {[]} - else BIGUNION (IMAGE ($interleave (n - 1)) (perm_count (n - 1))) -Proof - rw[perm_count_0] >> - metis_tac[perm_count_suc, num_CASES, SUC_SUB1] -QED - -(* -> EVAL ``perm_count 3``; -val it = |- perm_count 3 = -{[0; 1; 2]; [0; 2; 1]; [2; 0; 1]; [1; 0; 2]; [1; 2; 0]; [2; 1; 0]}: thm -*) - -(* Historical note. -This use of interleave to list all permutations is called -the Steinhaus–Johnson–Trotter algorithm, due to re-discovery by various people. -Outside mathematics, this method was known already to 17th-century English change ringers. -Equivalently, this algorithm finds a Hamiltonian cycle in the permutohedron. - -Steinhaus–Johnson–Trotter algorithm -https://en.wikipedia.org/wiki/Steinhaus–Johnson–Trotter_algorithm - -1677 A book by Fabian Stedman lists the solutions for up to six bells. -1958 A book by Steinhaus describes a related puzzle of generating all permutations by a system of particles. -Selmer M. Johnson and Hale F. Trotter discovered the algorithm independently of each other in the early 1960s. -1962 Hale F. Trotter, "Algorithm 115: Perm", August 1962. -1963 Selmer M. Johnson, "Generation of permutations by adjacent transposition". - -*) - -(* Theorem: perm 0 = 1 *) -(* Proof: - perm 0 - = CARD (perm_count 0) by perm_def - = CARD {[]} by perm_count_0 - = 1 by CARD_SING -*) -Theorem perm_0: - perm 0 = 1 -Proof - simp[perm_def, perm_count_0] -QED - -(* Theorem: perm 1 = 1 *) -(* Proof: - perm 1 - = CARD (perm_count 1) by perm_def - = CARD {[0]} by perm_count_1 - = 1 by CARD_SING -*) -Theorem perm_1: - perm 1 = 1 -Proof - simp[perm_def, perm_count_1] -QED - -(* Theorem: e IN IMAGE ($interleave n) (perm_count n) ==> FINITE e *) -(* Proof: - e IN IMAGE ($interleave n) (perm_count n) - <=> ?ls. ls IN perm_count n /\ - e = n interleave ls by IN_IMAGE - Thus FINITE e by interleave_finite -*) -Theorem perm_count_interleave_finite: - !n e. e IN IMAGE ($interleave n) (perm_count n) ==> FINITE e -Proof - rw[] >> - simp[interleave_finite] -QED - -(* Theorem: e IN IMAGE ($interleave n) (perm_count n) ==> CARD e = n + 1 *) -(* Proof: - e IN IMAGE ($interleave n) (perm_count n) - <=> ?ls. ls IN perm_count n /\ - e = n interleave ls by IN_IMAGE - Note ~MEM n ls by perm_count_element_no_self - and LENGTH ls = n by perm_count_element_length - Thus CARD e = n + 1 by interleave_card, ~MEM n ls -*) -Theorem perm_count_interleave_card: - !n e. e IN IMAGE ($interleave n) (perm_count n) ==> CARD e = n + 1 -Proof - rw[] >> - `~MEM n x` by rw[perm_count_element_no_self] >> - `LENGTH x = n` by rw[perm_count_element_length] >> - simp[interleave_card] -QED - -(* Theorem: PAIR_DISJOINT (IMAGE ($interleave n) (perm_count n)) *) -(* Proof: - By IN_IMAGE, this is to show: - x IN perm_count n /\ y IN perm_count n /\ - n interleave x <> n interleave y ==> - DISJOINT (n interleave x) (n interleave y) - By contradiction, suppose there is a list ls in both. - Then x = y by interleave_disjoint - This contradicts n interleave x <> n interleave y. -*) -Theorem perm_count_interleave_disjoint: - !n e. PAIR_DISJOINT (IMAGE ($interleave n) (perm_count n)) -Proof - rw[perm_count_def] >> - `~MEM n x` by fs[] >> - metis_tac[interleave_disjoint] -QED - -(* Theorem: INJ ($interleave n) (perm_count n) univ(:(num list -> bool)) *) -(* Proof: - By INJ_DEF, this is to show: - (1) x IN perm_count n ==> n interleave x IN univ - This is true by type. - (2) x IN perm_count n /\ y IN perm_count n /\ - n interleave x = n interleave y ==> x = y - Note ~MEM n x by perm_count_element_no_self - and ~MEM n y by perm_count_element_no_self - Thus x = y by interleave_eq -*) -Theorem perm_count_interleave_inj: - !n. INJ ($interleave n) (perm_count n) univ(:(num list -> bool)) -Proof - rw[INJ_DEF, perm_count_def, interleave_eq] -QED - -(* Theorem: perm (SUC n) = (SUC n) * perm n *) -(* Proof: - Let f = $interleave n, - s = IMAGE f (perm_count n). - Note FINITE (perm_count n) by perm_count_finite - so FINITE s by IMAGE_FINITE - and !e. e IN s ==> - FINITE e /\ by perm_count_interleave_finite - CARD e = n + 1 by perm_count_interleave_card - and PAIR_DISJOINT s by perm_count_interleave_disjoint - and INJ f (perm_count n) univ(:(num list -> bool)) - by perm_count_interleave_inj - perm (SUC n) - = CARD (perm_count (SUC n)) by perm_def - = CARD (BIGUNION s) by perm_count_suc - = CARD s * (n + 1) by CARD_BIGUNION_SAME_SIZED_SETS - = CARD (perm_count n) * (n + 1) by INJ_CARD_IMAGE - = perm n * (n + 1) by perm_def - = (SUC n) * perm n by MULT_COMM, ADD1 -*) -Theorem perm_suc: - !n. perm (SUC n) = (SUC n) * perm n -Proof - rpt strip_tac >> - qabbrev_tac `f = $interleave n` >> - qabbrev_tac `s = IMAGE f (perm_count n)` >> - `FINITE (perm_count n)` by rw[perm_count_finite] >> - `FINITE s` by rw[Abbr`s`] >> - `!e. e IN s ==> FINITE e /\ CARD e = n + 1` - by metis_tac[perm_count_interleave_finite, perm_count_interleave_card] >> - `PAIR_DISJOINT s` by metis_tac[perm_count_interleave_disjoint] >> - `INJ f (perm_count n) univ(:(num list -> bool))` by rw[perm_count_interleave_inj, Abbr`f`] >> - simp[perm_def] >> - `CARD (perm_count (SUC n)) = CARD (BIGUNION s)` by rw[perm_count_suc, Abbr`s`, Abbr`f`] >> - `_ = CARD s * (n + 1)` by rw[CARD_BIGUNION_SAME_SIZED_SETS] >> - `_ = CARD (perm_count n) * (n + 1)` by metis_tac[INJ_CARD_IMAGE] >> - simp[ADD1] -QED - -(* Theorem: perm (n + 1) = (n + 1) * perm n *) -(* Proof: by perm_suc, ADD1 *) -Theorem perm_suc_alt: - !n. perm (n + 1) = (n + 1) * perm n -Proof - simp[perm_suc, GSYM ADD1] -QED - -(* Theorem: perm 0 = 1 /\ !n. perm (n + 1) = (n + 1) * perm n *) -(* Proof: by perm_0, perm_suc_alt *) -Theorem perm_alt: - perm 0 = 1 /\ !n. perm (n + 1) = (n + 1) * perm n -Proof - simp[perm_0, perm_suc_alt] -QED - -(* Theorem: perm n = FACT n *) -(* Proof: by FACT_iff, perm_alt. *) -Theorem perm_eq_fact[compute]: - !n. perm n = FACT n -Proof - metis_tac[FACT_iff, perm_alt, ADD1] -QED - -(* This is fantastic! *) - -(* -> EVAL ``perm 3``; = 6 -> EVAL ``MAP perm [0 .. 10]``; = -[1; 1; 2; 6; 24; 120; 720; 5040; 40320; 362880; 3628800] -*) - -(* ------------------------------------------------------------------------- *) -(* Permutations of a set. *) -(* ------------------------------------------------------------------------- *) - -(* Note: SET_TO_LIST, using CHOICE and REST, is not effective for computations. -SET_TO_LIST_THM -|- FINITE s ==> - SET_TO_LIST s = if s = {} then [] else CHOICE s::SET_TO_LIST (REST s) -*) - -(* Define the set of permutation lists of a set. *) -Definition perm_set_def[nocompute]: - perm_set s = {ls | ALL_DISTINCT ls /\ set ls = s} -End -(* use [nocompute] as this is not effective for evalutaion. *) -(* Note: this cannot be made effective, unless sort s to list by some ordering. *) - -(* Theorem: ls IN perm_set s <=> ALL_DISTINCT ls /\ set ls = s *) -(* Proof: perm_set_def *) -Theorem perm_set_element: - !ls s. ls IN perm_set s <=> ALL_DISTINCT ls /\ set ls = s -Proof - simp[perm_set_def] -QED - -(* Theorem: perm_set (count n) = perm_count n *) -(* Proof: by perm_count_def, perm_set_def. *) -Theorem perm_set_perm_count: - !n. perm_set (count n) = perm_count n -Proof - simp[perm_count_def, perm_set_def] -QED - -(* Theorem: perm_set {} = {[]} *) -(* Proof: - perm_set {} - = {ls | ALL_DISTINCT ls /\ set ls = {}} by perm_set_def - = {ls | ALL_DISTINCT ls /\ ls = []} by LIST_TO_SET_EQ_EMPTY - = {[]} by ALL_DISTINCT -*) -Theorem perm_set_empty: - perm_set {} = {[]} -Proof - rw[perm_set_def, EXTENSION] >> - metis_tac[ALL_DISTINCT] -QED - -(* Theorem: perm_set {x} = {[x]} *) -(* Proof: - perm_set {x} - = {ls | ALL_DISTINCT ls /\ set ls = {x}} by perm_set_def - = {ls | ls = [x]} by DISTINCT_LIST_TO_SET_EQ_SING - = {[x]} by notation -*) -Theorem perm_set_sing: - !x. perm_set {x} = {[x]} -Proof - simp[perm_set_def, DISTINCT_LIST_TO_SET_EQ_SING] -QED - -(* Theorem: perm_set s = {[]} <=> s = {} *) -(* Proof: - If part: perm_set s = {[]} ==> s = {} - By contradiction, suppose s <> {}. - ls IN perm_set s - <=> ALL_DISTINCT ls /\ set ls = s by perm_set_element - ==> ls <> [] by LIST_TO_SET_EQ_EMPTY - This contradicts perm_set s = {[]} by IN_SING - Only-if part: s = {} ==> perm_set s = {[]} - This is true by perm_set_empty -*) -Theorem perm_set_eq_empty_sing: - !s. perm_set s = {[]} <=> s = {} -Proof - rw[perm_set_empty, EQ_IMP_THM] >> - `[] IN perm_set s` by fs[] >> - fs[perm_set_element] -QED - -(* Theorem: FINITE s ==> (SET_TO_LIST s) IN perm_set s *) -(* Proof: - Let ls = SET_TO_LIST s. - Note ALL_DISTINCT ls by ALL_DISTINCT_SET_TO_LIST - and set ls = s by SET_TO_LIST_INV - Thus ls IN perm_set s by perm_set_element -*) -Theorem perm_set_has_self_list: - !s. FINITE s ==> (SET_TO_LIST s) IN perm_set s -Proof - simp[perm_set_element, ALL_DISTINCT_SET_TO_LIST, SET_TO_LIST_INV] -QED - -(* Theorem: FINITE s ==> perm_set s <> {} *) -(* Proof: - Let ls = SET_TO_LIST s. - Then ls IN perm_set s by perm_set_has_self_list - Thus perm_set s <> {} by MEMBER_NOT_EMPTY -*) -Theorem perm_set_not_empty: - !s. FINITE s ==> perm_set s <> {} -Proof - metis_tac[perm_set_has_self_list, MEMBER_NOT_EMPTY] -QED - -(* Theorem: perm_set (set ls) <> {} *) -(* Proof: - Note FINITE (set ls) by FINITE_LIST_TO_SET - so perm_set (set ls) <> {} by perm_set_not_empty -*) -Theorem perm_set_list_not_empty: - !ls. perm_set (set ls) <> {} -Proof - simp[FINITE_LIST_TO_SET, perm_set_not_empty] -QED - -(* Theorem: ls IN perm_set s /\ BIJ f s (count n) ==> MAP f ls IN perm_count n *) -(* Proof: - By perm_set_def, perm_count_def, this is to show: - (1) ALL_DISTINCT ls /\ BIJ f (set ls) (count n) ==> ALL_DISTINCT (MAP f ls) - Note INJ f (set ls) (count n) by BIJ_DEF - so ALL_DISTINCT (MAP f ls) by ALL_DISTINCT_MAP_INJ, INJ_DEF - (2) ALL_DISTINCT ls /\ BIJ f (set ls) (count n) ==> set (MAP f ls) = count n - Note SURJ f (set ls) (count n) by BIJ_DEF - so set (MAP f ls) - = IMAGE f (set ls) by LIST_TO_SET_MAP - = count n by IMAGE_SURJ -*) -Theorem perm_set_map_element: - !ls f s n. ls IN perm_set s /\ BIJ f s (count n) ==> MAP f ls IN perm_count n -Proof - rw[perm_set_def, perm_count_def] >- - metis_tac[ALL_DISTINCT_MAP_INJ, BIJ_IS_INJ] >> - simp[LIST_TO_SET_MAP] >> - fs[IMAGE_SURJ, BIJ_DEF] -QED - -(* Theorem: BIJ f s (count n) ==> - INJ (MAP f) (perm_set s) (perm_count n) *) -(* Proof: - By INJ_DEF, this is to show: - (1) x IN perm_set s ==> MAP f x IN perm_count n - This is true by perm_set_map_element - (2) x IN perm_set s /\ y IN perm_set s /\ MAP f x = MAP f y ==> x = y - Note LENGTH x = LENGTH y by LENGTH_MAP - By LIST_EQ, it remains to show: - !j. j < LENGTH x ==> EL j x = EL j y - Note EL j x IN s by perm_set_element, MEM_EL - and EL j y IN s by perm_set_element, MEM_EL - MAP f x = MAP f y - ==> EL j (MAP f x) = EL j (MAP f y) - ==> f (EL j x) = f (EL j y) by EL_MAP - ==> EL j x = EL j y by BIJ_IS_INJ -*) -Theorem perm_set_map_inj: - !f s n. BIJ f s (count n) ==> - INJ (MAP f) (perm_set s) (perm_count n) -Proof - rw[INJ_DEF] >- - metis_tac[perm_set_map_element] >> - irule LIST_EQ >> - `LENGTH x = LENGTH y` by metis_tac[LENGTH_MAP] >> - rw[] >> - `EL x' x IN s` by metis_tac[perm_set_element, MEM_EL] >> - `EL x' y IN s` by metis_tac[perm_set_element, MEM_EL] >> - metis_tac[EL_MAP, BIJ_IS_INJ] -QED - -(* Theorem: BIJ f s (count n) ==> - SURJ (MAP f) (perm_set s) (perm_count n) *) -(* Proof: - By SURJ_DEF, this is to show: - (1) x IN perm_set s ==> MAP f x IN perm_count n - This is true by perm_set_map_element - (2) x IN perm_count n ==> ?y. y IN perm_set s /\ MAP f y = x - Let y = MAP (LINV f s) x. Then to show: - (1) y IN perm_set s, - Note BIJ (LINV f s) (count n) s by BIJ_LINV_BIJ - By perm_set_element, perm_count_element, to show: - (1) ALL_DISTINCT (MAP (LINV f s) x) - Note INJ (LINV f s) (count n) s by BIJ_DEF - so ALL_DISTINCT (MAP (LINV f s) x) - by ALL_DISTINCT_MAP_INJ, INJ_DEF - (2) set (MAP (LINV f s) x) = s - Note SURJ (LINV f s) (count n) s by BIJ_DEF - so set (MAP (LINV f s) x) - = IMAGE (LINV f s) (set x) by LIST_TO_SET_MAP - = IMAGE (LINV f s) (count n) by set x = count n - = s by IMAGE_SURJ - (2) x IN perm_count n ==> MAP f (MAP (LINV f s) x) = x - Let g = f o LINV f s. - The goal is: MAP g x = x by MAP_COMPOSE - Note LENGTH (MAP g x) = LENGTH x by LENGTH_MAP - To apply LIST_EQ, just need to show: - !k. k < LENGTH x ==> - EL k (MAP g x) = EL k x - or to show: g (EL k x) = EL k x by EL_MAP - Now set x = count n by perm_count_element - so EL k x IN (count n) by MEM_EL - Thus g (EL k x) = EL k x by BIJ_LINV_INV -*) -Theorem perm_set_map_surj: - !f s n. BIJ f s (count n) ==> - SURJ (MAP f) (perm_set s) (perm_count n) -Proof - rw[SURJ_DEF] >- - metis_tac[perm_set_map_element] >> - qexists_tac `MAP (LINV f s) x` >> - rpt strip_tac >| [ - `BIJ (LINV f s) (count n) s` by rw[BIJ_LINV_BIJ] >> - fs[perm_set_element, perm_count_element] >> - rpt strip_tac >- - metis_tac[ALL_DISTINCT_MAP_INJ, BIJ_IS_INJ] >> - simp[LIST_TO_SET_MAP] >> - fs[IMAGE_SURJ, BIJ_DEF], - simp[MAP_COMPOSE] >> - qabbrev_tac `g = f o LINV f s` >> - irule LIST_EQ >> - `LENGTH (MAP g x) = LENGTH x` by rw[LENGTH_MAP] >> - rw[] >> - simp[EL_MAP] >> - fs[perm_count_element, Abbr`g`] >> - metis_tac[MEM_EL, BIJ_LINV_INV] - ] -QED - -(* Theorem: BIJ f s (count n) ==> - BIJ (MAP f) (perm_set s) (perm_count n) *) -(* Proof: - Note INJ (MAP f) (perm_set s) (perm_count n) by perm_set_map_inj - and SURJ (MAP f) (perm_set s) (perm_count n) by perm_set_map_surj - Thus BIJ (MAP f) (perm_set s) (perm_count n) by BIJ_DEF -*) -Theorem perm_set_map_bij: - !f s n. BIJ f s (count n) ==> - BIJ (MAP f) (perm_set s) (perm_count n) -Proof - simp[BIJ_DEF, perm_set_map_inj, perm_set_map_surj] -QED - -(* Theorem: FINITE s ==> perm_set s =b= perm_count (CARD s) *) -(* Proof: - Note ?f. BIJ f s (count (CARD s)) by bij_eq_count, FINITE s - Thus BIJ (MAP f) (perm_set s) (perm_count (CARD s)) - by perm_set_map_bij - showing perm_set s =b= perm_count (CARD s) by notation -*) -Theorem perm_set_bij_eq_perm_count: - !s. FINITE s ==> perm_set s =b= perm_count (CARD s) -Proof - rpt strip_tac >> - imp_res_tac bij_eq_count >> - metis_tac[perm_set_map_bij] -QED - -(* Theorem: FINITE s ==> FINITE (perm_set s) *) -(* Proof: - Note perm_set s =b= perm_count (CARD s) by perm_set_bij_eq_perm_count - and FINITE (perm_count (CARD s)) by perm_count_finite - so FINITE (perm_set s) by bij_eq_finite -*) -Theorem perm_set_finite: - !s. FINITE s ==> FINITE (perm_set s) -Proof - metis_tac[perm_set_bij_eq_perm_count, perm_count_finite, bij_eq_finite] -QED - -(* Theorem: FINITE s ==> CARD (perm_set s) = perm (CARD s) *) -(* Proof: - Note perm_set s =b= perm_count (CARD s) by perm_set_bij_eq_perm_count - and FINITE (perm_count (CARD s)) by perm_count_finite - so CARD (perm_set s) - = CARD (perm_count (CARD s)) by bij_eq_card - = perm (CARD s) by perm_def -*) -Theorem perm_set_card: - !s. FINITE s ==> CARD (perm_set s) = perm (CARD s) -Proof - metis_tac[perm_set_bij_eq_perm_count, perm_count_finite, bij_eq_card, perm_def] -QED - -(* This is a major result! *) - -(* Theorem: FINITE s ==> CARD (perm_set s) = FACT (CARD s) *) -(* Proof: by perm_set_card, perm_eq_fact. *) -Theorem perm_set_card_alt: - !s. FINITE s ==> CARD (perm_set s) = FACT (CARD s) -Proof - simp[perm_set_card, perm_eq_fact] -QED - -(* ------------------------------------------------------------------------- *) -(* Counting number of arrangements. *) -(* ------------------------------------------------------------------------- *) - -(* Define the set of choices of k-tuples of (count n). *) -Definition list_count_def[nocompute]: - list_count n k = - { ls | ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k} -End -(* use [nocompute] as this is not effective for evalutaion. *) -(* Note: if defined as: - list_count n k = { ls | (set ls) SUBSET (count n) /\ CARD (set ls) = k} -then non-distinct lists will be in the set, which is not desirable. -*) - -(* Define the number of choices of k-tuples of (count n). *) -Definition arrange_def[nocompute]: - arrange n k = CARD (list_count n k) -End -(* use [nocompute] as this is not effective for evalutaion. *) -(* make this an infix operator *) -val _ = set_fixity "arrange" (Infix(NONASSOC, 550)); (* higher than arithmetic op 500. *) -(* arrange_def; -val it = |- !n k. n arrange k = CARD (list_count n k): thm *) - -(* Theorem: list_count n k = - { ls | ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ CARD (set ls) = k} *) -(* Proof: - ls IN list_count n k - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k - by list_count_def - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ CARD (set ls) = k - by ALL_DISTINCT_CARD_LIST_TO_SET - Hence the sets are equal by EXTENSION. -*) -Theorem list_count_alt: - !n k. list_count n k = - { ls | ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ CARD (set ls) = k} -Proof - simp[list_count_def, EXTENSION] >> - metis_tac[ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Theorem: ls IN list_count n k <=> - ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k *) -(* Proof: by list_count_def. *) -Theorem list_count_element: - !ls n k. ls IN list_count n k <=> - ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k -Proof - simp[list_count_def] -QED - -(* Theorem: ls IN list_count n k <=> - ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ CARD (set ls) = k *) -(* Proof: by list_count_alt. *) -Theorem list_count_element_alt: - !ls n k. ls IN list_count n k <=> - ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ CARD (set ls) = k -Proof - simp[list_count_alt] -QED - -(* Theorem: ls IN list_count n k ==> CARD (set ls) = k *) -(* Proof: - ls IN list_count n k - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k - by list_count_element - ==> CARD (set ls) = k by ALL_DISTINCT_CARD_LIST_TO_SET -*) -Theorem list_count_element_set_card: - !ls n k. ls IN list_count n k ==> CARD (set ls) = k -Proof - simp[list_count_def, ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Theorem: list_count n k SUBSET necklace k n *) -(* Proof: - ls IN list_count n k - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = k - by list_count_element - ==> (set ls) SUBSET (count n) /\ LENGTH ls = k - ==> ls IN necklace k n by necklace_def - Thus list_count n k SUBSET necklace k n by SUBSET_DEF -*) -Theorem list_count_subset: - !n k. list_count n k SUBSET necklace k n -Proof - simp[list_count_def, necklace_def, SUBSET_DEF] -QED - -(* Theorem: FINITE (list_count n k) *) -(* Proof: - Note list_count n k SUBSET necklace k n by list_count_subset - and FINITE (necklace k n) by necklace_finite - so FINITE (list_count n k) by SUBSET_FINITE -*) -Theorem list_count_finite: - !n k. FINITE (list_count n k) -Proof - metis_tac[list_count_subset, necklace_finite, SUBSET_FINITE] -QED - -(* Note: -list_count 4 2 has P(4,2) = 4 * 3 = 12 elements. -necklace 2 4 has 2 ** 4 = 16 elements. - -> EVAL ``necklace 2 4``; -val it = |- necklace 2 4 = - {[3; 3]; [3; 2]; [3; 1]; [3; 0]; [2; 3]; [2; 2]; [2; 1]; [2; 0]; - [1; 3]; [1; 2]; [1; 1]; [1; 0]; [0; 3]; [0; 2]; [0; 1]; [0; 0]}: thm -> EVAL ``IMAGE set (necklace 2 4)``; -val it = |- IMAGE set (necklace 2 4) = - {{3}; {2; 3}; {2}; {1; 3}; {1; 2}; {1}; {0; 3}; {0; 2}; {0; 1}; {0}}: -> EVAL ``IMAGE (\ls. if CARD (set ls) = 2 then ls else []) (necklace 2 4)``; -val it = |- IMAGE (\ls. if CARD (set ls) = 2 then ls else []) (necklace 2 4) = - {[3; 2]; [3; 1]; [3; 0]; [2; 3]; [2; 1]; [2; 0]; [1; 3]; [1; 2]; - [1; 0]; [0; 3]; [0; 2]; [0; 1]; []}: thm -> EVAL ``let n = 4; k = 2 in (IMAGE (\ls. if CARD (set ls) = k then ls else []) (necklace k n)) DELETE []``; -val it = |- (let n = 4; k = 2 in -IMAGE (\ls. if CARD (set ls) = k then ls else []) (necklace k n) DELETE []) = - {[3; 2]; [3; 1]; [3; 0]; [2; 3]; [2; 1]; [2; 0]; [1; 3]; [1; 2]; - [1; 0]; [0; 3]; [0; 2]; [0; 1]}: thm -> EVAL ``let n = 4; k = 2 in (IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n)) DELETE []``; -val it = |- (let n = 4; k = 2 in - IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE []) = - {[3; 2]; [3; 1]; [3; 0]; [2; 3]; [2; 1]; [2; 0]; [1; 3]; [1; 2]; - [1; 0]; [0; 3]; [0; 2]; [0; 1]}: thm -*) - -(* Note: -P(n,k) = C(n,k) * k! -P(n,0) = C(n,0) * 0! = 1 -P(0,k+1) = C(0,k+1) * (k+1)! = 0 -*) - -(* Theorem: list_count n 0 = {[]} *) -(* Proof: - ls IN list_count n 0 - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ LENGTH ls = 0 - by list_count_element - <=> ALL_DISTINCT ls /\ (set ls) SUBSET (count n) /\ ls = [] - by LENGTH_NIL - <=> T /\ T /\ ls = [] by ALL_DISTINCT, LIST_TO_SET, EMPTY_SUBSET - Thus list_count n 0 = {[]} by EXTENSION -*) -Theorem list_count_n_0: - !n. list_count n 0 = {[]} -Proof - rw[list_count_def, EXTENSION, EQ_IMP_THM] -QED - -(* Theorem: 0 < n ==> list_count 0 n = {} *) -(* Proof: - Note (list_count 0 n) SUBSET (necklace n 0) - by list_count_subset - but (necklace n 0) = {} by necklace_empty, 0 < n - Thus (list_count 0 n) = {} by SUBSET_EMPTY -*) -Theorem list_count_0_n: - !n. 0 < n ==> list_count 0 n = {} -Proof - metis_tac[list_count_subset, necklace_empty, SUBSET_EMPTY] -QED - -(* Theorem: list_count n n = perm_count n *) -(* Proof: - ls IN list_count n n - <=> ALL_DISTINCT ls /\ set ls SUBSET count n /\ CARD (set ls) = n - by list_count_element_alt - <=> ALL_DISTINCT ls /\ set ls SUBSET count n /\ CARD (set ls) = CARD (count n) - by CARD_COUNT - <=> ALL_DISTINCT ls /\ set ls SUBSET count n /\ set ls = count n - by SUBSET_CARD_EQ - <=> ALL_DISTINCT ls /\ set ls = count n by SUBSET_REFL - <=> ls IN perm_count n by perm_count_element -*) -Theorem list_count_n_n: - !n. list_count n n = perm_count n -Proof - rw_tac bool_ss[list_count_element_alt, EXTENSION] >> - `FINITE (count n) /\ CARD (count n) = n` by rw[] >> - metis_tac[SUBSET_REFL, SUBSET_CARD_EQ, perm_count_element] -QED - -(* Theorem: list_count n k = {} <=> n < k *) -(* Proof: - If part: list_count n k = {} ==> n < k - By contradiction, suppose k <= n. - Let ls = SET_TO_LIST (count k). - Note FINITE (count k) by FINITE_COUNT - Then ALL_DISTINCT ls by ALL_DISTINCT_SET_TO_LIST - and set ls = count k by SET_TO_LIST_INV - Now (count k) SUBSET (count n) by COUNT_SUBSET, k <= n - and CARD (count k) = k by CARD_COUNT - so ls IN list_count n k by list_count_element_alt - Thus list_count n k <> {} by MEMBER_NOT_EMPTY - which is a contradiction. - Only-if part: n < k ==> list_count n k = {} - By contradiction, suppose sub_count n k <> {}. - Then ?ls. ls IN list_count n k by MEMBER_NOT_EMPTY - ==> ALL_DISTINCT ls /\ set ls SUBSET count n /\ CARD (set ls) = k - by sub_count_element_alt - Note FINITE (count n) by FINITE_COUNT - so CARD (set ls) <= CARD (count n) - by CARD_SUBSET - ==> k <= n by CARD_COUNT - This contradicts n < k. -*) -Theorem list_count_eq_empty: - !n k. list_count n k = {} <=> n < k -Proof - rw[EQ_IMP_THM] >| [ - spose_not_then strip_assume_tac >> - qabbrev_tac `ls = SET_TO_LIST (count k)` >> - `FINITE (count k)` by rw[FINITE_COUNT] >> - `ALL_DISTINCT ls` by rw[ALL_DISTINCT_SET_TO_LIST, Abbr`ls`] >> - `set ls = count k` by rw[SET_TO_LIST_INV, Abbr`ls`] >> - `(count k) SUBSET (count n)` by rw[COUNT_SUBSET] >> - `CARD (count k) = k` by rw[] >> - metis_tac[list_count_element_alt, MEMBER_NOT_EMPTY], - spose_not_then strip_assume_tac >> - `?ls. ls IN list_count n k` by rw[MEMBER_NOT_EMPTY] >> - fs[list_count_element_alt] >> - `FINITE (count n)` by rw[] >> - `CARD (set ls) <= n` by metis_tac[CARD_SUBSET, CARD_COUNT] >> - decide_tac - ] -QED - -(* Theorem: 0 < k ==> - list_count n k = - IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE [] *) -(* Proof: - x IN IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE [] - <=> ?ls. x = (if ALL_DISTINCT ls then ls else []) /\ - LENGTH ls = k /\ set ls SUBSET count n) /\ x <> [] by IN_IMAGE, IN_DELETE - <=> ALL_DISTINCT x /\ LENGTH x = k /\ set x SUBSET count n by LENGTH_NIL, 0 < k, ls = x - <=> x IN list_count n k by list_count_element - Thus the two sets are equal by EXTENSION. -*) -Theorem list_count_by_image: - !n k. 0 < k ==> - list_count n k = - IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE [] -Proof - rw[list_count_def, necklace_def, EXTENSION] >> - (rw[EQ_IMP_THM] >> metis_tac[LENGTH_NIL, NOT_ZERO]) -QED - -(* Theorem: list_count n k = - if k = 0 then {[]} - else IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE [] *) -(* Proof: by list_count_n_0, list_count_by_image *) -Theorem list_count_eqn[compute]: - !n k. list_count n k = - if k = 0 then {[]} - else IMAGE (\ls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE [] -Proof - rw[list_count_n_0, list_count_by_image] -QED - -(* -> EVAL ``list_count 3 2``; -val it = |- list_count 3 2 = {[2; 1]; [2; 0]; [1; 2]; [1; 0]; [0; 2]; [0; 1]}: thm -> EVAL ``list_count 4 2``; -val it = |- list_count 4 2 = -{[3; 2]; [3; 1]; [3; 0]; [2; 3]; [2; 1]; [2; 0]; [1; 3]; [1; 2]; [1; 0]; [0; 3]; [0; 2]; [0; 1]}: thm -*) - -(* Idea: define an equivalence relation feq set: set x = set y. - There are k! elements in each equivalence class. - Thus n arrange k = perm k * n choose k. *) - -(* Theorem: (feq set) equiv_on s *) -(* Proof: by feq_equiv. *) -Theorem feq_set_equiv: - !s. (feq set) equiv_on s -Proof - simp[feq_equiv] -QED - -(* -> EVAL ``list_count 3 2``; -val it = |- list_count 3 2 = {[2; 1]; [1; 2]; [2; 0]; [0; 2]; [1; 0]; [0; 1]}: thm -*) - -(* Theorem: ls IN list_count n k ==> - equiv_class (feq set) (list_count n k) ls = perm_set (set ls) *) -(* Proof: - Note ALL_DISTINCT ls /\ set ls SUBSET count n /\ LENGTH ls = k - by list_count_element - x IN equiv_class (feq set) (list_count n k) ls - <=> x IN (list_count n k) /\ (feq set) ls x by equiv_class_element - <=> x IN (list_count n k) /\ set ls = set x by feq_def - <=> ALL_DISTINCT x /\ set x SUBSET count n /\ LENGTH x = k /\ - set x = set ls by list_count_element - <=> ALL_DISTINCT x /\ LENGTH x = LENGTH ls /\ set x = set ls - by given - <=> ALL_DISTINCT x /\ set x = set ls by ALL_DISTINCT_CARD_LIST_TO_SET - <=> x IN perm_set (set ls) by perm_set_element -*) -Theorem list_count_set_eq_class: - !ls n k. ls IN list_count n k ==> - equiv_class (feq set) (list_count n k) ls = perm_set (set ls) -Proof - rw[list_count_def, perm_set_def, fequiv_def, Once EXTENSION] >> - rw[EQ_IMP_THM] >> - metis_tac[ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Theorem: ls IN list_count n k ==> - CARD (equiv_class (feq set) (list_count n k) ls) = perm k *) -(* Proof: - Note ALL_DISTINCT ls /\ set ls SUBSET count n /\ LENGTH ls = k - by list_count_element - CARD (equiv_class (feq set) (list_count n k) ls) - = CARD (perm_set (set ls)) by list_count_set_eq_class - = perm (CARD (set ls)) by perm_set_card - = perm (LENGTH ls) by ALL_DISTINCT_CARD_LIST_TO_SET - = perm k by LENGTH ls = k -*) -Theorem list_count_set_eq_class_card: - !ls n k. ls IN list_count n k ==> - CARD (equiv_class (feq set) (list_count n k) ls) = perm k -Proof - rw[list_count_set_eq_class] >> - fs[list_count_element] >> - simp[perm_set_card, ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Theorem: e IN partition (feq set) (list_count n k) ==> CARD e = perm k *) -(* Proof: - By partition_element, this is to show: - ls IN list_count n k ==> - CARD (equiv_class (feq set) (list_count n k) ls) = perm k - This is true by list_count_set_eq_class_card. -*) -Theorem list_count_set_partititon_element_card: - !n k e. e IN partition (feq set) (list_count n k) ==> CARD e = perm k -Proof - rw_tac bool_ss [partition_element] >> - simp[list_count_set_eq_class_card] -QED - -(* Theorem: ls IN list_count n k ==> perm_set (set ls) <> {} *) -(* Proof: - Note (feq set) equiv_on (list_count n k) by feq_set_equiv - and perm_set (set ls) - = equiv_class (feq set) (list_count n k) ls by list_count_set_eq_class - <> {} by equiv_class_not_empty -*) -Theorem list_count_element_perm_set_not_empty: - !ls n k. ls IN list_count n k ==> perm_set (set ls) <> {} -Proof - metis_tac[list_count_set_eq_class, feq_set_equiv, equiv_class_not_empty] -QED - -(* This is more restrictive than perm_set_list_not_empty, hence not useful. *) - -(* Theorem: s IN (partition (feq set) (list_count n k)) ==> - (set o CHOICE) s IN (sub_count n k) *) -(* Proof: - s IN (partition (feq set) (list_count n k)) - <=> ?z. z IN list_count n k /\ - !x. x IN s <=> x IN list_count n k /\ set x = set z - by feq_partition_element - ==> z IN s, so s <> {} by MEMBER_NOT_EMPTY - Let ls = CHOICE s. - Then ls IN s by CHOICE_DEF - so ls IN list_count n k /\ set ls = set z - by implication - or ALL_DISTINCT ls /\ set ls SUBSET count n /\ LENGTH ls = k - by list_count_element - Note (set o CHOICE) s = set ls by o_THM - and CARD (set ls) = LENGTH ls by ALL_DISTINCT_CARD_LIST_TO_SET - so set ls IN (sub_count n k) by sub_count_element_alt -*) -Theorem list_count_set_map_element: - !s n k. s IN (partition (feq set) (list_count n k)) ==> - (set o CHOICE) s IN (sub_count n k) -Proof - rw[feq_partition_element] >> - `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> - `(CHOICE s) IN s` by fs[CHOICE_DEF] >> - fs[list_count_element, sub_count_element] >> - metis_tac[ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Theorem: INJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) *) -(* Proof: - Let R = feq set, - s = list_count n k, - t = sub_count n k. - By INJ_DEF, this is to show: - (1) x IN partition R s ==> (set o CHOICE) x IN t - This is true by list_count_set_map_element - (2) x IN partition R s /\ y IN partition R s /\ - (set o CHOICE) x = (set o CHOICE) y ==> x = y - Note ?u. u IN list_count n k - !ls. ls IN x <=> ls IN list_count n k /\ set ls = set u - by feq_partition_element - and ?v. v IN list_count n k - !ls. ls IN y <=> ls IN list_count n k /\ set ls = set v - by feq_partition_element - Thus u IN x, so x <> {} by MEMBER_NOT_EMPTY - and v IN y, so y <> {} by MEMBER_NOT_EMPTY - Let lx = CHOICE x IN x by CHOICE_DEF - and ly = CHOICE y IN y by CHOICE_DEF - With set lx = set ly by o_THM - Thus set lx = set u by implication - and set ly = set v by implication - so set u = set v by above - Thus x = y by EXTENSION -*) -Theorem list_count_set_map_inj: - !n k. INJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) -Proof - rw_tac bool_ss[INJ_DEF] >- - simp[list_count_set_map_element] >> - fs[feq_partition_element] >> - `x <> {} /\ y <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> - `CHOICE x IN x /\ CHOICE y IN y` by fs[CHOICE_DEF] >> - `set z = set z'` by rfs[] >> - simp[EXTENSION] -QED - -(* Theorem: SURJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) *) -(* Proof: - Let R = feq set, - s = list_count n k, - t = sub_count n k. - By SURJ_DEF, this is to show: - (1) x IN partition R s ==> (set o CHOICE) x IN t - This is true by list_count_set_map_element - (2) x IN t ==> ?y. y IN partition R s /\ (set o CHOICE) y = x - Note x SUBSET count n /\ CARD x = k by sub_count_element - Thus FINITE x by SUBSET_FINITE, FINITE_COUNT - Let y = perm_set x. - To show; - (1) y IN partition R s - Note y IN partition R s - <=> ?ls. ls IN list_count n k /\ - !z. z IN perm_set x <=> z IN list_count n k /\ set z = set ls - by feq_partition_element - Let ls = SET_TO_LIST x. - Then ALL_DISTINCT ls by ALL_DISTINCT_SET_TO_LIST, FINITE x - and set ls = x by SET_TO_LIST_INV, FINITE x - so set ls SUBSET (count n) by above, x SUBSET count n - and LENGTH ls = k by SET_TO_LIST_CARD, FINITE x - so ls IN list_count n k by list_count_element - To show: !z. z IN perm_set x <=> z IN list_count n k /\ set z = set ls - z IN perm_set x - <=> ALL_DISTINCT z /\ set z = x by perm_set_element - <=> ALL_DISTINCT z /\ set z SUBSET count n /\ set z = x - by x SUBSET count n - <=> ALL_DISTINCT z /\ set z SUBSET count n /\ LENGTH z = CARD x - by ALL_DISTINCT_CARD_LIST_TO_SET - <=> z IN list_count n k /\ set z = set ls - by list_count_element, CARD x = k, set ls = x. - (2) (set o CHOICE) y = x - Note y <> {} by perm_set_not_empty, FINITE x - Then CHOICE y IN y by CHOICE_DEF - so (set o CHOICE) y - = set (CHOICE y) by o_THM - = x by perm_set_element, y = perm_set x -*) -Theorem list_count_set_map_surj: - !n k. SURJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) -Proof - rw_tac bool_ss[SURJ_DEF] >- - simp[list_count_set_map_element] >> - fs[sub_count_element] >> - `FINITE x` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> - qexists_tac `perm_set x` >> - simp[feq_partition_element, list_count_element, perm_set_element] >> - rpt strip_tac >| [ - qabbrev_tac `ls = SET_TO_LIST x` >> - qexists_tac `ls` >> - `ALL_DISTINCT ls` by rw[ALL_DISTINCT_SET_TO_LIST, Abbr`ls`] >> - `set ls = x` by rw[SET_TO_LIST_INV, Abbr`ls`] >> - `LENGTH ls = k` by rw[SET_TO_LIST_CARD, Abbr`ls`] >> - rw[EQ_IMP_THM] >> - metis_tac[ALL_DISTINCT_CARD_LIST_TO_SET], - `perm_set x <> {}` by fs[perm_set_not_empty] >> - qabbrev_tac `ls = CHOICE (perm_set x)` >> - `ls IN perm_set x` by fs[CHOICE_DEF, Abbr`ls`] >> - fs[perm_set_element] - ] -QED - -(* Theorem: BIJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) *) -(* Proof: - Let f = set o CHOICE, - s = partition (feq set) (list_count n k), - t = sub_count n k. - Note INJ f s t by list_count_set_map_inj - and SURJ f s t by list_count_set_map_surj - so BIJ f s t by BIJ_DEF -*) -Theorem list_count_set_map_bij: - !n k. BIJ (set o CHOICE) (partition (feq set) (list_count n k)) (sub_count n k) -Proof - simp[BIJ_DEF, list_count_set_map_inj, list_count_set_map_surj] -QED - -(* Theorem: n arrange k = (n choose k) * perm k *) -(* Proof: - Let R = feq set, - s = list_count n k, - t = sub_count n k. - Then FINITE s by list_count_finite - and R equiv_on s by feq_set_equiv - and !e. e IN partition R s ==> CARD e = perm k - by list_count_set_partititon_element_card - Thus CARD s = perm k * CARD (partition R s) - by equal_partition_card, [1] - Note CARD s = n arrange k by arrange_def - and BIJ (set o CHOICE) (partition R s) t - by list_count_set_map_bij - and FINITE t by sub_count_finite - so CARD (partition R s) - = CARD t by bij_eq_card - = n choose k by choose_def - Hence n arrange k = n choose k * perm k - by MULT_COMM, [1], above. -*) -Theorem arrange_eqn[compute]: - !n k. n arrange k = (n choose k) * perm k -Proof - rpt strip_tac >> - assume_tac list_count_set_map_bij >> - last_x_assum (qspecl_then [`n`, `k`] strip_assume_tac) >> - qabbrev_tac `R = feq (set :num list -> num -> bool)` >> - qabbrev_tac `s = list_count n k` >> - qabbrev_tac `t = sub_count n k` >> - `FINITE s` by rw[list_count_finite, Abbr`s`] >> - `R equiv_on s` by rw[feq_set_equiv, Abbr`R`] >> - `!e. e IN partition R s ==> CARD e = perm k` by metis_tac[list_count_set_partititon_element_card] >> - imp_res_tac equal_partition_card >> - `FINITE t` by rw[sub_count_finite, Abbr`t`] >> - `CARD (partition R s) = CARD t` by metis_tac[bij_eq_card] >> - simp[arrange_def, choose_def, Abbr`s`, Abbr`t`] -QED - -(* This is P(n,k) = C(n,k) * k! *) - -(* Theorem: n arrange k = (n choose k) * FACT k *) -(* Proof: - n arrange k - = (n choose k) * perm k by arrange_eqn - = (n choose k) * FACT k by perm_eq_fact -*) -Theorem arrange_alt: - !n k. n arrange k = (n choose k) * FACT k -Proof - simp[arrange_eqn, perm_eq_fact] -QED - -(* -> EVAL ``5 arrange 2``; = 20 -> EVAL ``MAP ($arrange 5) [0 .. 5]``; = [1; 5; 20; 60; 120; 120] -*) - -(* Theorem: n arrange k = (binomial n k) * FACT k *) -(* Proof: - n arrange k - = (n choose k) * FACT k by arrange_alt - = (binomial n k) * FACT k by choose_eqn -*) -Theorem arrange_formula: - !n k. n arrange k = (binomial n k) * FACT k -Proof - simp[arrange_alt, choose_eqn] -QED - -(* Theorem: k <= n ==> n arrange k = FACT n DIV FACT (n - k) *) -(* Proof: - Note 0 < FACT (n - k) by FACT_LESS - (n arrange k) * FACT (n - k) - = (binomial n k) * FACT k * FACT (n - k) by arrange_formula - = binomial n k * (FACT (n - k) * FACT k) by arithmetic - = FACT n by binomial_formula2, k <= n - Thus n arrange k = FACT n DIV FACT (n - k) by DIV_SOLVE -*) -Theorem arrange_formula2: - !n k. k <= n ==> n arrange k = FACT n DIV FACT (n - k) -Proof - rpt strip_tac >> - `0 < FACT (n - k)` by rw[FACT_LESS] >> - `(n arrange k) * FACT (n - k) = (binomial n k) * FACT k * FACT (n - k)` by rw[arrange_formula] >> - `_ = binomial n k * (FACT (n - k) * FACT k)` by rw[] >> - `_ = FACT n` by rw[binomial_formula2] >> - simp[DIV_SOLVE] -QED - -(* Theorem: n arrange 0 = 1 *) -(* Proof: - n arrange 0 - = CARD (list_count n 0) by arrange_def - = CARD {[]} by list_count_n_0 - = 1 by CARD_SING -*) -Theorem arrange_n_0: - !n. n arrange 0 = 1 -Proof - simp[arrange_def, perm_def, list_count_n_0] -QED - -(* Theorem: 0 < n ==> 0 arrange n = 0 *) -(* Proof: - 0 arrange n - = CARD (list_count 0 n) by arrange_def - = CARD {} by list_count_0_n, 0 < n - = 0 by CARD_EMPTY -*) -Theorem arrange_0_n: - !n. 0 < n ==> 0 arrange n = 0 -Proof - simp[arrange_def, perm_def, list_count_0_n] -QED - -(* Theorem: n arrange n = perm n *) -(* Proof: - n arrange n - = (binomial n n) * FACT n by arrange_formula - = 1 * FACT n by binomial_n_n - = perm n by perm_eq_fact -*) -Theorem arrange_n_n: - !n. n arrange n = perm n -Proof - simp[arrange_formula, binomial_n_n, perm_eq_fact] -QED - -(* Theorem: n arrange n = FACT n *) -(* Proof: - n arrange n - = (binomial n n) * FACT n by arrange_formula - = 1 * FACT n by binomial_n_n -*) -Theorem arrange_n_n_alt: - !n. n arrange n = FACT n -Proof - simp[arrange_formula, binomial_n_n] -QED - -(* Theorem: n arrange k = 0 <=> n < k *) -(* Proof: - Note FINITE (list_count n k) by list_count_finite - n arrange k = 0 - <=> CARD (list_count n k) = 0 by arrange_def - <=> list_count n k = {} by CARD_EQ_0 - <=> n < k by list_count_eq_empty -*) -Theorem arrange_eq_0: - !n k. n arrange k = 0 <=> n < k -Proof - metis_tac[arrange_def, list_count_eq_empty, list_count_finite, CARD_EQ_0] -QED - -(* Note: - -k-permutation recurrence? - -P(n,k) = C(n,k) * k! -P(n,0) = C(n,0) * 0! = 1 -P(0,k+1) = C(0,k+1) * (k+1)! = 0 - -C(n+1,k+1) = C(n,k) + C(n,k+1) -P(n+1,k+1)/(k+1)! = P(n,k)/k! + P(n,k+1)/(k+1)! -P(n+1,k+1) = (k+1) * P(n,k) + P(n,k+1) -P(n+1,k+1) = P(n,k) * (k + 1) + P(n,k+1) - -P(2,1) = 2: [0] [1] -P(2,2) = 2: [0,1] [1,0] -P(3,2) = 6: [0,1] [0,2] include 2: [0,2] [1,2] [2,0] [2,1] - [1,0] [1,2] exclude 2: [0,1] [1,0] - [2,0] [2,1] -P(3,2) = P(2,1) * 2 + P(2,2) = ([0][1],2 + 2,[0][1]) + to_lists {0,1} -P(4,3): include 3: P(3,2) * 3 - exclude 3: P(3,3) - -list_count (n+1) (k+1) = IMAGE (interleave k) (list_count n k) UNION list_count n (k + 1) - -closed? -https://math.stackexchange.com/questions/3060456/ -using Pascal argument - -*) - - -(* ------------------------------------------------------------------------- *) - -(* export theory at end *) -val _ = export_theory(); - -(*===========================================================================*) diff --git a/examples/fermat/count/helperCountScript.sml b/examples/fermat/count/helperCountScript.sml deleted file mode 100644 index b76a28dd8b..0000000000 --- a/examples/fermat/count/helperCountScript.sml +++ /dev/null @@ -1,531 +0,0 @@ -(* ------------------------------------------------------------------------- *) -(* Count Helper. *) -(* ------------------------------------------------------------------------- *) - -(*===========================================================================*) - -(* add all dependent libraries for script *) -open HolKernel boolLib bossLib Parse; - -(* declare new theory at start *) -val _ = new_theory "helperCount"; - -(* ------------------------------------------------------------------------- *) - - -(* open dependent theories *) -(* val _ = load "EulerTheory"; *) -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; - - -(* ------------------------------------------------------------------------- *) -(* Count Helper Documentation *) -(* ------------------------------------------------------------------------- *) -(* Overloading (# is temporary): - over f s t = !x. x IN s ==> f x IN t - s bij_eq t = ?f. BIJ f s t - s =b= t = ?f. BIJ f s t -*) -(* Definitions and Theorems (# are exported, ! are in compute): - - Set Theorems: - over_inj |- !f s t. INJ f s t ==> over f s t - over_surj |- !f s t. SURJ f s t ==> over f s t - over_bij |- !f s t. BIJ f s t ==> over f s t - SURJ_CARD_IMAGE_EQ |- !f s t. FINITE t /\ over f s t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t) - FINITE_SURJ_IFF |- !f s t. FINITE t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t /\ over f s t) - INJ_IMAGE_BIJ_IFF |- !f s t. INJ f s t <=> BIJ f s (IMAGE f s) /\ over f s t - INJ_IFF_BIJ_IMAGE |- !f s t. over f s t ==> (INJ f s t <=> BIJ f s (IMAGE f s)) - INJ_IMAGE_IFF |- !f s t. INJ f s t <=> INJ f s (IMAGE f s) /\ over f s t - FUNSET_ALT |- !P Q. FUNSET P Q = {f | over f P Q} - - Bijective Equivalence: - bij_eq_empty |- !s t. s =b= t ==> (s = {} <=> t = {}) - bij_eq_refl |- !s. s =b= s - bij_eq_sym |- !s t. s =b= t <=> t =b= s - bij_eq_trans |- !s t u. s =b= t /\ t =b= u ==> s =b= u - bij_eq_equiv_on |- !P. $=b= equiv_on P - bij_eq_finite |- !s t. s =b= t ==> (FINITE s <=> FINITE t) - bij_eq_count |- !s. FINITE s ==> s =b= count (CARD s) - bij_eq_card |- !s t. s =b= t /\ (FINITE s \/ FINITE t) ==> CARD s = CARD t - bij_eq_card_eq |- !s t. FINITE s /\ FINITE t ==> (s =b= t <=> CARD s = CARD t) - - Alternate characterisation of maps: - surj_preimage_not_empty - |- !f s t. SURJ f s t <=> - over f s t /\ !y. y IN t ==> preimage f s y <> {} - inj_preimage_empty_or_sing - |- !f s t. INJ f s t <=> - over f s t /\ !y. y IN t ==> preimage f s y = {} \/ - SING (preimage f s y) - bij_preimage_sing |- !f s t. BIJ f s t <=> - over f s t /\ !y. y IN t ==> SING (preimage f s y) - surj_iff_preimage_card_not_0 - |- !f s t. FINITE s /\ over f s t ==> - (SURJ f s t <=> - !y. y IN t ==> CARD (preimage f s y) <> 0) - inj_iff_preimage_card_le_1 - |- !f s t. FINITE s /\ over f s t ==> - (INJ f s t <=> - !y. y IN t ==> CARD (preimage f s y) <= 1) - bij_iff_preimage_card_eq_1 - |- !f s t. FINITE s /\ over f s t ==> - (BIJ f s t <=> - !y. y IN t ==> CARD (preimage f s y) = 1) - finite_surj_inj_iff |- !f s t. FINITE s /\ SURJ f s t ==> - (INJ f s t <=> - !e. e IN IMAGE (preimage f s) t ==> CARD e = 1) -*) - -(* ------------------------------------------------------------------------- *) -(* Set Theorems *) -(* ------------------------------------------------------------------------- *) - -(* Overload a function from domain to range. *) -val _ = overload_on("over", ``\f s t. !x. x IN s ==> f x IN t``); -(* not easy to make this a good infix operator! *) - -(* Theorem: INJ f s t ==> over f s t *) -(* Proof: by INJ_DEF. *) -Theorem over_inj: - !f s t. INJ f s t ==> over f s t -Proof - simp[INJ_DEF] -QED - -(* Theorem: SURJ f s t ==> over f s t *) -(* Proof: by SURJ_DEF. *) -Theorem over_surj: - !f s t. SURJ f s t ==> over f s t -Proof - simp[SURJ_DEF] -QED - -(* Theorem: BIJ f s t ==> over f s t *) -(* Proof: by BIJ_DEF, INJ_DEF. *) -Theorem over_bij: - !f s t. BIJ f s t ==> over f s t -Proof - simp[BIJ_DEF, INJ_DEF] -QED - -(* Theorem: FINITE t /\ over f s t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t) *) -(* Proof: - If part: SURJ f s t ==> CARD (IMAGE f s) = CARD t - Note IMAGE f s = t by IMAGE_SURJ - Hence true. - Only-if part: CARD (IMAGE f s) = CARD t ==> SURJ f s t - By contradiction, suppose ~SURJ f s t. - Then IMAGE f s <> t by IMAGE_SURJ - but IMAGE f s SUBSET t by IMAGE_SUBSET_TARGET - so IMAGE f s PSUBSET t by PSUBSET_DEF - ==> CARD (IMAGE f s) < CARD t - by CARD_PSUBSET - This contradicts CARD (IMAGE f s) = CARD t. -*) -Theorem SURJ_CARD_IMAGE_EQ: - !f s t. FINITE t /\ over f s t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t) -Proof - rw[EQ_IMP_THM] >- - fs[IMAGE_SURJ] >> - spose_not_then strip_assume_tac >> - `IMAGE f s <> t` by rw[GSYM IMAGE_SURJ] >> - `IMAGE f s PSUBSET t` by fs[IMAGE_SUBSET_TARGET, PSUBSET_DEF] >> - imp_res_tac CARD_PSUBSET >> - decide_tac -QED - -(* Theorem: FINITE t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t /\ over f s t) *) -(* Proof: - If part: true by SURJ_DEF, IMAGE_SURJ - Only-if part: true by SURJ_CARD_IMAGE_EQ -*) -Theorem FINITE_SURJ_IFF: - !f s t. FINITE t ==> - (SURJ f s t <=> CARD (IMAGE f s) = CARD t /\ over f s t) -Proof - metis_tac[SURJ_CARD_IMAGE_EQ, SURJ_DEF] -QED - -(* Note: this cannot be proved: -g `!f s t. FINITE t /\ over f s t ==> - (INJ f s t <=> CARD (IMAGE f s) = CARD t)`; -Take f = I, s = count m, t = count n, with m <= n. -Then INJ I (count m) (count n) -and IMAGE I (count m) = (count m) -so CARD (IMAGE f s) = m, CARD t = n, may not equal. -*) - -(* INJ_IMAGE_BIJ |- !s f. (?t. INJ f s t) ==> BIJ f s (IMAGE f s) *) - -(* Theorem: INJ f s t <=> (BIJ f s (IMAGE f s) /\ over f s t) *) -(* Proof: - If part: INJ f s t ==> BIJ f s (IMAGE f s) /\ over f s t - Note BIJ f s (IMAGE f s) by INJ_IMAGE_BIJ - and over f s t by INJ_DEF - Only-if: BIJ f s (IMAGE f s) /\ over f s t ==> INJ f s t - By INJ_DEF, this is to show: - (1) x IN s ==> f x IN t, true by given - (2) x IN s /\ y IN s /\ f x = f y ==> x = y - Note f x IN (IMAGE f s) by IN_IMAGE - and f y IN (IMAGE f s) by IN_IMAGE - so f x = f y ==> x = y by BIJ_IS_INJ -*) -Theorem INJ_IMAGE_BIJ_IFF: - !f s t. INJ f s t <=> (BIJ f s (IMAGE f s) /\ over f s t) -Proof - rw[EQ_IMP_THM] >- - metis_tac[INJ_IMAGE_BIJ] >- - fs[INJ_DEF] >> - rw[INJ_DEF] >> - metis_tac[BIJ_IS_INJ, IN_IMAGE] -QED - -(* Theorem: over f s t ==> (INJ f s t <=> BIJ f s (IMAGE f s)) *) -(* Proof: by INJ_IMAGE_BIJ_IFF. *) -Theorem INJ_IFF_BIJ_IMAGE: - !f s t. over f s t ==> (INJ f s t <=> BIJ f s (IMAGE f s)) -Proof - metis_tac[INJ_IMAGE_BIJ_IFF] -QED - -(* -INJ_IMAGE |- !f s t. INJ f s t ==> INJ f s (IMAGE f s) -*) - -(* Theorem: INJ f s t <=> INJ f s (IMAGE f s) /\ over f s t *) -(* Proof: - Let P = over f s t. - If part: INJ f s t ==> INJ f s (IMAGE f s) /\ P - Note INJ f s (IMAGE f s) by INJ_IMAGE - and P is true by INJ_DEF - Only-if part: INJ f s (IMAGE f s) /\ P ==> INJ f s t - Note s SUBSET s by SUBSET_REFL - and (IMAGE f s) SUBSET t by IMAGE_SUBSET_TARGET - Thus INJ f s t by INJ_SUBSET -*) -Theorem INJ_IMAGE_IFF: - !f s t. INJ f s t <=> INJ f s (IMAGE f s) /\ over f s t -Proof - rw[EQ_IMP_THM] >- - metis_tac[INJ_IMAGE] >- - fs[INJ_DEF] >> - `s SUBSET s` by rw[] >> - `(IMAGE f s) SUBSET t` by fs[IMAGE_SUBSET_TARGET] >> - metis_tac[INJ_SUBSET] -QED - -(* pred_setTheory: -FUNSET |- !P Q. FUNSET P Q = (\f. over f P Q) -*) - -(* Theorem: FUNSET P Q = {f | over f P Q} *) -(* Proof: by FUNSET, EXTENSION *) -Theorem FUNSET_ALT: - !P Q. FUNSET P Q = {f | over f P Q} -Proof - rw[FUNSET, EXTENSION] -QED - -(* ------------------------------------------------------------------------- *) -(* Bijective Equivalence *) -(* ------------------------------------------------------------------------- *) - -(* Overload bijectively equal. *) -val _ = overload_on("bij_eq", ``\s t. ?f. BIJ f s t``); -val _ = set_fixity "bij_eq" (Infix(NONASSOC, 450)); (* same as relation *) - -val _ = overload_on ("=b=", ``$bij_eq``); -val _ = set_fixity "=b=" (Infix(NONASSOC, 450)); - -(* -> BIJ_SYM; -val it = |- !s t. s bij_eq t <=> t bij_eq s: thm -> BIJ_SYM; -val it = |- !s t. s =b= t <=> t =b= s: thm -> FINITE_BIJ_COUNT_CARD -val it = |- !s. FINITE s ==> count (CARD s) =b= s: thm -*) - -(* Theorem: s =b= t ==> (s = {} <=> t = {}) *) -(* Proof: by BIJ_EMPTY. *) -Theorem bij_eq_empty: - !s t. s =b= t ==> (s = {} <=> t = {}) -Proof - metis_tac[BIJ_EMPTY] -QED - -(* Theorem: s =b= s *) -(* Proof: by BIJ_I_SAME *) -Theorem bij_eq_refl: - !s. s =b= s -Proof - metis_tac[BIJ_I_SAME] -QED - -(* Theorem alias *) -Theorem bij_eq_sym = BIJ_SYM; -(* val bij_eq_sym = |- !s t. s =b= t <=> t =b= s: thm *) - -Theorem bij_eq_trans = BIJ_TRANS; -(* val bij_eq_trans = |- !s t u. s =b= t /\ t =b= u ==> s =b= u: thm *) - -(* Idea: bij_eq is an equivalence relation on any set of sets. *) - -(* Theorem: $=b= equiv_on P *) -(* Proof: - By equiv_on_def, this is to show: - (1) s IN P ==> s =b= s, true by bij_eq_refl - (2) s IN P /\ t IN P ==> (t =b= s <=> s =b= t) - This is true by bij_eq_sym - (3) s IN P /\ s' IN P /\ t IN P /\ - BIJ f s s' /\ BIJ f' s' t ==> s =b= t - This is true by bij_eq_trans -*) -Theorem bij_eq_equiv_on: - !P. $=b= equiv_on P -Proof - rw[equiv_on_def] >- - simp[bij_eq_refl] >- - simp[Once bij_eq_sym] >> - metis_tac[bij_eq_trans] -QED - -(* Theorem: s =b= t ==> (FINITE s <=> FINITE t) *) -(* Proof: by BIJ_FINITE_IFF *) -Theorem bij_eq_finite: - !s t. s =b= t ==> (FINITE s <=> FINITE t) -Proof - metis_tac[BIJ_FINITE_IFF] -QED - -(* This is the iff version of: -pred_setTheory.FINITE_BIJ_CARD; -|- !f s t. FINITE s /\ BIJ f s t ==> CARD s = CARD t -*) - -(* Theorem: FINITE s ==> s =b= (count (CARD s)) *) -(* Proof: by FINITE_BIJ_COUNT_CARD, BIJ_SYM *) -Theorem bij_eq_count: - !s. FINITE s ==> s =b= (count (CARD s)) -Proof - metis_tac[FINITE_BIJ_COUNT_CARD, BIJ_SYM] -QED - -(* Theorem: s =b= t /\ (FINITE s \/ FINITE t) ==> CARD s = CARD t *) -(* Proof: by FINITE_BIJ_CARD, BIJ_SYM. *) -Theorem bij_eq_card: - !s t. s =b= t /\ (FINITE s \/ FINITE t) ==> CARD s = CARD t -Proof - metis_tac[FINITE_BIJ_CARD, BIJ_SYM] -QED - -(* Theorem: FINITE s /\ FINITE t ==> (s =b= t <=> CARD s = CARD t) *) -(* Proof: - If part: s =b= t ==> CARD s = CARD t - This is true by FINITE_BIJ_CARD - Only-if part: CARD s = CARD t ==> s =b= t - Let n = CARD s = CARD t. - Note ?f. BIJ f s (count n) by bij_eq_count - and ?g. BIJ g (count n) t by FINITE_BIJ_COUNT_CARD - Thus s =b= t by bij_eq_trans -*) -Theorem bij_eq_card_eq: - !s t. FINITE s /\ FINITE t ==> (s =b= t <=> CARD s = CARD t) -Proof - rw[EQ_IMP_THM] >- - metis_tac[FINITE_BIJ_CARD] >> - `?f. BIJ f s (count (CARD s))` by rw[bij_eq_count] >> - `?g. BIJ g (count (CARD t)) t` by rw[FINITE_BIJ_COUNT_CARD] >> - metis_tac[bij_eq_trans] -QED - -(* ------------------------------------------------------------------------- *) -(* Alternate characterisation of maps. *) -(* ------------------------------------------------------------------------- *) - -(* Theorem: SURJ f s t <=> - over f s t /\ (!y. y IN t ==> preimage f s y <> {}) *) -(* Proof: - Let P = over f s t, - Q = !y. y IN t ==> preimage f s y <> {}. - If part: SURJ f s t ==> P /\ Q - P is true by SURJ_DEF - Q is true by preimage_def, SURJ_DEF - Only-if part: P /\ Q ==> SURJ f s t - This is true by preimage_def, SURJ_DEF -*) -Theorem surj_preimage_not_empty: - !f s t. SURJ f s t <=> - over f s t /\ (!y. y IN t ==> preimage f s y <> {}) -Proof - rw[SURJ_DEF, preimage_def, EXTENSION] >> - metis_tac[] -QED - -(* Theorem: INJ f s t <=> - over f s t /\ - (!y. y IN t ==> (preimage f s y = {} \/ - SING (preimage f s y))) *) -(* Proof: - Let P = over f s t, - Q = !y. y IN t ==> preimage f s y = {} \/ SING (preimage f s y). - If part: INJ f s t ==> P /\ Q - P is true by INJ_DEF - For Q, if preimage f s y <> {}, - Then ?x. x IN preimage f s y by MEMBER_NOT_EMPTY - or ?x. x IN s /\ f x = y by in_preimage - Thus !z. z IN preimage f s y ==> z = x - by in_preimage, INJ_DEF - or SING (preimage f s y) by SING_DEF, EXTENSION - Only-if part: P /\ Q ==> INJ f s t - By INJ_DEF, this is to show: - !x y. x IN s /\ y IN s /\ f x = f y ==> x = y - Let z = f x, then z IN t by over f s t - so x IN preimage f s z by in_preimage - and y IN preimage f s z by in_preimage - Thus preimage f s z <> {} by MEMBER_NOT_EMPTY - so SING (preimage f s z) by implication - ==> x = y by SING_ELEMENT -*) -Theorem inj_preimage_empty_or_sing: - !f s t. INJ f s t <=> - over f s t /\ - (!y. y IN t ==> (preimage f s y = {} \/ - SING (preimage f s y))) -Proof - rw[EQ_IMP_THM] >- - fs[INJ_DEF] >- - ((Cases_on `preimage f s y = {}` >> simp[]) >> - `?x. x IN s /\ f x = y` by metis_tac[in_preimage, MEMBER_NOT_EMPTY] >> - simp[SING_DEF] >> - qexists_tac `x` >> - rw[preimage_def, EXTENSION] >> - metis_tac[INJ_DEF]) >> - rw[INJ_DEF] >> - qabbrev_tac `z = f x` >> - `z IN t` by fs[Abbr`z`] >> - `x IN preimage f s z` by fs[preimage_def] >> - `y IN preimage f s z` by fs[preimage_def] >> - metis_tac[MEMBER_NOT_EMPTY, SING_ELEMENT] -QED - -(* Theorem: BIJ f s t <=> - over f s t /\ - (!y. y IN t ==> SING (preimage f s y)) *) -(* Proof: - Let P = over f s t, - Q = !y. y IN t ==> SING (preimage f s y). - If part: BIJ f s t ==> P /\ Q - P is true by BIJ_DEF, INJ_DEF - For Q, - Note INJ f s t /\ SURJ f s t by BIJ_DEF - so preimage f s y <> {} by surj_preimage_not_empty - Thus SING (preimage f s y) by inj_preimage_empty_or_sing - Only-if part: P /\ Q ==> BIJ f s t - Note !y. y IN t ==> (preimage f s y) <> {} - by SING_DEF, NOT_EMPTY_SING - so SURJ f s t by surj_preimage_not_empty - and INJ f s t by inj_preimage_empty_or_sing - Thus BIJ f s t by BIJ_DEF -*) -Theorem bij_preimage_sing: - !f s t. BIJ f s t <=> - over f s t /\ - (!y. y IN t ==> SING (preimage f s y)) -Proof - rw[EQ_IMP_THM] >- - fs[BIJ_DEF, INJ_DEF] >- - metis_tac[BIJ_DEF, surj_preimage_not_empty, inj_preimage_empty_or_sing] >> - `INJ f s t` by metis_tac[inj_preimage_empty_or_sing] >> - `SURJ f s t` by metis_tac[SING_DEF, NOT_EMPTY_SING, surj_preimage_not_empty] >> - simp[BIJ_DEF] -QED - -(* Theorem: FINITE s /\ over f s t ==> - (SURJ f s t <=> !y. y IN t ==> CARD (preimage f s y) <> 0) *) -(* Proof: - Note !y. FINITE (preimage f s y) by preimage_finite - and !y. CARD (preimage f s y) = 0 <=> preimage f s y = {} - by CARD_EQ_0 - The result follows by surj_preimage_not_empty -*) -Theorem surj_iff_preimage_card_not_0: - !f s t. FINITE s /\ over f s t ==> - (SURJ f s t <=> !y. y IN t ==> CARD (preimage f s y) <> 0) -Proof - metis_tac[surj_preimage_not_empty, preimage_finite, CARD_EQ_0] -QED - -(* Theorem: FINITE s /\ over f s t ==> - (INJ f s t <=> !y. y IN t ==> CARD (preimage f s y) <= 1) *) -(* Proof: - Note !y. FINITE (preimage f s y) by preimage_finite - and !y. CARD (preimage f s y) = 0 <=> preimage f s y = {} - by CARD_EQ_0 - and !y. CARD (preimage f s y) = 1 <=> SING (preimage f s y) - by CARD_EQ_1 - The result follows by inj_preimage_empty_or_sing, LE_ONE -*) -Theorem inj_iff_preimage_card_le_1: - !f s t. FINITE s /\ over f s t ==> - (INJ f s t <=> !y. y IN t ==> CARD (preimage f s y) <= 1) -Proof - metis_tac[inj_preimage_empty_or_sing, preimage_finite, CARD_EQ_0, CARD_EQ_1, LE_ONE] -QED - -(* Theorem: FINITE s /\ over f s t ==> - (BIJ f s t <=> !y. y IN t ==> CARD (preimage f s y) = 1) *) -(* Proof: - Note !y. FINITE (preimage f s y) by preimage_finite - and !y. CARD (preimage f s y) = 1 <=> SING (preimage f s y) - by CARD_EQ_1 - The result follows by bij_preimage_sing -*) -Theorem bij_iff_preimage_card_eq_1: - !f s t. FINITE s /\ over f s t ==> - (BIJ f s t <=> !y. y IN t ==> CARD (preimage f s y) = 1) -Proof - metis_tac[bij_preimage_sing, preimage_finite, CARD_EQ_1] -QED - -(* Theorem: FINITE s /\ SURJ f s t ==> - (INJ f s t <=> !e. e IN IMAGE (preimage f s) t ==> CARD e = 1) *) -(* Proof: - If part: INJ f s t /\ x IN t ==> CARD (preimage f s x) = 1 - Note BIJ f s t by BIJ_DEF - and over f s t by BIJ_DEF, INJ_DEF - so CARD (preimage f s x) = 1 by bij_iff_preimage_card_eq_1 - Only-if part: !e. (?x. e = preimage f s x /\ x IN t) ==> CARD e = 1 ==> INJ f s t - Note over f s t by SURJ_DEF - and !x. x IN t ==> ?y. y IN s /\ f y = x by SURJ_DEF - Thus !y. y IN t ==> CARD (preimage f s y) = 1 by IN_IMAGE - so INJ f s t by inj_iff_preimage_card_le_1 -*) -Theorem finite_surj_inj_iff: - !f s t. FINITE s /\ SURJ f s t ==> - (INJ f s t <=> !e. e IN IMAGE (preimage f s) t ==> CARD e = 1) -Proof - rw[EQ_IMP_THM] >- - prove_tac[BIJ_DEF, INJ_DEF, bij_iff_preimage_card_eq_1] >> - fs[SURJ_DEF] >> - `!y. y IN t ==> CARD (preimage f s y) = 1` by metis_tac[] >> - rw[inj_iff_preimage_card_le_1] -QED - - - -(* ------------------------------------------------------------------------- *) - -(* export theory at end *) -val _ = export_theory(); - -(*===========================================================================*) diff --git a/examples/fermat/count/mapCountScript.sml b/examples/fermat/count/mapCountScript.sml index f57b864313..6c0c5335a6 100644 --- a/examples/fermat/count/mapCountScript.sml +++ b/examples/fermat/count/mapCountScript.sml @@ -12,24 +12,10 @@ val _ = new_theory "mapCount"; (* ------------------------------------------------------------------------- *) +open arithmeticTheory pred_setTheory gcdsetTheory numberTheory listTheory + rich_listTheory listRangeTheory combinatoricsTheory; -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - -(* val _ = load "combinatoricsTheory"; *) -open helperCountTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; - -open listTheory rich_listTheory; -open listRangeTheory; -open helperListTheory; - -open necklaceTheory; (* for necklace_def *) -open combinatoricsTheory; - +val _ = temp_overload_on("over", ``\f s t. !x. x IN s ==> f x IN t``); (* ------------------------------------------------------------------------- *) (* Counting of maps between finite sets Documentation *) diff --git a/examples/fermat/count/permutationScript.sml b/examples/fermat/count/permutationScript.sml index aff5247f7e..e537d5d796 100644 --- a/examples/fermat/count/permutationScript.sml +++ b/examples/fermat/count/permutationScript.sml @@ -12,30 +12,23 @@ val _ = new_theory "permutation"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; (* for stripDup *) -(* open dependent theories *) -(* val _ = load "symmetryTheory"; *) -open pred_setTheory arithmeticTheory; -open helperCountTheory; -open helperSetTheory; - -open listTheory rich_listTheory; -open helperListTheory; +open pred_setTheory arithmeticTheory gcdsetTheory numberTheory listTheory + listRangeTheory rich_listTheory combinatoricsTheory; open mapCountTheory; -open combinatoricsTheory; (* Get dependent theories local *) open monoidTheory groupTheory; -open submonoidTheory subgroupTheory; -open monoidMapTheory groupMapTheory; +open subgroupTheory; +open groupMapTheory; open quotientGroupTheory; (* for homo_image_def *) open symmetryTheory; +val _ = temp_overload_on("over", ``\f s t. !x. x IN s ==> f x IN t``); (* ------------------------------------------------------------------------- *) (* Permutation Group Documentation *) diff --git a/examples/fermat/count/symmetryScript.sml b/examples/fermat/count/symmetryScript.sml index 4f989be82b..6e298244a2 100644 --- a/examples/fermat/count/symmetryScript.sml +++ b/examples/fermat/count/symmetryScript.sml @@ -12,27 +12,21 @@ val _ = new_theory "symmetry"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; (* for stripDup *) -(* open dependent theories *) -(* val _ = load "mapCountTheory"; *) -open pred_setTheory arithmeticTheory; -open helperCountTheory; -open helperSetTheory; +open pred_setTheory arithmeticTheory gcdsetTheory numberTheory + combinatoricsTheory; open mapCountTheory; (* for on_def *) -open combinatoricsTheory; -(* Get dependent theories local *) -(* val _ = load "fieldMapTheory"; *) open monoidTheory groupTheory; open ringTheory fieldTheory; -open submonoidTheory subgroupTheory; -open monoidMapTheory groupMapTheory; +open subgroupTheory; +open groupMapTheory; open ringMapTheory fieldMapTheory; +val _ = temp_overload_on("over", ``\f s t. !x. x IN s ==> f x IN t``); (* ------------------------------------------------------------------------- *) (* Symmetry Group Documentation *) diff --git a/examples/fermat/little/FLTactionScript.sml b/examples/fermat/little/FLTactionScript.sml index 46dbbed0e3..7ee0af5c17 100644 --- a/examples/fermat/little/FLTactionScript.sml +++ b/examples/fermat/little/FLTactionScript.sml @@ -35,25 +35,14 @@ val _ = new_theory "FLTaction"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* val _ = load "FLTnecklaceTheory"; *) -open helperNumTheory helperSetTheory; -open arithmeticTheory pred_setTheory; -(* val _ = load "helperFunctionTheory"; *) -open helperFunctionTheory; (* for prime_power_divisor, PRIME_EXP_FACTOR *) +open arithmeticTheory pred_setTheory dividesTheory gcdTheory gcdsetTheory + logrootTheory numberTheory combinatoricsTheory; open cycleTheory; -open necklaceTheory; -(* val _ = load "groupInstancesTheory"; *) -(* val _ = load "groupActionTheory"; *) open groupTheory; open groupActionTheory; -open dividesTheory; (* for divides_def, prime_def *) - - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Action Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/FLTbinomialScript.sml b/examples/fermat/little/FLTbinomialScript.sml index 63cfff82ce..8161d12cc9 100644 --- a/examples/fermat/little/FLTbinomialScript.sml +++ b/examples/fermat/little/FLTbinomialScript.sml @@ -32,18 +32,11 @@ Proof: (* add all dependent libraries for script *) open HolKernel boolLib bossLib Parse; +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory; + (* declare new theory at start *) val _ = new_theory "FLTbinomial"; -(* ------------------------------------------------------------------------- *) - - -(* open dependent theories *) -(* val _ = load "binomialTheory"; *) -open arithmeticTheory; (* for MOD and EXP *) -open dividesTheory; (* for PRIME_POS *) - - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Binomial Documentation *) (* ------------------------------------------------------------------------- *) @@ -97,66 +90,8 @@ open dividesTheory; (* for PRIME_POS *) (* Part 2: General Theory -------------------------------------------------- *) -val PRIME_FACTOR_PROPER = helperNumTheory.PRIME_FACTOR_PROPER; -(* |- !n. 1 < n /\ ~prime n ==> ?p. prime p /\ p < n /\ p divides n *) - -val MULTIPLE_INTERVAL = helperNumTheory.MULTIPLE_INTERVAL; -(* |- !n m. n divides m ==> !x. m - n < x /\ x < m + n /\ n divides x ==> x = m *) - -val PROD_SET_EUCLID = helperSetTheory.PROD_SET_EUCLID; -(* |- !s. FINITE s ==> !p. prime p /\ p divides PROD_SET s ==> ?b. b IN s /\ p divides b *) -(* This is: Generalized Euclid's Lemma. *) - -val PRIME_BIG_NOT_DIVIDES_FACT = helperFunctionTheory.PRIME_BIG_NOT_DIVIDES_FACT; -(* |- !p k. prime p /\ k < p ==> ~(p divides FACT k) *) - -val FACT_EQ_PROD = helperFunctionTheory.FACT_EQ_PROD; -(* |- !n. FACT n = PROD_SET (IMAGE SUC (count n)) *) - -val FACT_REDUCTION = helperFunctionTheory.FACT_REDUCTION; -(* |- !n m. m < n ==> FACT n = PROD_SET (IMAGE SUC (count n DIFF count m)) * FACT m *) -(* That is: n!/m! = product of (m+1) to n *) - (* Part 3: Actual Proof ---------------------------------------------------- *) -(* ------------------------------------------------------------------------- *) -(* Binomial Theorem for prime exponent and modulo. *) -(* ------------------------------------------------------------------------- *) - -val prime_divides_binomials = binomialTheory.prime_divides_binomials; -(* |- !n. prime n ==> 1 < n /\ !k. 0 < k /\ k < n ==> n divides binomial n k *) - -val prime_divisor_property = binomialTheory.prime_divisor_property; -(* |- !n p. 1 < n /\ p < n /\ prime p /\ p divides n ==> - ~(p divides FACT (n - 1) DIV FACT (n - p)) *) - -val divides_binomials_imp_prime = binomialTheory.divides_binomials_imp_prime; -(* !n. 1 < n /\ (!k. 0 < k /\ k < n ==> n divides binomial n k) ==> prime n *) - -val prime_iff_divides_binomials = binomialTheory.prime_iff_divides_binomials; -(* |- !n. prime n <=> 1 < n /\ !k. 0 < k /\ k < n ==> n divides binomial n k *) - -val binomial_range_shift = binomialTheory.binomial_range_shift; -(* |- !n. 0 < n ==> ((!k. 0 < k /\ k < n ==> binomial n k MOD n = 0) <=> - !h. h < PRE n ==> binomial n (SUC h) MOD n = 0) *) - -val binomial_mod_zero = binomialTheory.binomial_mod_zero; -(* |- !n. 0 < n ==> !k. binomial n k MOD n = 0 <=> - !x y. (binomial n k * x ** (n - k) * y ** k) MOD n = 0 *) - -val binomial_range_shift_alt = binomialTheory.binomial_range_shift_alt; -(* |- !n. 0 < n ==> - ((!k. 0 < k /\ k < n ==> !x y. (binomial n k * x ** (n - k) * y ** k) MOD n = 0) <=> - !h. h < PRE n ==> !x y. (binomial n (SUC h) * x ** (n - SUC h) * y ** SUC h) MOD n = 0) *) - -val binomial_mod_zero_alt = binomialTheory.binomial_mod_zero_alt; -(* |- !n. 0 < n ==> - ((!k. 0 < k /\ k < n ==> binomial n k MOD n = 0) <=> - !x y. SUM (GENLIST ((\k. (binomial n k * x ** (n - k) * y ** k) MOD n) o SUC) (PRE n)) = 0) *) - -val binomial_thm_prime = binomialTheory.binomial_thm_prime; -(* |- !p. prime p ==> !x y. (x + y) ** p MOD p = (x ** p + y ** p) MOD p *) - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/FLTeulerScript.sml b/examples/fermat/little/FLTeulerScript.sml index ee49b5a44c..9d7ba349b1 100644 --- a/examples/fermat/little/FLTeulerScript.sml +++ b/examples/fermat/little/FLTeulerScript.sml @@ -42,20 +42,12 @@ val _ = new_theory "FLTeuler"; (* ------------------------------------------------------------------------- *) +open arithmeticTheory pred_setTheory dividesTheory gcdTheory numberTheory + combinatoricsTheory; -(* open dependent theories *) -(* val _ = load "EulerTheory"; *) -open arithmeticTheory pred_setTheory; -open dividesTheory gcdTheory; (* for GCD_0R *) - -open helperNumTheory; (* for MOD_EXP *) - -(* val _ = load "finiteGroupTheory"; *) -(* val _ = load "groupInstancesTheory"; *) open groupTheory; (* for FiniteGroup_def *) open groupOrderTheory; (* for finite_group_Fermat *) - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Number Group Documentation *) (* ------------------------------------------------------------------------- *) @@ -112,58 +104,6 @@ open groupOrderTheory; (* for finite_group_Fermat *) (* Group-theoretic Proof appplied to E^{*}[n]. *) (* ------------------------------------------------------------------------- *) -(* ------------------------------------------------------------------------- *) -(* Relatively prime, or Coprime. *) -(* ------------------------------------------------------------------------- *) - -val coprime_mod = helperFunctionTheory.coprime_mod; -(* |- !m n. 0 < m /\ coprime m n ==> coprime m (n MOD m) *) - -val coprime_sym = helperFunctionTheory.coprime_sym; -(* |- !x y. coprime x y <=> coprime y x *) - -val MOD_NONZERO_WHEN_GCD_ONE = helperFunctionTheory.MOD_NONZERO_WHEN_GCD_ONE; -(* |- !n. 1 < n ==> !x. coprime n x ==> 0 < x /\ 0 < x MOD n *) - -val PRODUCT_WITH_GCD_ONE = helperFunctionTheory.PRODUCT_WITH_GCD_ONE; -(* |- !n x y. coprime n x /\ coprime n y ==> coprime n (x * y) *) - -val MOD_WITH_GCD_ONE = helperFunctionTheory.MOD_WITH_GCD_ONE; -(* |- !n x. 0 < n /\ coprime n x ==> coprime n (x MOD n) *) - -val GCD_DIVIDES = helperFunctionTheory.GCD_DIVIDES; -(* |- !m n. 0 < n /\ 0 < m ==> 0 < gcd n m /\ n MOD gcd n m = 0 /\ m MOD gcd n m = 0 *) - -val GCD_ONE_PROPERTY = helperFunctionTheory.GCD_ONE_PROPERTY; -(* |- !n x. 1 < n /\ coprime n x ==> ?k. (k * x) MOD n = 1 /\ coprime n k *) - -(* ------------------------------------------------------------------------- *) -(* Establish the existence of multiplicative inverse when p is prime. *) -(* ------------------------------------------------------------------------- *) - -val GCD_MOD_MULT_INV = helperFunctionTheory.GCD_MOD_MULT_INV; -(* |- !n x. 1 < n /\ coprime n x /\ 0 < x /\ x < n ==> - ?y. 0 < y /\ y < n /\ coprime n y /\ (y * x) MOD n = 1 *) - -(* Convert this into an existence definition *) -val GEN_MULT_INV_DEF = helperFunctionTheory.GEN_MULT_INV_DEF; -(* |- !n x. 1 < n /\ coprime n x /\ 0 < x /\ x < n ==> - 0 < GCD_MOD_MUL_INV n x /\ GCD_MOD_MUL_INV n x < n /\ - coprime n (GCD_MOD_MUL_INV n x) /\ (GCD_MOD_MUL_INV n x * x) MOD n = 1 *) - -(* ------------------------------------------------------------------------- *) -(* Euler's set and totient function *) -(* ------------------------------------------------------------------------- *) - -val Euler_def = EulerTheory.Euler_def; -(* |- !n. Euler n = {i | 0 < i /\ i < n /\ coprime n i} *) - -val totient_def = EulerTheory.totient_def; -(* |- !n. totient n = CARD (Euler n) *) - -val Euler_card_prime = EulerTheory.Euler_card_prime; -(* |- !p. prime p ==> totient p = p - 1 *) - (* ------------------------------------------------------------------------- *) (* Euler's group of coprimes. *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/FLTfixedpointScript.sml b/examples/fermat/little/FLTfixedpointScript.sml index 302b2cb0d4..7f3edba1d2 100644 --- a/examples/fermat/little/FLTfixedpointScript.sml +++ b/examples/fermat/little/FLTfixedpointScript.sml @@ -31,14 +31,10 @@ val _ = new_theory "FLTfixedpoint"; (* ------------------------------------------------------------------------- *) - (* open dependent theories *) -(* val _ = load "FLTactionTheory"; *) -open helperNumTheory helperSetTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for PRIME_POS *) +open arithmeticTheory pred_setTheory dividesTheory numberTheory + combinatoricsTheory; -open necklaceTheory; open cycleTheory; (* val _ = load "groupInstancesTheory"; *) @@ -46,7 +42,6 @@ open cycleTheory; open groupTheory; open groupActionTheory; - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Action Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/FLTgroupScript.sml b/examples/fermat/little/FLTgroupScript.sml index 7af727a597..2c83e45a15 100644 --- a/examples/fermat/little/FLTgroupScript.sml +++ b/examples/fermat/little/FLTgroupScript.sml @@ -37,22 +37,13 @@ which is Euler's generalization of Fermat's Little Theorem. (* add all dependent libraries for script *) open HolKernel boolLib bossLib Parse; -(* declare new theory at start *) -val _ = new_theory "FLTgroup"; - -(* ------------------------------------------------------------------------- *) - +open arithmeticTheory pred_setTheory dividesTheory numberTheory + combinatoricsTheory; -(* open dependent theories *) -(* val _ = load "dividesTheory"; *) -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for PRIME_POS *) - -(* val _ = load "finiteGroupTheory"; *) -(* val _ = load "groupInstancesTheory"; *) open groupTheory; (* for FiniteGroup_def *) open groupOrderTheory; (* for finite_group_Fermat *) +val _ = new_theory "FLTgroup"; (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Number Group Documentation *) @@ -99,22 +90,6 @@ open groupOrderTheory; (* for finite_group_Fermat *) (* Establish the existence of multiplicative inverse when p is prime. *) (* ------------------------------------------------------------------------- *) -val EUCLID_LEMMA = helperNumTheory.EUCLID_LEMMA; -(* |- !p x y. prime p ==> ((x * y) MOD p = 0 <=> x MOD p = 0 \/ y MOD p = 0) -[Euclid's Lemma in MOD notation] -A prime divides a product iff the prime divides a factor. *) - -val MOD_MULT_INV_EXISTS = helperNumTheory.MOD_MULT_INV_EXISTS; -(* |- !p x. prime p /\ 0 < x /\ x < p ==> - ?y. 0 < y /\ y < p /\ ((y * x) MOD p = 1) -[Existence of Inverse] For prime p, 0 < x < p ==> ?y. (y * x) MOD p = 1 *) - -(* Convert this into an existence definition *) -val MOD_MULT_INV_DEF = helperNumTheory.MOD_MULT_INV_DEF; -(* |- !p x. prime p /\ 0 < x /\ x < p ==> - 0 < MOD_MULT_INV p x /\ MOD_MULT_INV p x < p /\ - (MOD_MULT_INV p x * x) MOD p = 1 *) - (* Part 2: General Theory -------------------------------------------------- *) (* ------------------------------------------------------------------------- *) @@ -125,18 +100,6 @@ val MOD_MULT_INV_DEF = helperNumTheory.MOD_MULT_INV_DEF; (* Residue -- a close-relative of COUNT *) (* ------------------------------------------------------------------------- *) -val residue_def = EulerTheory.residue_def; -(* |- !n. residue n = {i | 0 < i /\ i < n} *) - -val residue_count = EulerTheory.residue_count; -(* |- !n. 0 < n ==> count n = 0 INSERT residue n *) - -val residue_finite = EulerTheory.residue_finite; -(* |- !n. FINITE (residue n) *) - -val residue_card = EulerTheory.residue_card; -(* |- !n. 0 < n ==> CARD (residue n) = n - 1 *) - (* ------------------------------------------------------------------------- *) (* The Group Z^{*}[p] = Multiplication Modulo p, for prime p. *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/FLTnecklaceScript.sml b/examples/fermat/little/FLTnecklaceScript.sml index aa095879ce..f49c6158be 100644 --- a/examples/fermat/little/FLTnecklaceScript.sml +++ b/examples/fermat/little/FLTnecklaceScript.sml @@ -31,20 +31,11 @@ val _ = new_theory "FLTnecklace"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* val _ = load "patternTheory"; *) -open helperNumTheory helperSetTheory; -open arithmeticTheory pred_setTheory; +open arithmeticTheory dividesTheory logrootTheory gcdTheory pred_setTheory + numberTheory combinatoricsTheory; open cycleTheory patternTheory; -(* val _ = load "necklaceTheory"; *) -open necklaceTheory; -open dividesTheory; (* for PRIME_POS *) -open gcdTheory; (* for PRIME_GCD *) - - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by necklace Documentation *) (* ------------------------------------------------------------------------- *) @@ -1193,7 +1184,6 @@ Proof metis_tac[DIVIDES_MOD_0, MOD_EQ] QED - (* ------------------------------------------------------------------------- *) (* export theory at end *) diff --git a/examples/fermat/little/FLTnumberScript.sml b/examples/fermat/little/FLTnumberScript.sml index 715618a033..139f2b9465 100644 --- a/examples/fermat/little/FLTnumberScript.sml +++ b/examples/fermat/little/FLTnumberScript.sml @@ -76,18 +76,8 @@ val _ = new_theory "FLTnumber"; (* ------------------------------------------------------------------------- *) - -(* Get dependent theories in lib *) -(* val _ = load "helperFunctionTheory"; *) -open helperNumTheory helperSetTheory; -open arithmeticTheory pred_setTheory; -open helperFunctionTheory; (* for FACT_0, FACT_MOD_PRIME *) - -open dividesTheory; (* for PRIME_POS, ONE_LT_PRIME *) - -(* val _ = load "EulerTheory"; *) -open EulerTheory; (* for residue_def *) - +open arithmeticTheory pred_setTheory dividesTheory gcdTheory numberTheory + combinatoricsTheory; (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Number Theory Documentation *) diff --git a/examples/fermat/little/FLTpetersenScript.sml b/examples/fermat/little/FLTpetersenScript.sml index 7782dd91b8..7f54412bd1 100644 --- a/examples/fermat/little/FLTpetersenScript.sml +++ b/examples/fermat/little/FLTpetersenScript.sml @@ -31,19 +31,12 @@ val _ = new_theory "FLTpetersen"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* val _ = load "FLTactionTheory"; *) -open helperNumTheory helperSetTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for PRIME_POS *) - -open necklaceTheory; (* for multicoloured_finite *) +open arithmeticTheory dividesTheory gcdTheory logrootTheory numberTheory; +open pred_setTheory combinatoricsTheory; open groupTheory; open groupActionTheory; - (* ------------------------------------------------------------------------- *) (* Fermat's Little Theorem by Action Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/little/Holmakefile b/examples/fermat/little/Holmakefile index 77830c8a87..f6375cb56f 100644 --- a/examples/fermat/little/Holmakefile +++ b/examples/fermat/little/Holmakefile @@ -1,7 +1,5 @@ # prefix to HOL examples LOC_PREFIX = $(HOLDIR)/examples -PRE_INCLUDES = $(LOC_PREFIX)/algebra/ring - -ALGEBRA_INCLUDES = lib monoid group +ALGEBRA_INCLUDES = group ring INCLUDES = $(patsubst %,$(LOC_PREFIX)/algebra/%,$(ALGEBRA_INCLUDES)) diff --git a/examples/fermat/little/cycleScript.sml b/examples/fermat/little/cycleScript.sml index 9f951048b7..0f0e72d562 100644 --- a/examples/fermat/little/cycleScript.sml +++ b/examples/fermat/little/cycleScript.sml @@ -43,14 +43,9 @@ val _ = new_theory "cycle"; (* ------------------------------------------------------------------------- *) - (* open dependent theories *) -(* val _ = load "helperFunctionTheory"; *) -open helperListTheory; (* for DROP_SUC, TAKE_SUC *) -open arithmeticTheory pred_setTheory listTheory; - -open gcdTheory; (* for GCD_0R, LINEAR_GCD *) - +open arithmeticTheory gcdTheory pred_setTheory listTheory rich_listTheory + combinatoricsTheory; (* ------------------------------------------------------------------------- *) (* Cycle Theory Documentation *) diff --git a/examples/fermat/little/necklaceScript.sml b/examples/fermat/little/necklaceScript.sml deleted file mode 100644 index 78a0318fd9..0000000000 --- a/examples/fermat/little/necklaceScript.sml +++ /dev/null @@ -1,1033 +0,0 @@ -(* ------------------------------------------------------------------------- *) -(* Necklace Theory - monocoloured and multicoloured. *) -(* ------------------------------------------------------------------------- *) - -(* - -Necklace Theory -=============== - -Consider the set N of necklaces of length n (i.e. with number of beads = n) -with a colors (i.e. the number of bead colors = a). A linear picture of such -a necklace is: - -+--+--+--+--+--+--+--+ -|2 |4 |0 |3 |1 |2 |3 | p = 7, with (lots of) beads of a = 5 colors: 01234. -+--+--+--+--+--+--+--+ - -Since a bead can have any of the a colors, and there are n beads in total, - -Number of such necklaces = CARD N = a*a*...*a = a^n. - -There is only 1 necklace of pure color A, 1 necklace with pure color B, etc. - -Number of monocoloured necklaces = a = CARD S, where S = monocoloured necklaces. - -So, N = S UNION M, where M = multicoloured necklaces (i.e. more than one color). - -Since S and M are disjoint, CARD M = CARD N - CARD S = a^n - a. - -*) - -(*===========================================================================*) - -(*===========================================================================*) - -(* add all dependent libraries for script *) -open HolKernel boolLib bossLib Parse; - -(* declare new theory at start *) -val _ = new_theory "necklace"; - -(* ------------------------------------------------------------------------- *) - - -(* open dependent theories *) -(* val _ = load "helperFunctionTheory"; *) -open arithmeticTheory pred_setTheory listTheory; -open helperNumTheory helperSetTheory; -open helperListTheory; (* for LENGTH_NON_NIL, LIST_TO_SET_SING_IFF *) - - -(* ------------------------------------------------------------------------- *) -(* Necklace Theory Documentation *) -(* ------------------------------------------------------------------------- *) -(* Overloading: -*) -(* Definitions and Theorems (# are exported, ! are in compute): - - Necklace: - necklace_def |- !n a. necklace n a = - {ls | LENGTH ls = n /\ set ls SUBSET count a} - necklace_element |- !n a ls. ls IN necklace n a <=> - LENGTH ls = n /\ set ls SUBSET count a - necklace_length |- !n a ls. ls IN necklace n a ==> LENGTH ls = n - necklace_colors |- !n a ls. ls IN necklace n a ==> set ls SUBSET count a - necklace_property |- !n a ls. ls IN necklace n a ==> - LENGTH ls = n /\ set ls SUBSET count a - necklace_0 |- !a. necklace 0 a = {[]} - necklace_empty |- !n. 0 < n ==> (necklace n 0 = {}) - necklace_not_nil |- !n a ls. 0 < n /\ ls IN necklace n a ==> ls <> [] - necklace_suc |- !n a. necklace (SUC n) a = - IMAGE (\(c,ls). c::ls) (count a CROSS necklace n a) -! necklace_eqn |- !n a. necklace n a = - if n = 0 then {[]} - else IMAGE (\(c,ls). c::ls) (count a CROSS necklace (n - 1) a) - necklace_1 |- !a. necklace 1 a = {[e] | e IN count a} - necklace_finite |- !n a. FINITE (necklace n a) - necklace_card |- !n a. CARD (necklace n a) = a ** n - - Mono-colored necklace: - monocoloured_def |- !n a. monocoloured n a = - {ls | ls IN necklace n a /\ (ls <> [] ==> SING (set ls))} - monocoloured_element - |- !n a ls. ls IN monocoloured n a <=> - ls IN necklace n a /\ (ls <> [] ==> SING (set ls)) - monocoloured_necklace |- !n a ls. ls IN monocoloured n a ==> ls IN necklace n a - monocoloured_subset |- !n a. monocoloured n a SUBSET necklace n a - monocoloured_finite |- !n a. FINITE (monocoloured n a) - monocoloured_0 |- !a. monocoloured 0 a = {[]} - monocoloured_1 |- !a. monocoloured 1 a = necklace 1 a - necklace_1_monocoloured - |- !a. necklace 1 a = monocoloured 1 a - monocoloured_empty|- !n. 0 < n ==> monocoloured n 0 = {} - monocoloured_mono |- !n. monocoloured n 1 = necklace n 1 - monocoloured_suc |- !n a. 0 < n ==> - monocoloured (SUC n) a = IMAGE (\ls. HD ls::ls) (monocoloured n a) - monocoloured_0_card |- !a. CARD (monocoloured 0 a) = 1 - monocoloured_card |- !n a. 0 < n ==> CARD (monocoloured n a) = a -! monocoloured_eqn |- !n a. monocoloured n a = - if n = 0 then {[]} - else IMAGE (\c. GENLIST (K c) n) (count a) - monocoloured_card_eqn |- !n a. CARD (monocoloured n a) = if n = 0 then 1 else a - - Multi-colored necklace: - multicoloured_def |- !n a. multicoloured n a = necklace n a DIFF monocoloured n a - multicoloured_element |- !n a ls. ls IN multicoloured n a <=> - ls IN necklace n a /\ ls <> [] /\ ~SING (set ls) - multicoloured_necklace|- !n a ls. ls IN multicoloured n a ==> ls IN necklace n a - multicoloured_subset |- !n a. multicoloured n a SUBSET necklace n a - multicoloured_finite |- !n a. FINITE (multicoloured n a) - multicoloured_0 |- !a. multicoloured 0 a = {} - multicoloured_1 |- !a. multicoloured 1 a = {} - multicoloured_n_0 |- !n. multicoloured n 0 = {} - multicoloured_n_1 |- !n. multicoloured n 1 = {} - multicoloured_empty |- !n. multicoloured n 0 = {} /\ multicoloured n 1 = {} - multi_mono_disjoint |- !n a. DISJOINT (multicoloured n a) (monocoloured n a) - multi_mono_exhaust |- !n a. necklace n a = multicoloured n a UNION monocoloured n a - multicoloured_card |- !n a. 0 < n ==> (CARD (multicoloured n a) = a ** n - a) - multicoloured_card_eqn|- !n a. CARD (multicoloured n a) = if n = 0 then 0 else a ** n - a - multicoloured_nonempty|- !n a. 1 < n /\ 1 < a ==> multicoloured n a <> {} - multicoloured_not_monocoloured - |- !n a ls. ls IN multicoloured n a ==> ls NOTIN monocoloured n a - multicoloured_not_monocoloured_iff - |- !n a ls. ls IN necklace n a ==> - (ls IN multicoloured n a <=> ls NOTIN monocoloured n a) - multicoloured_or_monocoloured - |- !n a ls. ls IN necklace n a ==> - ls IN multicoloured n a \/ ls IN monocoloured n a -*) - - -(* ------------------------------------------------------------------------- *) -(* Helper Theorems. *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) -(* Necklace *) -(* ------------------------------------------------------------------------- *) - -(* Define necklaces as lists of length n, i.e. with n beads, in a colors. *) -Definition necklace_def[nocompute]: - necklace n a = {ls | LENGTH ls = n /\ (set ls) SUBSET (count a) } -End -(* Note: use [nocompute] as this is not effective. *) - -(* Theorem: ls IN necklace n a <=> (LENGTH ls = n /\ (set ls) SUBSET (count a)) *) -(* Proof: by necklace_def *) -Theorem necklace_element: - !n a ls. ls IN necklace n a <=> (LENGTH ls = n /\ (set ls) SUBSET (count a)) -Proof - simp[necklace_def] -QED - -(* Theorem: ls IN (necklace n a) ==> LENGTH ls = n *) -(* Proof: by necklace_def *) -Theorem necklace_length: - !n a ls. ls IN (necklace n a) ==> LENGTH ls = n -Proof - simp[necklace_def] -QED - -(* Theorem: ls IN (necklace n a) ==> set ls SUBSET count a *) -(* Proof: by necklace_def *) -Theorem necklace_colors: - !n a ls. ls IN (necklace n a) ==> set ls SUBSET count a -Proof - simp[necklace_def] -QED - -(* Idea: If ls in (necklace n a), LENGTH ls = n and colors in count a. *) - -(* Theorem: ls IN (necklace n a) ==> LENGTH ls = n /\ set ls SUBSET count a *) -(* Proof: by necklace_def *) -Theorem necklace_property: - !n a ls. ls IN (necklace n a) ==> LENGTH ls = n /\ set ls SUBSET count a -Proof - simp[necklace_def] -QED - -(* ------------------------------------------------------------------------- *) -(* Know the necklaces. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: zero-length necklaces of whatever colors is the set of NIL. *) - -(* Theorem: necklace 0 a = {[]} *) -(* Proof: - necklace 0 a - = {ls | (LENGTH ls = 0) /\ (set ls) SUBSET (count a) } by necklace_def - = {ls | ls = [] /\ (set []) SUBSET (count a) } by LENGTH_NIL - = {ls | ls = [] /\ [] SUBSET (count a) } by LIST_TO_SET - = {[]} by EMPTY_SUBSET -*) -Theorem necklace_0: - !a. necklace 0 a = {[]} -Proof - rw[necklace_def, EXTENSION] >> - metis_tac[LIST_TO_SET, EMPTY_SUBSET] -QED - -(* Idea: necklaces with some length but 0 colors is EMPTY. *) - -(* Theorem: 0 < n ==> (necklace n 0 = {}) *) -(* Proof: - necklace n 0 - = {ls | LENGTH ls = n /\ (set ls) SUBSET (count 0) } by necklace_def - = {ls | LENGTH ls = n /\ (set ls) SUBSET {} by COUNT_0 - = {ls | LENGTH ls = n /\ (set ls = {}) } by SUBSET_EMPTY - = {ls | LENGTH ls = n /\ (ls = []) } by LIST_TO_SET_EQ_EMPTY - = {} by LENGTH_NIL, 0 < n -*) -Theorem necklace_empty: - !n. 0 < n ==> (necklace n 0 = {}) -Proof - rw[necklace_def, EXTENSION] -QED - -(* Idea: A necklace of length n <> 0 is non-NIL. *) - -(* Theorem: 0 < n /\ ls IN (necklace n a) ==> ls <> [] *) -(* Proof: - By contradiction, suppose ls = []. - Then n = LENGTH ls by necklace_element - = LENGTH [] = 0 by LENGTH_NIL - This contradicts 0 < n. -*) -Theorem necklace_not_nil: - !n a ls. 0 < n /\ ls IN (necklace n a) ==> ls <> [] -Proof - rw[necklace_def] >> - metis_tac[LENGTH_NON_NIL] -QED - -(* ------------------------------------------------------------------------- *) -(* To show: (necklace n a) is FINITE. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: Relate (necklace (n+1) a) to (necklace n a) for induction. *) - -(* Theorem: necklace (SUC n) a = - IMAGE (\(c, ls). c :: ls) (count a CROSS necklace n a) *) -(* Proof: - By necklace_def, EXTENSION, this is to show: - (1) LENGTH x = SUC n /\ set x SUBSET count a ==> - ?h t. (x = h::t) /\ h < a /\ (LENGTH t = n) /\ set t SUBSET count a - Note SUC n <> 0 by SUC_NOT_ZERO - so ?h t. x = h::t by list_CASES - Take these h, t, true by LENGTH, MEM - (2) h < a /\ set t SUBSET count a ==> x < a ==> LENGTH (h::t) = SUC (LENGTH t) - This is true by LENGTH - (3) h < a /\ set t SUBSET count a ==> set (h::t) SUBSET count a - Note set (h::t) c <=> - (c = h) \/ set t c by LIST_TO_SET_DEF - If c = h, h < a - ==> h IN count a by IN_COUNT - If set t c, set t SUBSET count a - ==> c IN count a by SUBSET_DEF - Thus set (h::t) SUBSET count a by SUBSET_DEF -*) -Theorem necklace_suc: - !n a. necklace (SUC n) a = - IMAGE (\(c, ls). c :: ls) (count a CROSS necklace n a) -Proof - rw[necklace_def, EXTENSION] >> - rw[pairTheory.EXISTS_PROD, EQ_IMP_THM] >| [ - `SUC n <> 0` by decide_tac >> - `?h t. x = h::t` by metis_tac[LENGTH_NIL, list_CASES] >> - qexists_tac `h` >> - qexists_tac `t` >> - fs[], - simp[], - fs[] - ] -QED - -(* Idea: display the necklaces. *) - -(* Theorem: necklace n a = - if n = 0 then {[]} - else IMAGE (\(c,ls). c::ls) (count a CROSS necklace (n - 1) a) *) -(* Proof: by necklace_0, necklace_suc. *) -Theorem necklace_eqn[compute]: - !n a. necklace n a = - if n = 0 then {[]} - else IMAGE (\(c,ls). c::ls) (count a CROSS necklace (n - 1) a) -Proof - rw[necklace_0] >> - metis_tac[necklace_suc, num_CASES, SUC_SUB1] -QED - -(* -> EVAL ``necklace 3 2``; -= {[1; 1; 1]; [1; 1; 0]; [1; 0; 1]; [1; 0; 0]; [0; 1; 1]; [0; 1; 0]; [0; 0; 1]; [0; 0; 0]} -> EVAL ``necklace 2 3``; -= {[2; 2]; [2; 1]; [2; 0]; [1; 2]; [1; 1]; [1; 0]; [0; 2]; [0; 1]; [0; 0]} -*) - -(* Idea: Unit-length necklaces are singletons from (count a). *) - -(* Theorem: necklace 1 a = {[e] | e IN count a} *) -(* Proof: - Let f = (\(c,ls). c::ls). - necklace 1 a - = necklace (SUC 0) a by ONE - = IMAGE f ((count a) CROSS (necklace 0 a)) by necklace_suc - = IMAGE f ((count a) CROSS {[]}) by necklace_0 - = {[e] | e IN count a} by EXTENSION -*) -Theorem necklace_1: - !a. necklace 1 a = {[e] | e IN count a} -Proof - rewrite_tac[ONE] >> - rw[necklace_suc, necklace_0, pairTheory.EXISTS_PROD, EXTENSION] -QED - -(* Idea: The set of (necklace n a) is finite. *) - -(* Theorem: FINITE (necklace n a) *) -(* Proof: - By induction on n. - Base: FINITE (necklace 0 a) - Note necklace 0 a = {[]} by necklace_0 - and FINITE {[]} by FINITE_SING - Step: FINITE (necklace n a) ==> FINITE (necklace (SUC n) a) - Let f = (\(c, ls). c :: ls), b = count a, c = necklace n a. - Note necklace (SUC n) a - = IMAGE f (b CROSS c) by necklace_suc - and FINITE b by FINITE_COUNT - and FINITE c by induction hypothesis - so FINITE (b CROSS c) by FINITE_CROSS - Thus FINITE (necklace (SUC n) a) by IMAGE_FINITE -*) -Theorem necklace_finite: - !n a. FINITE (necklace n a) -Proof - rpt strip_tac >> - Induct_on `n` >- - simp[necklace_0] >> - simp[necklace_suc] -QED - -(* ------------------------------------------------------------------------- *) -(* To show: CARD (necklace n a) = a^n. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: size of (necklace n a) = a^n. *) - -(* Theorem: CARD (necklace n a) = a ** n *) -(* Proof: - By induction on n. - Base: CARD (necklace 0 a) = a ** 0 - CARD (necklace 0 a) - = CARD {[]} by necklace_0 - = 1 by CARD_SING - = a ** 0 by EXP_0 - Step: CARD (necklace n a) = a ** n ==> - CARD (necklace (SUC n) a) = a ** SUC n - Let f = (\(c, ls). c :: ls), b = count a, c = necklace n a. - Note FINITE b by FINITE_COUNT - and FINITE c by necklace_finite - and FINITE (b CROSS c) by FINITE_CROSS - Also INJ f (b CROSS c) univ(:num list) by INJ_DEF, CONS_11 - CARD (necklace (SUC n) a) - = CARD (IMAGE f (b CROSS c)) by necklace_suc - = CARD (b CROSS c) by INJ_CARD_IMAGE_EQN - = CARD b * CARD c by CARD_CROSS - = a * CARD c by CARD_COUNT - = a * a ** n by induction hypothesis - = a ** SUC n by EXP -*) -Theorem necklace_card: - !n a. CARD (necklace n a) = a ** n -Proof - rpt strip_tac >> - Induct_on `n` >- - simp[necklace_0] >> - qabbrev_tac `f = (\(c:num, ls:num list). c :: ls)` >> - qabbrev_tac `b = count a` >> - qabbrev_tac `c = necklace n a` >> - `FINITE b` by rw[FINITE_COUNT, Abbr`b`] >> - `FINITE c` by rw[necklace_finite, Abbr`c`] >> - `necklace (SUC n) a = IMAGE f (b CROSS c)` by rw[necklace_suc, Abbr`f`, Abbr`b`, Abbr`c`] >> - `INJ f (b CROSS c) univ(:num list)` by rw[INJ_DEF, pairTheory.FORALL_PROD, Abbr`f`] >> - `FINITE (b CROSS c)` by rw[FINITE_CROSS] >> - `CARD (necklace (SUC n) a) = CARD (b CROSS c)` by rw[INJ_CARD_IMAGE_EQN] >> - `_ = CARD b * CARD c` by rw[CARD_CROSS] >> - `_ = a * a ** n` by fs[Abbr`b`, Abbr`c`] >> - simp[EXP] -QED - -(* ------------------------------------------------------------------------- *) -(* Mono-colored necklace - necklace with a single color. *) -(* ------------------------------------------------------------------------- *) - -(* Define mono-colored necklace *) -Definition monocoloured_def[nocompute]: - monocoloured n a = - {ls | ls IN necklace n a /\ (ls <> [] ==> SING (set ls)) } -End -(* Note: use [nocompute] as this is not effective. *) - -(* Theorem: ls IN monocoloured n a <=> - ls IN necklace n a /\ (ls <> [] ==> SING (set ls)) *) -(* Proof: by monocoloured_def *) -Theorem monocoloured_element: - !n a ls. ls IN monocoloured n a <=> - ls IN necklace n a /\ (ls <> [] ==> SING (set ls)) -Proof - simp[monocoloured_def] -QED - -(* ------------------------------------------------------------------------- *) -(* Know the Mono-coloured necklaces. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: A monocoloured necklace is indeed a necklace. *) - -(* Theorem: ls IN monocoloured n a ==> ls IN necklace n a *) -(* Proof: by monocoloured_def *) -Theorem monocoloured_necklace: - !n a ls. ls IN monocoloured n a ==> ls IN necklace n a -Proof - simp[monocoloured_def] -QED - -(* Idea: The monocoloured set is subset of necklace set. *) - -(* Theorem: (monocoloured n a) SUBSET (necklace n a) *) -(* Proof: by monocoloured_necklace, SUBSET_DEF *) -Theorem monocoloured_subset: - !n a. (monocoloured n a) SUBSET (necklace n a) -Proof - simp[monocoloured_necklace, SUBSET_DEF] -QED - -(* Idea: The monocoloured set is FINITE. *) - -(* Theorem: FINITE (monocoloured n a) *) -(* Proof: - Note (monocoloured n a) SUBSET (necklace n a) by monocoloured_subset - and FINITE (necklace n a) by necklace_finite - so FINITE (monocoloured n a) by SUBSET_FINITE -*) -Theorem monocoloured_finite: - !n a. FINITE (monocoloured n a) -Proof - metis_tac[monocoloured_subset, necklace_finite, SUBSET_FINITE] -QED - -(* Idea: Zero-length monocoloured set is singleton NIL. *) - -(* Theorem: monocoloured 0 a = {[]} *) -(* Proof: - monocoloured 0 a - = {ls | ls IN necklace 0 a /\ (ls <> [] ==> SING (set ls)) } by monocoloured_def - = {ls | ls IN {[]} /\ (ls <> [] ==> SING (set ls)) } by necklace_0 - = {[]} by IN_SING -*) -Theorem monocoloured_0: - !a. monocoloured 0 a = {[]} -Proof - rw[monocoloured_def, necklace_0, EXTENSION, EQ_IMP_THM] -QED - -(* Idea: Unit-length monocoloured set are necklaces of length 1. *) - -(* Theorem: monocoloured 1 a = necklace 1 a *) -(* Proof: - By necklace_def, monocoloured_def, EXTENSION, - this is to show: - (LENGTH x = 1) /\ set x SUBSET count a /\ (x <> [] ==> SING (set x)) <=> - (LENGTH x = 1) /\ set x SUBSET count a - This is true by LIST_TO_SET_SING -*) -Theorem monocoloured_1: - !a. monocoloured 1 a = necklace 1 a -Proof - rw[necklace_def, monocoloured_def, EXTENSION] >> - metis_tac[LIST_TO_SET_SING] -QED - -(* Idea: Unit-length necklaces are monocoloured. *) - -(* Theorem: necklace 1 a = monocoloured 1 a *) -(* Proof: by monocoloured_1 *) -Theorem necklace_1_monocoloured: - !a. necklace 1 a = monocoloured 1 a -Proof - simp[monocoloured_1] -QED - -(* Idea: Some non-NIL necklaces are monocoloured. *) - -(* Theorem: 0 < n ==> monocoloured n 0 = {} *) -(* Proof: - Note (monocoloured n 0) SUBSET (necklace n 0) by monocoloured_subset - but necklace n 0 = {} by necklace_empty - so monocoloured n 0 = {} by SUBSET_EMPTY -*) -Theorem monocoloured_empty: - !n. 0 < n ==> monocoloured n 0 = {} -Proof - metis_tac[monocoloured_subset, necklace_empty, SUBSET_EMPTY] -QED - -(* Idea: One-colour necklaces are monocoloured. *) - -(* Theorem: monocoloured n 1 = necklace n 1 *) -(* Proof: - By monocoloured_def, necklace_def, EXTENSION, - this is to show: - set x SUBSET count 1 /\ x <> [] ==> SING (set x) - Note count 1 = {0} by COUNT_1 - and set x <> {} by LIST_TO_SET - so set x = {0} by SUBSET_SING_IFF - or SING (set x) by SING_DEF -*) -Theorem monocoloured_mono: - !n. monocoloured n 1 = necklace n 1 -Proof - rw[monocoloured_def, necklace_def, EXTENSION, EQ_IMP_THM] >> - fs[COUNT_1] >> - `set x = {0}` by fs[SUBSET_SING_IFF] >> - simp[] -QED - -(* ------------------------------------------------------------------------- *) -(* To show: CARD (monocoloured n a) = a. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: Relate (monocoloured (SUC n) a) to (monocoloured n a) for induction. *) - -(* Theorem: 0 < n ==> (monocoloured (SUC n) a = - IMAGE (\ls. HD ls :: ls) (monocoloured n a)) *) -(* Proof: - By monocoloured_def, necklace_def, EXTENSION, this is to show: - (1) 0 < n /\ LENGTH x = SUC n /\ set x SUBSET count a /\ x <> [] ==> SING (set x) ==> - ?ls. (x = HD ls::ls) /\ (LENGTH ls = n /\ set ls SUBSET count a) /\ - (ls <> [] ==> SING (set ls)) - Note SUC n <> 0 by SUC_NOT_ZERO - so x <> [] by LENGTH_NIL - ==> ?h t. x = h::t by list_CASES - and LENGTH t = n by LENGTH - but t <> [] by LENGTH_NON_NIL, 0 < n - so ?k p. t = k::p by list_CASES - Thus x = h::k::p by above - Now h IN set x by MEM - and k IN set x by MEM, SUBSET_DEF - so h = k by IN_SING, SING (set x) - Let ls = t, - then set ls SUBSET count a by MEM, SUBSET_DEF - and SING (set ls) by LIST_TO_SET_DEF - (2) 0 < LENGTH ls /\ set ls SUBSET count a /\ ls <> [] ==> SING (set ls) ==> - LENGTH (HD ls::ls) = SUC (LENGTH ls) - This is true by LENGTH - (3) 0 < LENGTH ls /\ set ls SUBSET count a /\ ls <> [] ==> SING (set ls) ==> - set (HD ls::ls) SUBSET count a - Note ls <> [] by LENGTH_NON_NIL - so ?h t. ls = h::t by list_CASES - Also set (h::ls) x <=> - (x = h) \/ set t x by LIST_TO_SET_DEF - Thus set (h::ls) SUBSET count a by SUBSET_DEF - (4) 0 < LENGTH ls /\ set ls SUBSET count a /\ ls <> [] ==> SING (set ls) ==> - SING (set (HD ls::ls)) - Note ls <> [] by LENGTH_NON_NIL - so ?h t. ls = h::t by list_CASES - Also set (h::ls) x <=> - (x = h) \/ set t x by LIST_TO_SET_DEF - Thus SING (set (h::ls)) by SUBSET_DEF -*) -Theorem monocoloured_suc: - !n a. 0 < n ==> (monocoloured (SUC n) a = - IMAGE (\ls. HD ls :: ls) (monocoloured n a)) -Proof - rw[monocoloured_def, necklace_def, EXTENSION] >> - rw[pairTheory.EXISTS_PROD, EQ_IMP_THM] >| [ - `SUC n <> 0` by decide_tac >> - `x <> [] /\ ?h t. x = h::t` by metis_tac[LENGTH_NIL, list_CASES] >> - `LENGTH t = n` by fs[] >> - `t <> []` by metis_tac[LENGTH_NON_NIL] >> - `h IN set x` by fs[] >> - `?k p. t = k::p` by metis_tac[list_CASES] >> - `HD t IN set x` by rfs[SUBSET_DEF] >> - `HD t = h` by metis_tac[SING_DEF, IN_SING] >> - qexists_tac `t` >> - fs[], - simp[], - `ls <> [] /\ ?h t. ls = h::t` by metis_tac[LENGTH_NON_NIL, list_CASES] >> - fs[], - `ls <> [] /\ ?h t. ls = h::t` by metis_tac[LENGTH_NON_NIL, list_CASES] >> - fs[] - ] -QED - -(* Idea: size of (monocoloured 0 a) = 1. *) - -(* Theorem: CARD (monocoloured 0 a) = 1 *) -(* Proof: - Note monocoloured 0 a = {[]} by monocoloured_0 - so CARD (monocoloured 0 a) = 1 by CARD_SING -*) -Theorem monocoloured_0_card: - !a. CARD (monocoloured 0 a) = 1 -Proof - simp[monocoloured_0] -QED - -(* Idea: size of (monocoloured n a) = a. *) - -(* Theorem: 0 < n ==> CARD (monocoloured n a) = a *) -(* Proof: - By induction on n. - Base: 0 < 0 ==> (CARD (monocoloured 0 a) = a) - True by 0 < 0 = F. - Step: 0 < n ==> CARD (monocoloured n a) = a ==> - 0 < SUC n ==> (CARD (monocoloured (SUC n) a) = a) - If n = 0, - CARD (monocoloured (SUC 0) a) - = CARD (monocoloured 1 a) by ONE - = CARD (necklace 1 a) by monocoloured_1 - = a ** 1 by necklace_card - = a by EXP_1 - If n <> 0, then 0 < n. - Let f = (\ls. HD ls :: ls). - Then INJ f (monocoloured n a) - univ(:num list) by INJ_DEF, CONS_11 - and FINITE (monocoloured n a) by monocoloured_finite - CARD (monocoloured (SUC n) a) - = CARD (IMAGE f (monocoloured n a)) by monocoloured_suc - = CARD (monocoloured n a) by INJ_CARD_IMAGE_EQN - = a by induction hypothesis -*) -Theorem monocoloured_card: - !n a. 0 < n ==> CARD (monocoloured n a) = a -Proof - rpt strip_tac >> - Induct_on `n` >- - simp[] >> - (Cases_on `n = 0` >> simp[]) >- - simp[monocoloured_1, necklace_card] >> - qabbrev_tac `f = \ls:num list. HD ls :: ls` >> - `INJ f (monocoloured n a) univ(:num list)` by rw[INJ_DEF, Abbr`f`] >> - `FINITE (monocoloured n a)` by rw[monocoloured_finite] >> - `CARD (monocoloured (SUC n) a) = - CARD (IMAGE f (monocoloured n a))` by rw[monocoloured_suc, Abbr`f`] >> - `_ = CARD (monocoloured n a)` by rw[INJ_CARD_IMAGE_EQN] >> - fs[] -QED - -(* Theorem: monocoloured n a = - if n = 0 then {[]} else IMAGE (\c. GENLIST (K c) n) (count a) *) -(* Proof: - If n = 0, true by monocoloured_0 - If n <> 0, then 0 < n. - By monocoloured_def, necklace_def, EXTENSION, this is to show: - (1) 0 < LENGTH x /\ set x SUBSET count a /\ x <> [] ==> SING (set x) ==> - ?c. (x = GENLIST (K c) (LENGTH x)) /\ c < a - Note x <> [] by LENGTH_NON_NIL - so ?c. set x = {c} by SING_DEF - Then c < a by SUBSET_DEF, IN_COUNT - and x = GENLIST (K c) (LENGTH x) by LIST_TO_SET_SING_IFF - (2) c < a ==> LENGTH (GENLIST (K c) n) = n, - This is true by LENGTH_GENLIST - (3) c < a ==> set (GENLIST (K c) n) SUBSET count a - Note set (GENLIST (K c) n) = {c} by GENLIST_K_SET - so c < a ==> {c} SUBSET (count a) by SUBSET_DEF - (4) c < a /\ GENLIST (K c) n <> [] ==> SING (set (GENLIST (K c) n)) - Note set (GENLIST (K c) n) = {c} by GENLIST_K_SET - so SING (set (GENLIST (K c) n)) by SING_DEF -*) -Theorem monocoloured_eqn[compute]: - !n a. monocoloured n a = - if n = 0 then {[]} - else IMAGE (\c. GENLIST (K c) n) (count a) -Proof - rw_tac bool_ss[] >- - simp[monocoloured_0] >> - `0 < n` by decide_tac >> - rw[monocoloured_def, necklace_def, EXTENSION, EQ_IMP_THM] >| [ - `x <> []` by metis_tac[LENGTH_NON_NIL] >> - `SING (set x) /\ ?c. set x = {c}` by rw[GSYM SING_DEF] >> - `c < a` by fs[SUBSET_DEF] >> - `?b. x = GENLIST (K b) (LENGTH x)` by metis_tac[LIST_TO_SET_SING_IFF] >> - metis_tac[GENLIST_K_SET, IN_SING], - simp[], - rw[GENLIST_K_SET], - rw[GENLIST_K_SET] - ] -QED - -(* -> EVAL ``monocoloured 2 3``; = {[2; 2]; [1; 1]; [0; 0]}: thm -> EVAL ``monocoloured 3 2``; = {[1; 1; 1]; [0; 0; 0]}: thm -*) - -(* Slight improvement of a previous result. *) - -(* Theorem: CARD (monocoloured n a) = if n = 0 then 1 else a *) -(* Proof: - If n = 0, - CARD (monocoloured 0 a) - = CARD {[]} by monocoloured_eqn - = 1 by CARD_SING - If n <> 0, then 0 < n. - Let f = (\c:num. GENLIST (K c) n). - Then INJ f (count a) univ(:num list) - by INJ_DEF, GENLIST_K_SET, IN_SING - and FINITE (count a) by FINITE_COUNT - CARD (monocoloured n a) - = CARD (IMAGE f (count a)) by monocoloured_eqn - = CARD (count a) by INJ_CARD_IMAGE_EQN - = a by CARD_COUNT -*) -Theorem monocoloured_card_eqn: - !n a. CARD (monocoloured n a) = if n = 0 then 1 else a -Proof - rw[monocoloured_eqn] >> - qmatch_abbrev_tac `CARD (IMAGE f (count a)) = a` >> - `INJ f (count a) univ(:num list)` by - (rw[INJ_DEF, Abbr`f`] >> - `0 < n` by decide_tac >> - metis_tac[GENLIST_K_SET, IN_SING]) >> - rw[INJ_CARD_IMAGE_EQN] -QED - -(* ------------------------------------------------------------------------- *) -(* Multi-colored necklace *) -(* ------------------------------------------------------------------------- *) - -(* Define multi-colored necklace *) -Definition multicoloured_def: - multicoloured n a = (necklace n a) DIFF (monocoloured n a) -End -(* Note: EVAL can handle set DIFF. *) - -(* -> EVAL ``multicoloured 3 2``; -= {[1; 1; 0]; [1; 0; 1]; [1; 0; 0]; [0; 1; 1]; [0; 1; 0]; [0; 0; 1]}: thm -> EVAL ``multicoloured 2 3``; -= {[2; 1]; [2; 0]; [1; 2]; [1; 0]; [0; 2]; [0; 1]}: thm -*) - -(* Theorem: ls IN multicoloured n a <=> - ls IN necklace n a /\ ls <> [] /\ ~SING (set ls) *) -(* Proof: - ls IN multicoloured n a - <=> ls IN (necklace n a) DIFF (monocoloured n a) by multicoloured_def - <=> ls IN (necklace n a) /\ ls NOTIN (monocoloured n a) by IN_DIFF - <=> ls IN (necklace n a) /\ - ~ls IN necklace n a /\ (ls <> [] ==> SING (set ls)) by monocoloured_def - <=> ls IN (necklace n a) /\ ls <> [] /\ ~SING (set ls) by logical equivalence - - t /\ ~(t /\ (p ==> q)) - = t /\ (~t \/ ~(p ==> q)) - = t /\ ~t \/ (t /\ ~(~p \/ q)) - = t /\ (p /\ ~q) -*) -Theorem multicoloured_element: - !n a ls. ls IN multicoloured n a <=> - ls IN necklace n a /\ ls <> [] /\ ~SING (set ls) -Proof - (rw[multicoloured_def, monocoloured_def, EQ_IMP_THM] >> simp[]) -QED - -(* ------------------------------------------------------------------------- *) -(* Know the Multi-coloured necklaces. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: multicoloured is a necklace. *) - -(* Theorem: ls IN multicoloured n a ==> ls IN necklace n a *) -(* Proof: by multicoloured_def *) -Theorem multicoloured_necklace: - !n a ls. ls IN multicoloured n a ==> ls IN necklace n a -Proof - simp[multicoloured_def] -QED - -(* Idea: The multicoloured set is subset of necklace set. *) - -(* Theorem: (multicoloured n a) SUBSET (necklace n a) *) -(* Proof: - Note multicoloured n a - = (necklace n a) DIFF (monocoloured n a) by multicoloured_def - so (multicoloured n a) SUBSET (necklace n a) by DIFF_SUBSET -*) -Theorem multicoloured_subset: - !n a. (multicoloured n a) SUBSET (necklace n a) -Proof - simp[multicoloured_def] -QED - -(* Idea: multicoloured set is FINITE. *) - -(* Theorem: FINITE (multicoloured n a) *) -(* Proof: - Note multicoloured n a - = (necklace n a) DIFF (monocoloured n a) by multicoloured_def - and FINITE (necklace n a) by necklace_finite - so FINITE (multicoloured n a) by FINITE_DIFF -*) -Theorem multicoloured_finite: - !n a. FINITE (multicoloured n a) -Proof - simp[multicoloured_def, necklace_finite, FINITE_DIFF] -QED - -(* Idea: (multicoloured 0 a) is EMPTY. *) - -(* Theorem: multicoloured 0 a = {} *) -(* Proof: - multicoloured 0 a - = (necklace 0 a) DIFF (monocoloured 0 a) by multicoloured_def - = {[]} - {[]} by necklace_0, monocoloured_0 - = {} by DIFF_EQ_EMPTY -*) -Theorem multicoloured_0: - !a. multicoloured 0 a = {} -Proof - simp[multicoloured_def, necklace_0, monocoloured_0] -QED - -(* Idea: (mutlicoloured 1 a) is also EMPTY. *) - -(* Theorem: multicoloured 1 a = {} *) -(* Proof: - multicoloured 1 a - = (necklace 1 a) DIFF (monocoloured 1 a) by multicoloured_def - = (necklace 1 a) DIFF (necklace 1 a) by monocoloured_1 - = {} by DIFF_EQ_EMPTY -*) -Theorem multicoloured_1: - !a. multicoloured 1 a = {} -Proof - simp[multicoloured_def, monocoloured_1] -QED - -(* Idea: (multicoloured n 0) without color is EMPTY. *) - -(* Theorem: multicoloured n 0 = {} *) -(* Proof: - If n = 0, - Then multicoloured 0 0 = {} by multicoloured_0 - If n <> 0, then 0 < n. - multicoloured n 0 - = (necklace n 0) DIFF (monocoloured n 0) by multicoloured_def - = {} DIFF (monocoloured n 0) by necklace_empty - = {} by EMPTY_DIFF -*) -Theorem multicoloured_n_0: - !n. multicoloured n 0 = {} -Proof - rpt strip_tac >> - Cases_on `n = 0` >- - simp[multicoloured_0] >> - simp[multicoloured_def, necklace_empty] -QED - -(* Idea: (multicoloured n 1) with one color is EMPTY. *) - -(* Theorem: multicoloured n 1 = {} *) -(* Proof: - multicoloured n 1 - = (necklace n 1) DIFF (monocoloured n 1) by multicoloured_def - = {necklace n 1} DIFF (necklace n 1) by monocoloured_mono - = {} by DIFF_EQ_EMPTY -*) -Theorem multicoloured_n_1: - !n. multicoloured n 1 = {} -Proof - simp[multicoloured_def, monocoloured_mono] -QED - -(* Theorem: multicoloured n 0 = {} /\ multicoloured n 1 = {} *) -(* Proof: by multicoloured_n_0, multicoloured_n_1. *) -Theorem multicoloured_empty: - !n. multicoloured n 0 = {} /\ multicoloured n 1 = {} -Proof - simp[multicoloured_n_0, multicoloured_n_1] -QED - -(* ------------------------------------------------------------------------- *) -(* To show: CARD (multicoloured n a) = a^n - a. *) -(* ------------------------------------------------------------------------- *) - -(* Idea: a multicoloured necklace is not monocoloured. *) - -(* Theorem: DISJOINT (multicoloured n a) (monocoloured n a) *) -(* Proof: - Let s = necklace n a, t = monocoloured n a. - Then multicoloured n a = s DIFF t by multicoloured_def - so DISJOINT (multicoloured n a) t by DISJOINT_DIFF -*) -Theorem multi_mono_disjoint: - !n a. DISJOINT (multicoloured n a) (monocoloured n a) -Proof - simp[multicoloured_def, DISJOINT_DIFF] -QED - -(* Idea: a necklace is either monocoloured or multicolored. *) - -(* Theorem: necklace n a = (multicoloured n a) UNION (monocoloured n a) *) -(* Proof: - Let s = necklace n a, t = monocoloured n a. - Then multicoloured n a = s DIFF t by multicoloured_def - Now t SUBSET s by monocoloured_subset - so necklace n a = s - = (multicoloured n a) UNION t by UNION_DIFF -*) -Theorem multi_mono_exhaust: - !n a. necklace n a = (multicoloured n a) UNION (monocoloured n a) -Proof - simp[multicoloured_def, monocoloured_subset, UNION_DIFF] -QED - -(* Idea: size of (multicoloured n a) = a^n - a. *) - -(* Theorem: 0 < n ==> (CARD (multicoloured n a) = a ** n - a) *) -(* Proof: - Let s = necklace n a, - t = monocoloured n a. - Note t SUBSET s by monocoloured_subset - and FINITE s by necklace_finite - CARD (multicoloured n a) - = CARD (s DIFF t) by multicoloured_def - = CARD s - CARD t by SUBSET_DIFF_CARD, t SUBSET s - = a ** n - CARD t by necklace_card - = a ** n - a by monocoloured_card, 0 < n -*) -Theorem multicoloured_card: - !n a. 0 < n ==> (CARD (multicoloured n a) = a ** n - a) -Proof - rpt strip_tac >> - `(monocoloured n a) SUBSET (necklace n a)` by rw[monocoloured_subset] >> - `FINITE (necklace n a)` by rw[necklace_finite] >> - simp[multicoloured_def, SUBSET_DIFF_CARD, necklace_card, monocoloured_card] -QED - -(* Theorem: CARD (multicoloured n a) = if n = 0 then 0 else a ** n - a *) -(* Proof: - If n = 0, - CARD (multicoloured 0 a) - = CARD {} by multicoloured_0 - = 0 by CARD_EMPTY - If n <> 0, then 0 < n. - CARD (multicoloured 0 a) - = a ** n - a by multicoloured_card -*) -Theorem multicoloured_card_eqn: - !n a. CARD (multicoloured n a) = if n = 0 then 0 else a ** n - a -Proof - rpt strip_tac >> - Cases_on `n = 0` >- - simp[multicoloured_0] >> - simp[multicoloured_card] -QED - -(* Idea: (multicoloured n a) NOT empty when 1 < n /\ 1 < a. *) - -(* Theorem: 1 < n /\ 1 < a ==> (multicoloured n a) <> {} *) -(* Proof: - Let s = multicoloured n a. - Then FINITE s by multicoloured_finite - and CARD s = a ** n - a by multicoloured_card - Note a < a ** n by EXP_LT, 1 < a, 1 < n - Thus CARD s <> 0, - or s <> {} by CARD_EMPTY -*) -Theorem multicoloured_nonempty: - !n a. 1 < n /\ 1 < a ==> (multicoloured n a) <> {} -Proof - rpt strip_tac >> - qabbrev_tac `s = multicoloured n a` >> - `FINITE s` by rw[multicoloured_finite, Abbr`s`] >> - `CARD s = a ** n - a` by rw[multicoloured_card, Abbr`s`] >> - `a < a ** n` by rw[EXP_LT] >> - `CARD s <> 0` by decide_tac >> - rfs[] -QED - -(* ------------------------------------------------------------------------- *) - -(* For revised necklace proof using GCD. *) - -(* Idea: multicoloured lists are not monocoloured. *) - -(* Theorem: ls IN multicoloured n a ==> ~(ls IN monocoloured n a) *) -(* Proof: - Let s = necklace n a, - t = monocoloured n a. - Note multicoloured n a = s DIFF t by multicoloured_def - so ls IN multicoloured n a - ==> ls NOTIN t by IN_DIFF -*) -Theorem multicoloured_not_monocoloured: - !n a ls. ls IN multicoloured n a ==> ~(ls IN monocoloured n a) -Proof - simp[multicoloured_def] -QED - -(* Theorem: ls IN necklace n a ==> - (ls IN multicoloured n a <=> ~(ls IN monocoloured n a)) *) -(* Proof: - Let s = necklace n a, - t = monocoloured n a. - Note multicoloured n a = s DIFF t by multicoloured_def - so ls IN multicoloured n a - <=> ls IN s /\ ls NOTIN t by IN_DIFF -*) -Theorem multicoloured_not_monocoloured_iff: - !n a ls. ls IN necklace n a ==> - (ls IN multicoloured n a <=> ~(ls IN monocoloured n a)) -Proof - simp[multicoloured_def] -QED - -(* Theorem: ls IN necklace n a ==> - ls IN multicoloured n a \/ ls IN monocoloured n a *) -(* Proof: by multicoloured_def. *) -Theorem multicoloured_or_monocoloured: - !n a ls. ls IN necklace n a ==> - ls IN multicoloured n a \/ ls IN monocoloured n a -Proof - simp[multicoloured_def] -QED - - -(* ------------------------------------------------------------------------- *) - -(* export theory at end *) -val _ = export_theory(); - -(*===========================================================================*) diff --git a/examples/fermat/little/patternScript.sml b/examples/fermat/little/patternScript.sml index 467ad459c6..da15a2d8a7 100644 --- a/examples/fermat/little/patternScript.sml +++ b/examples/fermat/little/patternScript.sml @@ -116,18 +116,12 @@ val _ = new_theory "pattern"; (* ------------------------------------------------------------------------- *) - (* open dependent theories *) -(* val _ = load "cycleTheory"; *) -open arithmeticTheory pred_setTheory listTheory; -open helperNumTheory helperSetTheory; -open helperListTheory; (* for LENGTH_NON_NIL *) +open arithmeticTheory pred_setTheory listTheory numberTheory dividesTheory + combinatoricsTheory; open cycleTheory; -open dividesTheory; (* for prime_def, NOT_PRIME_0 *) - - (* ------------------------------------------------------------------------- *) (* Pattern Theory Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/Holmakefile b/examples/fermat/twosq/Holmakefile index 4368914df1..98aae4c86f 100644 --- a/examples/fermat/twosq/Holmakefile +++ b/examples/fermat/twosq/Holmakefile @@ -1,7 +1,5 @@ # prefix to HOL examples LOC_PREFIX = $(HOLDIR)/examples -PRE_INCLUDES = $(LOC_PREFIX)/algebra/ring - -ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield +ALGEBRA_INCLUDES = group ring field polynomial finitefield INCLUDES = $(patsubst %,$(LOC_PREFIX)/algebra/%,$(ALGEBRA_INCLUDES)) diff --git a/examples/fermat/twosq/cornerScript.sml b/examples/fermat/twosq/cornerScript.sml index e9eba52a3c..0381d08f71 100644 --- a/examples/fermat/twosq/cornerScript.sml +++ b/examples/fermat/twosq/cornerScript.sml @@ -12,26 +12,20 @@ val _ = new_theory "corner"; (* ------------------------------------------------------------------------- *) +open arithmeticTheory pred_setTheory dividesTheory gcdsetTheory numberTheory + pairTheory combinatoricsTheory; -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - -(* val _ = load "quarityTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) -open EulerTheory; (* for natural_finite, natural_card *) open quarityTheory; -open pairTheory; (* val _ = load "involuteFixTheory"; *) open involuteTheory; open involuteFixTheory; +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Fermat Two Squares by Corners Documentation *) diff --git a/examples/fermat/twosq/helperTwosqScript.sml b/examples/fermat/twosq/helperTwosqScript.sml index 3329996c5e..6dd612af3c 100644 --- a/examples/fermat/twosq/helperTwosqScript.sml +++ b/examples/fermat/twosq/helperTwosqScript.sml @@ -12,21 +12,8 @@ val _ = new_theory "helperTwosq"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -open helperFunctionTheory; -open helperSetTheory; -open helperNumTheory; - -(* arithmeticTheory -- load by default *) -open arithmeticTheory pred_setTheory; -open dividesTheory; -open gcdTheory; (* for GCD_IS_GREATEST_COMMON_DIVISOR *) - -open logPowerTheory; (* for SQRT *) - -open whileTheory; (* for HOARE_SPEC_DEF *) - +open arithmeticTheory pred_setTheory dividesTheory gcdTheory numberTheory + whileTheory combinatoricsTheory primeTheory; (* ------------------------------------------------------------------------- *) (* Helper Theorems Documentation *) diff --git a/examples/fermat/twosq/hoppingScript.sml b/examples/fermat/twosq/hoppingScript.sml index a5a1b2a177..5a9ce3393f 100644 --- a/examples/fermat/twosq/hoppingScript.sml +++ b/examples/fermat/twosq/hoppingScript.sml @@ -12,28 +12,14 @@ val _ = new_theory "hopping"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) +open arithmeticTheory pred_setTheory logrootTheory dividesTheory pairTheory + listTheory rich_listTheory listRangeTheory indexedListsTheory + numberTheory combinatoricsTheory primeTheory; (* val _ = load "quarityTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) -open logPowerTheory; (* for square_alt *) - -open listTheory rich_listTheory; -open helperListTheory; -open listRangeTheory; (* for listRangeLHI_ALL_DISTINCT *) -open indexedListsTheory; (* for findi_EL and EL_findi *) - -open sublistTheory; open quarityTheory; -open pairTheory; (* val _ = load "twoSquaresTheory"; *) open windmillTheory; @@ -44,6 +30,9 @@ open iterateComposeTheory; (* for involute_involute_fix_orbit_fix_odd *) open iterateComputeTheory; (* for iterate_while_thm *) open twoSquaresTheory; (* for loop test found *) +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Node Hopping Algorithm Documentation *) diff --git a/examples/fermat/twosq/involuteActionScript.sml b/examples/fermat/twosq/involuteActionScript.sml index e3ba4fece8..b8aa2625c2 100644 --- a/examples/fermat/twosq/involuteActionScript.sml +++ b/examples/fermat/twosq/involuteActionScript.sml @@ -12,17 +12,10 @@ val _ = new_theory "involuteAction"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) +open arithmeticTheory pred_setTheory numberTheory dividesTheory; (* val _ = load "helperTwosqTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) (* val _ = load "involuteTheory"; *) open involuteTheory; @@ -33,7 +26,6 @@ open groupInstancesTheory; (* for Zadd_def *) (* val _ = load "groupActionTheory"; *) open groupActionTheory; (* for fixed_points_def *) - (* ------------------------------------------------------------------------- *) (* Involution and Action Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/involuteFixScript.sml b/examples/fermat/twosq/involuteFixScript.sml index 50736ccfdb..4cce431ac3 100644 --- a/examples/fermat/twosq/involuteFixScript.sml +++ b/examples/fermat/twosq/involuteFixScript.sml @@ -12,18 +12,13 @@ val _ = new_theory "involuteFix"; (* ------------------------------------------------------------------------- *) +open arithmeticTheory pred_setTheory numberTheory gcdsetTheory + combinatoricsTheory; (* open dependent theories *) -open helperFunctionTheory; (* for FUNPOW_2 *) -open helperSetTheory; (* for BIJ_ELEMENT *) -open helperNumTheory; (* for MOD_EQ *) open helperTwosqTheory; (* for doublet_finite, doublet_card *) open involuteTheory; -(* arithmeticTheory -- load by default *) -open arithmeticTheory pred_setTheory; - - (* ------------------------------------------------------------------------- *) (* Involution Fix Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/involuteScript.sml b/examples/fermat/twosq/involuteScript.sml index 46807b00bb..e417e9719c 100644 --- a/examples/fermat/twosq/involuteScript.sml +++ b/examples/fermat/twosq/involuteScript.sml @@ -12,20 +12,11 @@ val _ = new_theory "involute"; (* ------------------------------------------------------------------------- *) +open arithmeticTheory pred_setTheory gcdsetTheory numberTheory + combinatoricsTheory; -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - -(* val _ = load "helperTwosqTheory"; *) -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; open helperTwosqTheory; (* for FUNPOW_closure *) -(* arithmeticTheory -- load by default *) -open arithmeticTheory pred_setTheory; - - (* ------------------------------------------------------------------------- *) (* Involution: Basic Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/iterateComposeScript.sml b/examples/fermat/twosq/iterateComposeScript.sml index 9a9ec0a44c..b08167d94f 100644 --- a/examples/fermat/twosq/iterateComposeScript.sml +++ b/examples/fermat/twosq/iterateComposeScript.sml @@ -7,22 +7,16 @@ (* add all dependent libraries for script *) open HolKernel boolLib bossLib Parse; +open arithmeticTheory pred_setTheory dividesTheory gcdsetTheory numberTheory + combinatoricsTheory; + (* declare new theory at start *) val _ = new_theory "iterateCompose"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - (* val _ = load "helperTwosqTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) (* val _ = load "involuteFixTheory"; *) open involuteTheory; (* for involute_bij *) @@ -32,6 +26,9 @@ open involuteFixTheory; open iterationTheory; open iterateComputeTheory; (* for iterate_while_thm *) +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Iteration of Involution Composition Documentation *) diff --git a/examples/fermat/twosq/iterateComputeScript.sml b/examples/fermat/twosq/iterateComputeScript.sml index 2a44839e18..66ef3dca35 100644 --- a/examples/fermat/twosq/iterateComputeScript.sml +++ b/examples/fermat/twosq/iterateComputeScript.sml @@ -12,24 +12,13 @@ val _ = new_theory "iterateCompute"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -open helperFunctionTheory; -open helperSetTheory; -open helperNumTheory; - -(* arithmeticTheory -- load by default *) -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def *) +open arithmeticTheory pred_setTheory dividesTheory numberTheory listTheory + rich_listTheory listRangeTheory combinatoricsTheory whileTheory; open iterationTheory; -open listTheory rich_listTheory listRangeTheory; -open helperListTheory; (* for listRangeINC_SNOC *) (* val _ = load "helperTwosqTheory"; *) open helperTwosqTheory; (* for WHILE_RULE_PRE_POST *) -open whileTheory; (* for WHILE definition *) - (* ------------------------------------------------------------------------- *) (* Iteration Period Computation Documentation *) @@ -651,27 +640,32 @@ Proof irule WHILE_RULE_PRE_POST >> qexists_tac `\x. MEM x ls /\ findi x ls <= n` >> qexists_tac `\x. 1 + c - findi x ls` >> - rw[] >| [ + rw[] >| (* 5 subgoals *) + [ (* goal 1 (of 5) *) `a = HD ls` by rw[iterate_trace_head, Abbr`ls`] >> metis_tac[HEAD_MEM, iterate_trace_non_nil], + (* goal 2 (of 5) *) `a = iterate a b 0` by simp[] >> `findi a ls = 0` by metis_tac[iterate_trace_element_idx, DECIDE``0 <= c``] >> decide_tac, + (* goal 3 (of 5) *) qabbrev_tac `p = iterate_period b a` >> qabbrev_tac `y = iterate a b c` >> - `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= c``] >> + `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= (c :num)``] >> `x <> y` by metis_tac[NOT_LESS] >> `findi (b x) ls = 1 + findi x ls` by metis_tac[iterate_trace_index] >> decide_tac, + (* goal 4 (of 5) *) qabbrev_tac `p = iterate_period b a` >> `?j. j <= c /\ (x = iterate a b j)` by metis_tac[iterate_trace_member_iff] >> `findi x ls = j` by metis_tac[iterate_trace_element_idx] >> `~(j < n)` by metis_tac[] >> `j = n` by decide_tac >> fs[], + (* goal 5 (of 5) *) qabbrev_tac `p = iterate_period b a` >> qabbrev_tac `y = iterate a b c` >> - `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= c``] >> + `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= (c :num)``] >> simp[whileTheory.HOARE_SPEC_DEF] >> rpt strip_tac >| [ `x <> y` by metis_tac[NOT_LESS] >> @@ -892,8 +886,6 @@ Proof fs[iterate_while_thm] QED - - (* ------------------------------------------------------------------------- *) (* export theory at end *) diff --git a/examples/fermat/twosq/iterationScript.sml b/examples/fermat/twosq/iterationScript.sml index 4059fbff5f..e4534ee979 100644 --- a/examples/fermat/twosq/iterationScript.sml +++ b/examples/fermat/twosq/iterationScript.sml @@ -12,17 +12,8 @@ val _ = new_theory "iteration"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* open helperTwosqTheory; *) -open helperFunctionTheory; -open helperSetTheory; -open helperNumTheory; - -(* arithmeticTheory -- load by default *) -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def *) - +open arithmeticTheory pred_setTheory dividesTheory gcdTheory numberTheory + combinatoricsTheory; (* ------------------------------------------------------------------------- *) (* Iteration Period Documentation *) diff --git a/examples/fermat/twosq/quarityScript.sml b/examples/fermat/twosq/quarityScript.sml index e00a9a4317..cffd89ee45 100644 --- a/examples/fermat/twosq/quarityScript.sml +++ b/examples/fermat/twosq/quarityScript.sml @@ -7,33 +7,20 @@ (* add all dependent libraries for script *) open HolKernel boolLib bossLib Parse; +open arithmeticTheory pred_setTheory pairTheory listTheory rich_listTheory + listRangeTheory dividesTheory gcdTheory logrootTheory numberTheory + combinatoricsTheory primeTheory; + +open helperTwosqTheory windmillTheory; + (* declare new theory at start *) val _ = new_theory "quarity"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) -(* val _ = load "helperTwosqTheory"; *) -open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperListTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open listTheory rich_listTheory listRangeTheory; -(* val _ = load "dividesTheory"; *) -open dividesTheory; - -(* val _ = load "windmillTheory"; *) -open windmillTheory; - -open pairTheory; (* for FORALL_PROD, PAIR_EQ *) - -(* val _ = load "GaussTheory"; *) -open logrootTheory logPowerTheory GaussTheory EulerTheory; (* for SQRT, divisors_upper_bound *) - +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Quarity Documentation *) diff --git a/examples/fermat/twosq/twoSquaresScript.sml b/examples/fermat/twosq/twoSquaresScript.sml index 2e21df9d3f..8ea9bdb464 100644 --- a/examples/fermat/twosq/twoSquaresScript.sml +++ b/examples/fermat/twosq/twoSquaresScript.sml @@ -12,18 +12,12 @@ val _ = new_theory "twoSquares"; (* ------------------------------------------------------------------------- *) - -(* open dependent theories *) -(* arithmeticTheory -- load by default *) - (* val _ = load "windmillTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -open dividesTheory; (* for divides_def, prime_def *) -open logPowerTheory; (* for prime_non_square *) + +open arithmeticTheory pred_setTheory dividesTheory numberTheory gcdsetTheory + pairTheory listTheory rich_listTheory listRangeTheory combinatoricsTheory + primeTheory; open windmillTheory; @@ -38,21 +32,15 @@ open iterateComposeTheory; (* val _ = load "iterateComputeTheory"; *) open iterateComputeTheory; -(* for later computation *) -open listTheory; -open rich_listTheory; (* for MAP_REVERSE *) -open helperListTheory; (* for listRangeINC_LEN *) -open listRangeTheory; (* for listRangeINC_CONS *) - (* for group action *) (* val _ = load "involuteActionTheory"; *) open involuteActionTheory; open groupActionTheory; open groupInstancesTheory; -(* for pairs *) -open pairTheory; (* for ELIM_UNCURRY, PAIR_FST_SND_EQ, PAIR_EQ, FORALL_PROD *) - +val _ = temp_overload_on("SQ", ``\n. n * (n :num)``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Windmills of the minds Documentation *) diff --git a/examples/fermat/twosq/windmillScript.sml b/examples/fermat/twosq/windmillScript.sml index ec2a807c1b..0d22050ce7 100644 --- a/examples/fermat/twosq/windmillScript.sml +++ b/examples/fermat/twosq/windmillScript.sml @@ -12,30 +12,15 @@ val _ = new_theory "windmill"; (* ------------------------------------------------------------------------- *) - (* open dependent theories *) -(* arithmeticTheory -- load by default *) -(* val _ = load "helperTwosqTheory"; *) open helperTwosqTheory; -open helperNumTheory; -open helperSetTheory; -open helperFunctionTheory; -open arithmeticTheory pred_setTheory; -(* val _ = load "dividesTheory"; *) -open dividesTheory; -(* val _ = load "gcdTheory"; *) -open gcdTheory; (* for P_EUCLIDES *) -open pairTheory; (* for FORALL_PROD, PAIR_EQ *) +open arithmeticTheory pred_setTheory numberTheory combinatoricsTheory + dividesTheory gcdTheory pairTheory logrootTheory primeTheory; (* val _ = load "involuteFixTheory"; *) open involuteTheory involuteFixTheory; -(* val _ = load "GaussTheory"; *) -open logrootTheory logPowerTheory; (* for SQRT, SQRT_LE *) -open GaussTheory; (* for divisors_has_factor *) - - (* ------------------------------------------------------------------------- *) (* Windmills and Involutions Documentation *) (* ------------------------------------------------------------------------- *) diff --git a/examples/simple_complexity/lib/Holmakefile b/examples/simple_complexity/lib/Holmakefile index c37318a6e9..30e0860ab8 100644 --- a/examples/simple_complexity/lib/Holmakefile +++ b/examples/simple_complexity/lib/Holmakefile @@ -1 +1 @@ -INCLUDES = ../../algebra/lib +INCLUDES = $(HOLDIR)/src/algebra diff --git a/examples/simple_complexity/lib/bitsizeScript.sml b/examples/simple_complexity/lib/bitsizeScript.sml index 572987d0d1..c25a15a490 100644 --- a/examples/simple_complexity/lib/bitsizeScript.sml +++ b/examples/simple_complexity/lib/bitsizeScript.sml @@ -12,22 +12,16 @@ val _ = new_theory "bitsize"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "helperFunctionTheory"; (* has helperNum, helperSet *) *) -(* val _ = load "helperListTheory"; *) -open pred_setTheory arithmeticTheory dividesTheory gcdTheory; -open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; (* for DIV_EQ_0 *) - -(* open dependent theories *) -open listTheory rich_listTheory; - -(* val _ = load "logPowerTheory"; *) -open logrootTheory logPowerTheory; (* for LOG_1, ulog *) +open pred_setTheory arithmeticTheory dividesTheory gcdTheory numberTheory + combinatoricsTheory listTheory rich_listTheory logrootTheory + primeTheory; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Bit Size for Numbers Documentation *) diff --git a/examples/simple_complexity/lib/complexityScript.sml b/examples/simple_complexity/lib/complexityScript.sml index 5a3a79ca9c..b457dc474d 100644 --- a/examples/simple_complexity/lib/complexityScript.sml +++ b/examples/simple_complexity/lib/complexityScript.sml @@ -12,22 +12,19 @@ val _ = new_theory "complexity"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* val _ = load "bitsizeTheory"; *) -open bitsizeTheory; -open logrootTheory; (* for LOG_1 *) - -open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; -open logPowerTheory; (* for ulog_pos *) - (* open dependent theories *) -open prim_recTheory pred_setTheory arithmeticTheory dividesTheory gcdTheory; -open listTheory rich_listTheory;; +open prim_recTheory pred_setTheory arithmeticTheory dividesTheory gcdTheory + listTheory rich_listTheory logrootTheory numberTheory combinatoricsTheory + primeTheory; + +open bitsizeTheory; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); (* ------------------------------------------------------------------------- *) (* Computational Complexity Documentation *) diff --git a/examples/simple_complexity/loop/Holmakefile b/examples/simple_complexity/loop/Holmakefile index 862db19adc..807c307bb6 100644 --- a/examples/simple_complexity/loop/Holmakefile +++ b/examples/simple_complexity/loop/Holmakefile @@ -1 +1 @@ -INCLUDES = ../../algebra/lib ../lib +INCLUDES = ../lib diff --git a/examples/simple_complexity/loop/loopDecreaseScript.sml b/examples/simple_complexity/loop/loopDecreaseScript.sml index 0b8b13af5b..4794120266 100644 --- a/examples/simple_complexity/loop/loopDecreaseScript.sml +++ b/examples/simple_complexity/loop/loopDecreaseScript.sml @@ -12,22 +12,17 @@ val _ = new_theory "loopDecrease"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "loopTheory"; *) -open loopTheory; - (* open dependent theories *) -open arithmeticTheory; -open dividesTheory; -open helperNumTheory helperListTheory helperFunctionTheory; (* for DIV_EQUAL_0 *) -open listTheory rich_listTheory; -open listRangeTheory; +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory listTheory + rich_listTheory listRangeTheory; + +open loopTheory; +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence with Decreasing argument Documentation *) diff --git a/examples/simple_complexity/loop/loopDivideScript.sml b/examples/simple_complexity/loop/loopDivideScript.sml index 711cf355f9..348c53cbd1 100644 --- a/examples/simple_complexity/loop/loopDivideScript.sml +++ b/examples/simple_complexity/loop/loopDivideScript.sml @@ -12,26 +12,20 @@ val _ = new_theory "loopDivide"; (* ------------------------------------------------------------------------- *) - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "loopTheory"; *) -open loopTheory; - -(* val _ = load "bitsizeTheory"; *) -open bitsizeTheory; - (* open dependent theories *) -open arithmeticTheory dividesTheory; -open helperNumTheory helperListTheory helperFunctionTheory; (* for DIV_EQUAL_0 *) -open listTheory rich_listTheory; -open listRangeTheory; +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory listTheory + rich_listTheory listRangeTheory logrootTheory; -open logrootTheory; (* for LOG_EQ_0 *) -open logPowerTheory; (* for LOG_LE_REVERSE *) +open loopTheory bitsizeTheory; +val _ = temp_overload_on("SQ", ``\n. n * n``); +val _ = temp_overload_on("HALF", ``\n. n DIV 2``); +val _ = temp_overload_on("TWICE", ``\n. 2 * n``); +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence with Dividing argument Documentation *) diff --git a/examples/simple_complexity/loop/loopIncreaseScript.sml b/examples/simple_complexity/loop/loopIncreaseScript.sml index f69fe7bfbf..16b961b5ce 100644 --- a/examples/simple_complexity/loop/loopIncreaseScript.sml +++ b/examples/simple_complexity/loop/loopIncreaseScript.sml @@ -12,21 +12,17 @@ val _ = new_theory "loopIncrease"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "loopTheory"; *) -open loopTheory; - (* open dependent theories *) -open arithmeticTheory dividesTheory; -open helperNumTheory helperListTheory helperFunctionTheory; (* for DIV_EQUAL_0 *) -open listTheory rich_listTheory; -open listRangeTheory; +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory listTheory + rich_listTheory listRangeTheory; + +open loopTheory; +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence with Increasing argument Documentation *) diff --git a/examples/simple_complexity/loop/loopListScript.sml b/examples/simple_complexity/loop/loopListScript.sml index aef9ce8f32..808e5b8221 100644 --- a/examples/simple_complexity/loop/loopListScript.sml +++ b/examples/simple_complexity/loop/loopListScript.sml @@ -12,8 +12,6 @@ val _ = new_theory "loopList"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; @@ -25,14 +23,11 @@ open loopTheory; open bitsizeTheory; (* open dependent theories *) -open arithmeticTheory dividesTheory; -open helperNumTheory helperListTheory helperFunctionTheory; -open listTheory rich_listTheory; -open listRangeTheory; - -(* val _ = load "sublistTheory"; *) -open sublistTheory; (* for sublist_drop *) +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory listTheory + rich_listTheory listRangeTheory; +(* Overload sublist by infix operator *) +val _ = temp_overload_on ("<=", ``sublist``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence with List argument Documentation *) diff --git a/examples/simple_complexity/loop/loopMultiplyScript.sml b/examples/simple_complexity/loop/loopMultiplyScript.sml index 289307cdb6..9c6198dc3f 100644 --- a/examples/simple_complexity/loop/loopMultiplyScript.sml +++ b/examples/simple_complexity/loop/loopMultiplyScript.sml @@ -12,24 +12,17 @@ val _ = new_theory "loopMultiply"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "loopTheory"; *) -open loopTheory; - (* open dependent theories *) -open arithmeticTheory dividesTheory; -open helperNumTheory helperListTheory helperFunctionTheory; (* for DIV_EQUAL_0 *) -open listTheory rich_listTheory; -open listRangeTheory; +open arithmeticTheory dividesTheory numberTheory combinatoricsTheory listTheory + rich_listTheory listRangeTheory logrootTheory primeTheory; -(* val _ = load "logPowerTheory"; *) -open logrootTheory logPowerTheory; (* for mop_eqn *) +open loopTheory; +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence with Multiplying argument Documentation *) diff --git a/examples/simple_complexity/loop/loopScript.sml b/examples/simple_complexity/loop/loopScript.sml index 79a0000f54..c65c1b4b68 100644 --- a/examples/simple_complexity/loop/loopScript.sml +++ b/examples/simple_complexity/loop/loopScript.sml @@ -12,21 +12,14 @@ val _ = new_theory "loop"; (* ------------------------------------------------------------------------- *) - - (* val _ = load "jcLib"; *) open jcLib; -(* Get dependent theories in lib *) -(* val _ = load "logPowerTheory"; (* has helperNum, helperSet, helperFunction *) *) -open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; - -(* open dependent theories *) -open listTheory rich_listTheory; -open listRangeTheory; - -open arithmeticTheory; +open arithmeticTheory listTheory rich_listTheory listRangeTheory numberTheory + combinatoricsTheory; +val _ = temp_overload_on ("RISING", ``\f. !x:num. x <= f x``); +val _ = temp_overload_on ("FALLING", ``\f. !x:num. f x <= x``); (* ------------------------------------------------------------------------- *) (* Loop Recurrence Documentation *)