cooperScript.sml

1Theory cooper
2Ancestors
3  integer int_arith
4
5Theorem elim_le[unlisted] = GSYM INT_NOT_LT;
6
7Theorem move_add[unlisted]:
8  !x y z:int. (x + y) + z = (x + z) + y
9Proof
10  REPEAT GEN_TAC THEN CONV_TAC (AC_CONV (INT_ADD_ASSOC, INT_ADD_COMM))
11QED
12
13val AND_CLAUSES0 = CONJUNCTS (Q.ID_SPEC AND_CLAUSES);
14val OR_CLAUSES0 = CONJUNCTS (Q.ID_SPEC OR_CLAUSES);
15Theorem T_and_l = GEN_ALL (List.nth(AND_CLAUSES0, 0));
16Theorem T_and_r = GEN_ALL (List.nth(AND_CLAUSES0, 1));
17Theorem F_and_l = GEN_ALL (List.nth(AND_CLAUSES0, 2));
18Theorem F_and_r = GEN_ALL (List.nth(AND_CLAUSES0, 3));
19Theorem T_or_l = GEN_ALL (List.nth(OR_CLAUSES0, 0));
20Theorem T_or_r = GEN_ALL (List.nth(OR_CLAUSES0, 1));
21Theorem F_or_l = GEN_ALL (List.nth(OR_CLAUSES0, 2));
22Theorem F_or_r = GEN_ALL (List.nth(OR_CLAUSES0, 3));
23
24Theorem NOT_NOT_P = List.nth(CONJUNCTS NOT_CLAUSES, 0);
25Theorem NOT_OR = GEN_ALL (#2 (CONJ_PAIR (SPEC_ALL DE_MORGAN_THM)));
26Theorem NOT_AND = GEN_ALL (#1 (CONJ_PAIR (SPEC_ALL DE_MORGAN_THM)));
27
28Theorem NOT_AND_IMP[unlisted] =
29  tautLib.TAUT_PROVE ``!p q. ~(p /\ q) = (p ==> ~q)``;
30
31Theorem DISJ_NEQ_ELIM[unlisted]:
32  !P x v:'a. ~(x = v) \/ P x <=> ~(x = v) \/ P v
33Proof
34  REWRITE_TAC [GSYM IMP_DISJ_THM] THEN REPEAT GEN_TAC THEN EQ_TAC THEN
35  REPEAT STRIP_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
36  POP_ASSUM MP_TAC THEN REWRITE_TAC []
37QED
38
39Theorem cpEU_THM[unlisted]:
40  !P. (?!x:int. P x) <=>
41      (?x. P x) /\ (!y y'. (~P y \/ ~P y') \/ (1*y = 1*y'))
42Proof
43  REWRITE_TAC [INT_MUL_LID, EXISTS_UNIQUE_THM, GSYM DE_MORGAN_THM,
44               GSYM IMP_DISJ_THM]
45QED
46
47Theorem simple_disj_congruence:
48  !p q r. (~p ==> (q = r)) ==> (p \/ q <=> p \/ r)
49Proof
50  REPEAT GEN_TAC THEN MAP_EVERY Q.ASM_CASES_TAC [`p`,`q`,`r`] THEN
51  ASM_REWRITE_TAC []
52QED
53
54Theorem simple_conj_congruence:
55  !p q r. (p ==> (q = r)) ==> (p /\ q <=> p /\ r)
56Proof
57  REPEAT GEN_TAC THEN MAP_EVERY Q.ASM_CASES_TAC [`p`,`q`,`r`] THEN
58  ASM_REWRITE_TAC []
59QED
60
61Theorem my_INT_MUL_LID[unlisted]:
62  (1 * (c * d) = c * d) /\
63  (~1 * (c * d) = ~c * d) /\
64  (1 * (c * d + x) = c * d + x) /\
65  (~1 * (c * d + x) = ~c * d + ~x) /\
66  (~~x = x)
67Proof
68  REWRITE_TAC [INT_MUL_LID, GSYM INT_NEG_MINUS1, INT_NEG_LMUL,
69               INT_NEG_ADD, INT_NEGNEG]
70QED
71
72Theorem INT_DIVIDES_NEG'[unlisted] =
73  CONV_RULE (DEPTH_CONV FORALL_AND_CONV) INT_DIVIDES_NEG;
74
75Theorem INT_NEG_FLIP_LTL[local]:
76  !x y. ~x < y <=> ~y < x
77Proof
78  REPEAT GEN_TAC THEN
79  CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV (GSYM INT_NEGNEG)))) THEN
80  REWRITE_TAC [INT_LT_NEG]
81QED
82
83Theorem INT_NEG_FLIP_LTR[local]:
84  !x y. x < ~y <=> y < ~x
85Proof
86  REPEAT GEN_TAC THEN
87  CONV_TAC (RAND_CONV (LAND_CONV (REWR_CONV (GSYM INT_NEGNEG)))) THEN
88  REWRITE_TAC [INT_LT_NEG]
89QED
90
91Theorem negated_elim_lt_coeffs1[unlisted] =
92  (ONCE_REWRITE_RULE [INT_NEG_FLIP_LTR] o
93   REWRITE_RULE [GSYM INT_NEG_RMUL] o
94   Q.SPECL [`n`, `m`, `~x`])
95  elim_lt_coeffs1;
96
97Theorem negated_elim_lt_coeffs2[unlisted] =
98  (ONCE_REWRITE_RULE [INT_NEG_FLIP_LTL] o
99   REWRITE_RULE [GSYM INT_NEG_RMUL] o
100   Q.SPECL [`n`, `m`, `~x`])
101  elim_lt_coeffs2;
102
103Theorem elim_eq_coeffs'[unlisted] =
104  CONV_RULE (STRIP_QUANT_CONV (RAND_CONV
105                               (BINOP_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))))
106  elim_eq_coeffs;
107
108Theorem p6_step[unlisted]:
109  (?x:int. K (lo < x /\ x <= hi) x /\ P x) <=>
110  lo < hi /\ (P hi \/ (?x:int. K (lo < x /\ x <= hi - 1) x /\ P x))
111Proof
112  REWRITE_TAC [combinTheory.K_THM, LEFT_AND_OVER_OR] THEN
113  EQ_TAC THENL [
114    CONV_TAC
115      (LAND_CONV (ONCE_REWRITE_CONV [restricted_quantification_simp])) THEN
116    STRIP_TAC THENL [
117      FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_REWRITE_TAC [],
118      ASM_REWRITE_TAC [] THEN DISJ2_TAC THEN
119      Q.EXISTS_TAC `x` THEN ASM_REWRITE_TAC []
120    ],
121    STRIP_TAC THENL [
122      Q.EXISTS_TAC `hi` THEN ASM_REWRITE_TAC [INT_LE_REFL],
123      ONCE_REWRITE_TAC [restricted_quantification_simp] THEN
124      Q.EXISTS_TAC `x` THEN  ASM_REWRITE_TAC []
125    ]
126  ]
127QED
128
129Theorem NOT_EXISTS_THM'[unlisted] = GEN_ALL $ SYM $
130  PURE_REWRITE_RULE [NOT_CLAUSES] $ BETA_RULE $
131  SPEC ``\x:'a. ~ P x : bool`` boolTheory.NOT_EXISTS_THM;
132
133Theorem NOT_NOT[unlisted] = tautLib.TAUT_PROVE ``~~p:bool = p``;
134
135Theorem K_THM'[unlisted] =
136  INST_TYPE [(alpha |-> bool), (beta |-> ``:int``)] combinTheory.K_THM;