From cf0c3e813e4601f7462268703efd5b14424bd6c3 Mon Sep 17 00:00:00 2001 From: mark <> Date: Fri, 24 Feb 2012 12:07:26 +0000 Subject: Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'. Add wrapper function for :thm -> thm list. Promote more objects. --- hol-light/TacticRecording/ex.dot | 29 ++-- hol-light/TacticRecording/ex2.dot | 13 ++ hol-light/TacticRecording/ex3.dot | 24 ++++ hol-light/TacticRecording/ex3.png | Bin 0 -> 39644 bytes hol-light/TacticRecording/examples1.ml | 2 - hol-light/TacticRecording/examples3.ml | 4 +- hol-light/TacticRecording/examples5.ml | 241 +++++++++++++++++++++++--------- hol-light/TacticRecording/hiproofs.ml | 59 ++++---- hol-light/TacticRecording/lib.ml | 9 ++ hol-light/TacticRecording/main.ml | 1 + hol-light/TacticRecording/mldata.ml | 33 +++++ hol-light/TacticRecording/mlexport.ml | 22 +-- hol-light/TacticRecording/printutils.ml | 42 +++--- hol-light/TacticRecording/promote.ml | 14 ++ hol-light/TacticRecording/tacticrec.ml | 24 ++-- hol-light/TacticRecording/wrappers.ml | 163 +++++++++++---------- hol-light/TacticRecording/xtactics.ml | 10 +- hol-light/TacticRecording/xthm.ml | 55 ++------ 18 files changed, 470 insertions(+), 275 deletions(-) create mode 100644 hol-light/TacticRecording/ex2.dot create mode 100644 hol-light/TacticRecording/ex3.dot create mode 100644 hol-light/TacticRecording/ex3.png create mode 100644 hol-light/TacticRecording/mldata.ml (limited to 'hol-light') diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot index fbe961bd..e96142f9 100644 --- a/hol-light/TacticRecording/ex.dot +++ b/hol-light/TacticRecording/ex.dot @@ -1,13 +1,24 @@ digraph G { - subgraph cluster0 { - label = "process #1" - a0->a1->a2->a3 - } subgraph cluster1 { - label = "process #2" - b0->b1->b2->b3 + label = "induction"; + 517 -> 518; + 517 -> 519; + } + subgraph cluster2 { + label = "base case"; + 528; + } + subgraph cluster3 { + label = "step case"; + 537 -> 538; + 538 -> 540; + 540 -> 542; + 542 -> 544; + 544 -> 546; + 546 -> 548; } - b3->23 - b2->a3 - a3->23 + 512 -> 513; + 513 -> 517; + 518 -> 528; + 519 -> 537; } \ No newline at end of file diff --git a/hol-light/TacticRecording/ex2.dot b/hol-light/TacticRecording/ex2.dot new file mode 100644 index 00000000..fbe961bd --- /dev/null +++ b/hol-light/TacticRecording/ex2.dot @@ -0,0 +1,13 @@ +digraph G { + subgraph cluster0 { + label = "process #1" + a0->a1->a2->a3 + } + subgraph cluster1 { + label = "process #2" + b0->b1->b2->b3 + } + b3->23 + b2->a3 + a3->23 +} \ No newline at end of file diff --git a/hol-light/TacticRecording/ex3.dot b/hol-light/TacticRecording/ex3.dot new file mode 100644 index 00000000..1704533d --- /dev/null +++ b/hol-light/TacticRecording/ex3.dot @@ -0,0 +1,24 @@ +digraph G { + subgraph cluster1 { + label = "induction"; + 351 -> 352; + 351 -> 353; + 352 -> 358; + subgraph cluster2 { + label = "base case"; + 358; + } + 353 -> 367; + subgraph cluster3 { + label = "step case"; + 367 -> 368; + 368 -> 370; + 370 -> 372; + 372 -> 374; + 374 -> 376; + 376 -> 378; + } + } + 344 -> 345; + 345 -> 351; +} diff --git a/hol-light/TacticRecording/ex3.png b/hol-light/TacticRecording/ex3.png new file mode 100644 index 00000000..f2edfbdc Binary files /dev/null and b/hol-light/TacticRecording/ex3.png differ diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml index fd0b446c..4e67ca18 100644 --- a/hol-light/TacticRecording/examples1.ml +++ b/hol-light/TacticRecording/examples1.ml @@ -43,8 +43,6 @@ g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;; e (REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);; let th = top_thm ();; -#use"TacticRecording/mlexport.ml";; - print_executed_proof true;; print_flat_proof true;; print_thenl_proof ();; diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml index 62a2ef70..f78ace3f 100644 --- a/hol-light/TacticRecording/examples3.ml +++ b/hol-light/TacticRecording/examples3.ml @@ -29,14 +29,14 @@ let LEMMA_1 = prove CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN HILABEL "induction" (INDUCT_TAC THEN - REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES]) THENL + REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL [HILABEL "base case" REAL_ARITH_TAC; ALL_TAC] THEN HILABEL "step case" (REWRITE_TAC[ARITH_RULE `1 <= SUC n`] THEN SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN REWRITE_TAC[real_pow; REAL_MUL_RID] THEN REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN - REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC));; + REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC)));; let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;; diff --git a/hol-light/TacticRecording/examples5.ml b/hol-light/TacticRecording/examples5.ml index 6e34aaee..1ded99cf 100644 --- a/hol-light/TacticRecording/examples5.ml +++ b/hol-light/TacticRecording/examples5.ml @@ -1,79 +1,182 @@ -from Library/binomial.ml +(* Taken from Library/prime.ml *) prioritize_num();; (* ------------------------------------------------------------------------- *) -(* Binomial coefficients. *) +(* HOL88 compatibility (since all this is a port of old HOL88 stuff). *) (* ------------------------------------------------------------------------- *) -let binom = define - `(!n. binom(n,0) = 1) /\ - (!k. binom(0,SUC(k)) = 0) /\ - (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;; - -let binom = theorem_wrap "binom" binom;; - -let BINOM_LT = prove - (`!n k. n < k ==> (binom(n,k) = 0)`, - INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN - ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);; -let BINOM_LT = theorem_wrap "BINOM_LT" BINOM_LT;; - -print_flat_proof true;; - -let BINOM_REFL = prove - (`!n. binom(n,n) = 1`, - INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);; -let BINOM_REFL = theorem_wrap "BINOM_REFL" BINOM_REFL;; - -let BINOM_1 = prove - (`!n. binom(n,1) = n`, - REWRITE_TAC[num_CONV `1`] THEN - INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);; -let BINOM_1 = theorem_wrap "BINOM_1" BINOM_1;; - -let BINOM_FACT = prove - (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`, - INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN - INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN - FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN - REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);; -let BINOM_FACT = theorem_wrap "BINOM_FACT" BINOM_FACT;; - -let BINOM_EQ_0 = prove - (`!n k. binom(n,k) = 0 <=> n < k`, - REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[BINOM_LT]] THEN - ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN - REWRITE_TAC[NOT_LT; LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN - DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN - DISCH_TAC THEN MP_TAC(SYM(SPECL [`d:num`; `k:num`] BINOM_FACT)) THEN - ASM_REWRITE_TAC[GSYM LT_NZ; MULT_CLAUSES; FACT_LT]);; -let BINOM_EQ_0 = theorem_wrap "BINOM_EQ_0" BINOM_EQ_0;; - -let BINOM_PENULT = prove - (`!n. binom(SUC n,n) = SUC n`, - INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN - SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL - [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);; -let BINOM_PENULT = theorem_wrap "BINOM_PENULT" BINOM_PENULT;; +let MULT_MONO_EQ = prove + (`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`, + REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);; +let LESS_ADD_1 = prove + (`!m n. n < m ==> (?p. m = n + (p + 1))`, + REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);; + +let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;; + +let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;; + +let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;; + +let LESS_EQ_0 = prove + (`!n. n <= 0 <=> (n = 0)`, + REWRITE_TAC[LE]);; + +let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;; + +let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;; + +let NOT_EXP_0 = prove + (`!m n. ~((SUC n) EXP m = 0)`, + REWRITE_TAC[EXP_EQ_0; NOT_SUC]);; + +let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;; + +let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;; + +let ZERO_LESS_EXP = prove + (`!m n. 0 < ((SUC n) EXP m)`, + REWRITE_TAC[LT_NZ; NOT_EXP_0]);; + +(* ------------------------------------------------------------------------- *) +(* General arithmetic lemmas. *) (* ------------------------------------------------------------------------- *) -(* More potentially useful lemmas. *) + +let MULT_FIX = prove( + `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`, + REPEAT GEN_TAC THEN + STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN + REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN + REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN + GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) (* MMA: this is a problem !!!!) + [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN + MATCH_ACCEPT_TAC MULT_MONO_EQ);; + +let LESS_EQ_MULT = prove( + `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`, + REPEAT GEN_TAC THEN + DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN + ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; + GSYM ADD_ASSOC; LE_ADD]);; + +let LESS_MULT = prove( + `!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`, + REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN + ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN + REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN + ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN + MATCH_ACCEPT_TAC LESS_ADD_SUC);; + +let MULT_LCANCEL = prove( + `!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`, + REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN + REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);; + +let LT_POW2_REFL = prove + (`!n. n < 2 EXP n`, + INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);; + (* ------------------------------------------------------------------------- *) +(* Properties of the exponential function. *) +(* ------------------------------------------------------------------------- *) + +let EXP_0 = prove + (`!n. 0 EXP (SUC n) = 0`, + REWRITE_TAC[EXP; MULT_CLAUSES]);; + +let EXP_MONO_LT_SUC = prove + (`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`, + REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);; + +let EXP_MONO_LE_SUC = prove + (`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`, + REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);; + +let EXP_MONO_EQ_SUC = prove + (`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`, + REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);; + +let EXP_EXP = prove + (`!x m n. (x EXP m) EXP n = x EXP (m * n)`, + REWRITE_TAC[EXP_MULT]);; + +(* ------------------------------------------------------------------------- *) +(* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere. *) +(* ------------------------------------------------------------------------- *) + +let DIFF_LEMMA = prove( + `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`, + REPEAT GEN_TAC THEN + DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN + DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN + DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN + REWRITE_TAC[ADD_ASSOC] THEN + REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);; + +let NOT_EVEN_EQ_ODD = prove( + `!m n. ~(2 * m = SUC(2 * n))`, + REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN + REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);; + +let CANCEL_TIMES2 = prove( + `!x y. (2 * x = 2 * y) <=> (x = y)`, + REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);; + +let EVEN_SQUARE = prove( + `!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`, + GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN + DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN + EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN + REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN + REWRITE_TAC[MULT_AC]);; + +let ODD_SQUARE = prove( + `!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`, + GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN + DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN + ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN + REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN + EXISTS_TAC `(m * m) + m` THEN + REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN + REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN + REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[ADD_AC]);; + +let DIFF_SQUARE = prove( + `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`, + REPEAT GEN_TAC THEN + DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL + [SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL + [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[]; + POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN + REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]]; + POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN + AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);; + +let ADD_IMP_SUB = prove( + `!x y z. (x + y = z) ==> (x = z - y)`, + REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN + REWRITE_TAC[ADD_SUB]);; + +let ADD_SUM_DIFF = prove( + `!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\ + ((w + v) + (w - v) = 2 * w)`, + REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN + DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN + ONCE_REWRITE_TAC[ADD_SYM] THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);; -let BINOM_TOP_STEP = prove - (`!n k. ((n + 1) - k) * binom(n + 1,k) = (n + 1) * binom(n,k)`, - REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k:num` THENL - [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP - (ARITH_RULE `n < k ==> n + 1 = k \/ n + 1 < k`)) THEN - ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES]; - ALL_TAC] THEN - FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN - DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN - REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN - MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN - MP_TAC(SPECL [`d:num`; `k:num`] BINOM_FACT) THEN - REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN - MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN - REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);; -let BINOM_TOP_STEP = theorem_wrap "BINOM_TOP_STEP" BINOM_TOP_STEP;; +let EXP_4 = prove( + `!n. n EXP 4 = (n EXP 2) EXP 2`, + GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN + REWRITE_TAC[ARITH]);; diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml index 370e0dc3..310ba677 100644 --- a/hol-light/TacticRecording/hiproofs.ml +++ b/hol-light/TacticRecording/hiproofs.ml @@ -143,7 +143,7 @@ let collapse_tensor h hs = let trivsimp_hiproof h = let trivsimp h = match h with - Hatomic (id,_) when (gtree_tactic (get_gtree id) = (Some "ALL_TAC",[])) + Hatomic (id,_) when (gtree_tactic (get_gtree id) = ("ALL_TAC",[])) -> Hidentity id | Hsequence (h1, Hempty) -> h1 | Hsequence (h1, Hidentity _) -> h1 @@ -161,7 +161,7 @@ let trivsimp_hiproof h = refactor_hiproof true trivsimp h;; -(* Matching up lists of hiproofs *) +(* Matching up two tensored lists to create single tensored list *) let rec matchup_hiproofs0 hs1 hs2 = match hs1 with @@ -181,19 +181,17 @@ let matchup_hiproofs hs1 hs2 = map (fun (h1,hs2) -> Hsequence (h1, Htensor hs2)) hhs;; -(* Separating out lists of hiproofs *) +(* Separating out tensored list into head tensor and tail tensor *) -(* let separate_hiproofs0 h (hs01,hs02) = match h with Hsequence (h1,h2) -> (h1::hs01, h2::hs02) | _ -> let n = hiproof_arity h in - let h2 = Htensor (copy n Hidentity) in + let h2 = Htensor (copy n (Hidentity (-1))) in (h::hs01, h2::hs02);; let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);; -*) (* Delabelling *) @@ -205,7 +203,7 @@ let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);; let delabel_hiproof h = let delabel h = match h with - Hlabelled (Tactical (Some "SUBGOAL_THEN",_), h0) + Hlabelled (Tactical ("SUBGOAL_THEN",_), h0) -> h | Hlabelled (_,h0) -> h0 @@ -215,7 +213,7 @@ let delabel_hiproof h = let dethen_hiproof h = let dethen h = match h with - Hlabelled (Tactical (Some ("THEN" | "THENL"),_), h0) + Hlabelled (Tactical (("THEN" | "THENL"),_), h0) -> h0 | _ -> h in refactor_hiproof true dethen h;; @@ -248,32 +246,40 @@ let leftgroup_hiproof h = match h with Hsequence (h1, Hsequence (h2, h3)) -> Hsequence (Hsequence (h1,h2), h3) -(* | Hsequence (h1, Htensor hs2) - -> if (exists is_hsequence hs2) - then let (hs2a,hs2b) = separate_hiproofs hs2 in - Hsequence (Hsequence (h1, Htensor hs2a), Htensor hs2b) - else h *) | _ -> h in refactor_hiproof true leftgroup h;; (* THEN insertion *) -(* Looks for opportunities to use 'THEN' tacticals. Note that this disrupts *) -(* arity consistency. *) +(* Looks for opportunities to use 'THEN' tacticals. Note that assumes a *) +(* normal form where trivsimp has taken place. *) + +let rec head_hiproof_equiv h1 h2 = + match (h1,h2) with + (Hatomic (id1,_), Hatomic (id2,_)) + -> (gtree_tactic o get_gtree) id1 = (gtree_tactic o get_gtree) id2 + | (Hidentity _, Hidentity _) + -> true + | (Hsequence (h1a,h1b), h2) + -> head_hiproof_equiv h1a h2 + | (h1, Hsequence (h2a,h2b)) + -> head_hiproof_equiv h1 h2a + | (Hempty, Hempty) + -> true + | _ -> false;; let thenise_hiproof h = - let thenise h = + let rec thenise h = match h with Hsequence (h1, Htensor (h2::h2s)) - -> if (forall (fun h0 -> h0 = h2) h2s) - then Hlabelled (Tactical (Some "THEN", []), h) - else h - | Hsequence (h1, Hsequence (Htensor (h2::h2s), h3)) - -> if (forall (fun h0 -> h0 = h2) h2s) - then Hsequence - (Hlabelled (Tactical (Some "THEN", []), - Hsequence (h1, Htensor (h2::h2s))), h3) + -> if not (is_hidentity h2) & (forall (head_hiproof_equiv h2) h2s) + then let (hs2a,hs2b) = separate_hiproofs (h2::h2s) in + let h' = Hsequence + (Hlabelled (Tactical ("THEN",[]), + Hsequence (h1, Htensor hs2a)), + Htensor hs2b) in + thenise h' else h | _ -> h in refactor_hiproof false thenise h;; @@ -360,10 +366,7 @@ let rec hiproof_graph0 h = let hiproof_graph h = let ges = hiproof_graph0 h in let ids = graph_nodes ges in - let tacname_of_id id = - match ((fst o gtree_tactic1 o get_gtree) id) with - Some x -> x - | None -> "" in + let tacname_of_id id = (fst o gtree_tactic1 o get_gtree) id in let ges' = map (fun id -> Name (id, tacname_of_id id)) ids in ges' @ ges;; diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml index b1309f84..5de28331 100644 --- a/hol-light/TacticRecording/lib.ml +++ b/hol-light/TacticRecording/lib.ml @@ -19,6 +19,15 @@ let rec foldr f xs a = | [] -> a;; +(* foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a *) + +let rec foldr1 f xs = + match xs with + x::[] -> x + | x1::xs2 -> f x1 (foldr1 f xs2) + | [] -> failwith "foldr1: Empty list";; + + (* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b *) let rec foldl f a xs = diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml index bfdc1488..57c82547 100644 --- a/hol-light/TacticRecording/main.ml +++ b/hol-light/TacticRecording/main.ml @@ -6,6 +6,7 @@ (* Datatypes and recording mechanism *) +#use "TacticRecording/mldata.ml";; #use "TacticRecording/xthm.ml";; #use "TacticRecording/xtactics.ml";; #use "TacticRecording/tacticrec.ml";; diff --git a/hol-light/TacticRecording/mldata.ml b/hol-light/TacticRecording/mldata.ml new file mode 100644 index 00000000..b547a89b --- /dev/null +++ b/hol-light/TacticRecording/mldata.ml @@ -0,0 +1,33 @@ + + +type mlarg = + Mlint of int + | Mlstring of string + | Mlterm of term + | Mltype of hol_type + | Mlthm of mldata + | Mlpair of mlarg * mlarg + | Mllist of mlarg list + | Mlfn of mldata + +and mldata = string * mlarg list;; (* ML object name and args *) + + +type label = + Tactical of mldata + | Label of string;; + + +(* Atomic tests *) + +let is_atomic_mlarg arg = + match arg with + Mlthm (_,(_::_)) | Mlpair _ | Mlfn (_, _::_) -> false + | _ -> true;; + +let is_atomic_mldata ((x,args):mldata) = (is_empty args);; + + +(* active_info *) + +let active_info = ("...",[]);; diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml index 429cb770..9a9207d5 100644 --- a/hol-light/TacticRecording/mlexport.ml +++ b/hol-light/TacticRecording/mlexport.ml @@ -15,10 +15,9 @@ (* ** UTILS ** *) -(* Printer for tactic 'finfo' *) +(* Printer for tactic is just the ML data printer *) -let print_tactic br ((x_,args):finfo) = - print_finfo "" br ((x_,args):finfo);; +let print_tactic br obj = print_mldata br obj;; (* Printer for subgoal comments *) @@ -35,8 +34,8 @@ let print_hicomment_line ns = let print_tactic_line_with pr arg = (print_string "e ("; pr false arg; print_string ");;\n");; -let print_tactic_line info = - (print_tactic_line_with print_tactic info);; +let print_tactic_line obj = + (print_tactic_line_with print_tactic obj);; let print_hitrace_line_with fl pr htr = match htr with @@ -91,22 +90,22 @@ let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;; let rec print_hiproof2 br h = match h with - Hlabelled (Tactical (Some "REPEAT", _), Hsequence (h1,h2)) (* if repeated *) + Hlabelled (Tactical ("REPEAT", _), Hsequence (h1,h2)) (* if repeated *) -> (print_string_if br "("; print_string "REPEAT "; print_hiproof2 true h1; print_string_if br ")") - | Hlabelled (Tactical (Some "THEN", _), (* if tac2 used *) + | Hlabelled (Tactical ("THEN", _), (* if tac2 used *) Hsequence (h1, Htensor (h2::h2s))) -> (print_string_if br "("; print_hiproof2 false h1; print_string " THEN "; print_hiproof2 true h2; print_string_if br ")") - | Hlabelled (Tactical ((Some "SUBGOAL_THEN", (* special case *) - (Fterm tm)::[farg]) as info), + | Hlabelled (Tactical (("SUBGOAL_THEN", (* special case *) + (Mlterm tm)::[_]) as obj), _) - -> (print_tactic br info) + -> (print_tactic br obj) | Hlabelled (Label x, h) -> (print_string_if br "("; print_string "HILABEL "; @@ -145,7 +144,8 @@ let print_executed_proof fl = print_gtree_executed_proof fl !the_goal_tree;; (* ! 'REPEAT' not currently catered for. *) let print_hiproof_packaged_proof h = - let h' = (thenise_hiproof o trivsimp_hiproof o leftgroup_hiproof) h in + let h' = (trivsimp_hiproof o thenise_hiproof o + trivsimp_hiproof o leftgroup_hiproof) h in print_tactic_line_with print_hiproof2 h';; let print_gtree_packaged_proof gtr = diff --git a/hol-light/TacticRecording/printutils.ml b/hol-light/TacticRecording/printutils.ml index 9131e18d..aa74ee22 100644 --- a/hol-light/TacticRecording/printutils.ml +++ b/hol-light/TacticRecording/printutils.ml @@ -22,34 +22,35 @@ let print_goalid id = print_int id;; let print_indent d = print_string (String.make d ' ');; -(* Printer for 'finfo' *) +(* Printer for 'mldata' *) -let rec print_farg x0 br arg = +let rec print_mlarg br arg = match arg with - Fint n -> print_int n - | Fstring x -> print_fstring x - | Fterm tm -> print_fterm tm - | Ftype ty -> print_ftype ty - | Fthm prf -> print_finfo "" br prf - | Fpair (arg1,arg2) - -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in + Mlint n -> print_int n + | Mlstring x -> print_fstring x + | Mlterm tm -> print_fterm tm + | Mltype ty -> print_ftype ty + | Mlthm prf -> print_mldata br prf + | Mlpair (arg1,arg2) + -> let sep = + if (forall is_atomic_mlarg [arg1;arg2]) then "," else ", " in (print_string_if br "("; - print_farg x0 false arg1; + print_mlarg false arg1; print_string sep; - print_farg x0 false arg2; + print_mlarg false arg2; print_string_if br ")") - | Flist args - -> let sep = if (forall is_atomic_farg args) then ";" else "; " in + | Mllist args + -> let sep = if (forall is_atomic_mlarg args) then ";" else "; " in (print_string "["; - print_seplist (print_farg x0 false) sep args; + print_seplist (print_mlarg false) sep args; print_string "]") - | Ffn f - -> (print_finfo x0 br f) + | Mlfn f + -> (print_mldata br f) -and print_finfo x0 br ((x_,args):finfo) = +and print_mldata br ((x,args):mldata) = (print_string_if (br & not (is_empty args)) "("; - print_option x0 x_; - do_list (fun arg -> print_string " "; print_farg x0 true arg) args; + print_string x; + do_list (fun arg -> print_string " "; print_mlarg true arg) args; print_string_if (br & not (is_empty args)) ")");; @@ -57,5 +58,4 @@ and print_finfo x0 br ((x_,args):finfo) = let print_label l = match l with - Tactical (Some x, _) | Label x -> print_fstring x - | Tactical (None, _) -> print_fstring "";; + Tactical (x,_) | Label x -> print_fstring x;; diff --git a/hol-light/TacticRecording/promote.ml b/hol-light/TacticRecording/promote.ml index cd711707..c19abb8a 100644 --- a/hol-light/TacticRecording/promote.ml +++ b/hol-light/TacticRecording/promote.ml @@ -252,11 +252,15 @@ let BINDER_CONV = conv_conv_wrap "BINDER_CONV" BINDER_CONV;; let SUB_CONV = conv_conv_wrap "SUB_CONV" SUB_CONV;; let BINOP_CONV = conv_conv_wrap "BINOP_CONV" BINOP_CONV;; let GSYM = rule_wrap "GSYM" GSYM;; +let CONJUNCTS = multirule_wrap "CONJUNCTS" CONJUNCTS;; +let SPEC_ALL = rule_wrap "SPEC_ALL" SPEC_ALL;; let ISPECL = termlist_rule_wrap "ISPECL" ISPECL;; let ALL_CONV = conv_wrap "ALL_CONV" ALL_CONV;; let (REPEATC) = conv_conv_wrap "REPEATC" REPEATC;; let ONCE_DEPTH_CONV = conv_conv_wrap "ONCE_DEPTH_CONV" ONCE_DEPTH_CONV;; +let REWRITE_RULE = thmlist_rule_wrap "REWRITE_RULE" REWRITE_RULE;; + let num_CONV = conv_wrap "num_CONV" num_CONV;; let ARITH_RULE = conv_wrap "ARITH_RULE" ARITH_RULE;; @@ -272,14 +276,24 @@ let EQ_IMP = theorem_wrap "EQ_IMP" EQ_IMP;; let ARITH = theorem_wrap "ARITH" ARITH;; let ARITH_EQ = theorem_wrap "ARITH_EQ" ARITH_EQ;; +let ADD_ASSOC = theorem_wrap "ADD_ASSOC" ADD_ASSOC;; let ADD_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;; +let LEFT_ADD_DISTRIB = theorem_wrap "LEFT_ADD_DISTRIB" LEFT_ADD_DISTRIB;; +let RIGHT_ADD_DISTRIB = theorem_wrap "RIGHT_ADD_DISTRIB" RIGHT_ADD_DISTRIB;; let MULT_CLAUSES =theorem_wrap "MULT_CLAUSES" MULT_CLAUSES;; let SUB_REFL = theorem_wrap "SUB_REFL" SUB_REFL;; let ADD1 = theorem_wrap "ADD1" ADD1;; +let EQ_MULT_LCANCEL = theorem_wrap "EQ_MULT_LCANCEL" EQ_MULT_LCANCEL;; +let LE_EXISTS = theorem_wrap "LE_EXISTS" LE_EXISTS;; +let LE_ADD = theorem_wrap "LE_ADD" LE_ADD;; let LE_1 = theorem_wrap "LE_1" LE_1;; let LE_REFL = theorem_wrap "LE_REFL" LE_REFL;; let LT_SUC = theorem_wrap "LT_SUC" LT_SUC;; +let LT_EXISTS = theorem_wrap "LT_EXISTS" LT_EXISTS;; +let LT_NZ = theorem_wrap "LT_NZ" LT_NZ;; +let EXP_EQ_0 = theorem_wrap "EXP_EQ_0" EXP_EQ_0;; let FACT = theorem_wrap "FACT" FACT;; +let = theorem_wrap "" ;; let REAL_ADD_LDISTRIB = theorem_wrap "REAL_ADD_LDISTRIB" REAL_ADD_LDISTRIB;; let REAL_OF_NUM_ADD = theorem_wrap "REAL_OF_NUM_ADD" REAL_OF_NUM_ADD;; diff --git a/hol-light/TacticRecording/tacticrec.ml b/hol-light/TacticRecording/tacticrec.ml index 7df77fad..c65ee71c 100644 --- a/hol-light/TacticRecording/tacticrec.ml +++ b/hol-light/TacticRecording/tacticrec.ml @@ -60,7 +60,7 @@ type ginfo = * unit option ref;; (* Formal proof (optional) *) type gstep = - Gatom of finfo (* Atomic tactic *) + Gatom of mldata (* Atomic tactic *) | Gbox of (label * gtree * bool) (* Box for a tactical; flag for special *) and gtree0 = @@ -80,19 +80,19 @@ and gtree = (* *) (* (_, ref *) (* Gexecuted *) -(* (Gbox (Tactical (Some "T1")) *) +(* (Gbox (Tactical ("T1",[]) *) (* (_, ref *) (* Gexecuted *) -(* (Gatom (Some "T2"), *) -(* [ (_, ref Gexecuted (Gatom (Some "WF"), [])); *) +(* (Gatom ("T2",[]), *) +(* [ (_, ref Gexecuted (Gatom ("WF",[]), [])); *) (* (_, ref Gexit _) ])), *) (* [ (_, ref *) (* Gexecuted *) -(* (Gbox (Tactical (Some "DP")) *) +(* (Gbox (Tactical ("DP",[])) *) (* (_, ref *) (* Gexecuted *) -(* (Gatom (Some "Normalise"), *) -(* [ (_, ref Gexecuted (Gatom (Some "Taut"), [])) ])), *) +(* (Gatom ("Normalise",[]), *) +(* [ (_, ref Gexecuted (Gatom ("Taut",[]), [])) ])), *) (* [])) ])) *) @@ -125,7 +125,7 @@ let gtree_fproof ((info,_):gtree) = ginfo_fproof info;; let gstep_tactic (gstp:gstep) = match gstp with - Gatom info | Gbox (Tactical info, _, true) -> info + Gatom obj | Gbox (Tactical obj, _, true) -> obj | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";; let gtree_proof ((_,gtrm):gtree) = @@ -304,9 +304,11 @@ let (xTAC_PROOF : goal * xtactic -> thm) = let xprove(t,tac) = let th = xTAC_PROOF(([],t),tac) in let t' = concl th in - if t' = t then th else - try EQ_MP (ALPHA t' t) th - with Failure _ -> failwith "prove: justification generated wrong theorem";; + let th' = + if t' = t then th else + try EQ_MP (ALPHA t' t) th + with Failure _ -> failwith "prove: justification generated wrong theorem" in + mk_xthm (th', ("",[])) let xset_goal(asl,w) = current_xgoalstack := diff --git a/hol-light/TacticRecording/wrappers.ml b/hol-light/TacticRecording/wrappers.ml index 1244c89f..115163d4 100644 --- a/hol-light/TacticRecording/wrappers.ml +++ b/hol-light/TacticRecording/wrappers.ml @@ -11,19 +11,19 @@ (* ** THEOREM-RELATED WRAPPER FUNCTIONS ** *) -(* finfo_as_meta_arg *) +(* mldata_as_meta_arg *) -let finfo_as_meta_arg (info:finfo) = - match info with - (x_, ((_::_) as args)) - -> Ffn (x_, front args) - | _ -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";; +let mldata_as_meta_arg (obj:mldata) = + match obj with + (x, ((_::_) as args)) + -> Mlfn (x, front args) + | _ -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";; -let finfo_as_meta2_arg (info:finfo) = - match info with - (x_, ((_::_) as args)) - -> Ffn (x_, (front o front) args) - | _ -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";; +let mldata_as_meta2_arg (obj:mldata) = + match obj with + (x, ((_::_) as args)) + -> Mlfn (x, (front o front) args) + | _ -> failwith "mldata_as_meta_arg: Unexpected empty rule arg list";; (* detect_rule_app *) @@ -34,24 +34,24 @@ let finfo_as_meta2_arg (info:finfo) = (* result is returned along with an 'farg' that captures the rule. *) let detect_rule_app (mfunc:('a->thm)->'b) (xr:'a->xthm) : 'c = - let temp = ref (Ffn (Some "", []) : farg) in + let temp = ref (Mlfn ("", []) : mlarg) in let r arg = let xth = xr arg in - let (th,info) = dest_xthm xth in - (temp := finfo_as_meta_arg info; + let (th,obj) = dest_xthm xth in + (temp := mldata_as_meta_arg obj; th) in let th = mfunc r in (th,!temp);; let detect_metarule_app (mfunc:(('a->thm)->'b->thm)->'c) (xmr:('a->xthm)->'b->xthm) : 'd = - let temp = ref (Ffn (Some "", []) : farg) in + let temp = ref (Mlfn ("",[]) : mlarg) in let mr marg arg = let xmarg arg0 = let th = marg arg0 in - let info = (Some "", [Ffn (Some "",[])]) in - mk_xthm (th,info) in + let obj = ("", [Mlfn ("",[])]) in + mk_xthm (th,obj) in let xth = xmr xmarg arg in - let (th,info) = dest_xthm xth in - (temp := finfo_as_meta2_arg info; + let (th,obj) = dest_xthm xth in + (temp := mldata_as_meta2_arg obj; th) in let th = mfunc mr in (th,!temp);; @@ -60,7 +60,7 @@ let detect_metarule_app (mfunc:(('a->thm)->'b->thm)->'c) (* Theorem wrapper *) let theorem_wrap (x:string) (th:thm) : xthm = - (th, (Some x, []));; + (th, (x,[]));; (* Rule wrappers *) @@ -68,94 +68,109 @@ let theorem_wrap (x:string) (th:thm) : xthm = (* Lots of rule wrappers are required because there are many different type *) (* shapes for rules. *) -let rule_wrap0 finfo (r:'a->thm) (arg:'a) : xthm = +let rule_wrap0 obj (r:'a->thm) (arg:'a) : xthm = let th' = r arg in - mk_xthm (th',finfo);; + mk_xthm (th',obj);; let conv_wrap x (r:term->thm) (tm:term) : xthm = - rule_wrap0 (Some x, [Fterm tm]) r tm;; + rule_wrap0 (x, [Mlterm tm]) r tm;; let thm_conv_wrap x (r:thm->term->thm) (xth:xthm) tm : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;; + rule_wrap0 (x, [Mlthm prf; Mlterm tm]) (r th) tm;; let thmlist_conv_wrap x (r:thm list->term->thm) xths (tm:term) : xthm = let (ths,prfs) = unzip (map dest_xthm xths) in - rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm]) + rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlterm tm]) (r ths) tm;; let rule_wrap x (r:thm->thm) (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Fthm prf]) r th;; + rule_wrap0 (x, [Mlthm prf]) r th;; let drule_wrap x (r:thm->thm->thm) (xth1:xthm) (xth2:xthm) : xthm = let (th1,prf1) = dest_xthm xth1 in let (th2,prf2) = dest_xthm xth2 in - rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;; + rule_wrap0 (x, [Mlthm prf1; Mlthm prf2]) (r th1) th2;; let prule_wrap x (r:thm*thm->thm) ((xth1:xthm),(xth2:xthm)) : xthm = let (th1,prf1) = dest_xthm xth1 in let (th2,prf2) = dest_xthm xth2 in - rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);; + rule_wrap0 (x, [Mlpair(Mlthm prf1, Mlthm prf2)]) r (th1,th2);; let trule_wrap x (r:thm->thm->thm->thm) (xth1:xthm) (xth2:xthm) (xth3:xthm) : xthm = let (th1,prf1) = dest_xthm xth1 in let (th2,prf2) = dest_xthm xth2 in let (th3,prf3) = dest_xthm xth3 in - rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;; + rule_wrap0 (x, [Mlthm prf1; Mlthm prf2; Mlthm prf3]) (r th1 th2) th3;; let term_rule_wrap x (r:term->thm->thm) tm (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;; + rule_wrap0 (x, [Mlterm tm; Mlthm prf]) (r tm) th;; let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;; + rule_wrap0 (x, [Mlpair(Mlterm tm1,Mlterm tm2); Mlthm prf]) (r (tm1,tm2)) th;; let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,xth0) (xth:xthm) : xthm = let (th0,prf0) = dest_xthm xth0 in let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;; + rule_wrap0 (x, [Mlpair(Mlterm tm, Mlthm prf0); Mlthm prf]) (r (tm,th0)) th;; let termlist_rule_wrap x (r:term list->thm->thm) tms (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf]) + rule_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms); Mlthm prf]) (r tms) th;; let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, - [Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta); - Fthm prf]) + rule_wrap0 (x, + [Mllist (map (fun (tm1,tm2) -> Mlpair(Mlterm tm1, Mlterm tm2)) + theta); + Mlthm prf]) (r theta) th;; let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm) theta (xth:xthm) : xthm = let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, - [Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta); - Fthm prf]) + rule_wrap0 (x, + [Mllist (map (fun (tm1,tm2) -> Mlpair(Mltype tm1, Mltype tm2)) + theta); + Mlthm prf]) (r theta) th;; let thmlist_rule_wrap x (r:thm list->thm->thm) xths (xth:xthm) : xthm = let (ths,prfs) = unzip (map dest_xthm xths) in let (th,prf) = dest_xthm xth in - rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf]) + rule_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs); Mlthm prf]) (r ths) th;; +(* Multi-rule wrappers *) + +let multirule_wrap0 obj (r:'a->thm list) (arg:'a) : xthm list = + let ths' = r arg in + let n = length ths' in + let infos' = map (fun i -> ("el", [Mlint i; Mlfn obj])) (0 -- (n-1)) in + map mk_xthm (zip ths' infos');; + +let multirule_wrap x (r:thm->thm list) (xth:xthm) : xthm list = + let (th,prf) = dest_xthm xth in + multirule_wrap0 (x, [Mlthm prf]) r th;; + + (* Meta rule wrappers *) let meta_rule_wrap0 info0 (mr:('a->thm)->'b->thm) (xr:'a->xthm) (arg:'b) : xthm = let (th',f) = detect_rule_app (fun r -> mr r arg) xr in - let (x_,args0) = info0 in - let info' = (x_, f::args0) in - (th',info');; + let (x,args0) = info0 in + let obj' = (x, f::args0) in + (th',obj');; let conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm = - meta_rule_wrap0 (Some x, [Fterm tm]) mc xc tm;; + meta_rule_wrap0 (x, [Mlterm tm]) mc xc tm;; @@ -171,10 +186,10 @@ let conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm = (* returns 'goalstate', but that also returns a 'gstep' summary of the *) (* operation. This is used to promote every basic tactic-based function. *) -let infotactic_wrap (infotac:goal->goalstate*finfo) (xg:xgoal) : xgoalstate = +let infotactic_wrap (infotac:goal->goalstate*mldata) (xg:xgoal) : xgoalstate = let (g,id) = dest_xgoal xg in - let ((meta,gs,just),info) = infotac g in - let xgs = extend_gtree id (Gatom info) gs in + let ((meta,gs,just),obj) = infotac g in + let xgs = extend_gtree id (Gatom obj) gs in (meta,xgs,just);; @@ -203,36 +218,36 @@ let infobox_wrap (xinfotac:xgoal->xgoalstate*label) (xg:xgoal) : xgoalstate = (* This is for wrapping around a tactic, to promote it to work on xgoals and *) (* incorporate the results into an existing gtree. *) -let tactic_wrap0 info (tac:tactic) : xtactic = - let infotac g = (tac g, info) in +let tactic_wrap0 obj (tac:tactic) : xtactic = + let infotac g = (tac g, obj) in infotactic_wrap infotac;; let tactic_wrap x tac = - tactic_wrap0 (Some x, []) tac;; + tactic_wrap0 (x, []) tac;; let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic = - tactic_wrap0 (Some x, [Fstring s]) (tac s);; + tactic_wrap0 (x, [Mlstring s]) (tac s);; let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic = - tactic_wrap0 (Some x, [Fterm tm]) (tac tm);; + tactic_wrap0 (x, [Mlterm tm]) (tac tm);; let termpair_tactic_wrap x (tac:term*term->tactic) (tm1,tm2) : xtactic = - tactic_wrap0 (Some x, [Fpair (Fterm tm1, Fterm tm2)]) (tac (tm1,tm2));; + tactic_wrap0 (x, [Mlpair (Mlterm tm1, Mlterm tm2)]) (tac (tm1,tm2));; let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic = - tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms)]) (tac tms);; + tactic_wrap0 (x, [Mllist (map (fun tm -> Mlterm tm) tms)]) (tac tms);; let thm_tactic_wrap x (tac:thm->tactic) (xth:xthm) : xtactic = let (th,prf) = dest_xthm xth in - tactic_wrap0 (Some x, [Fthm prf]) (tac th);; + tactic_wrap0 (x, [Mlthm prf]) (tac th);; let thmlist_tactic_wrap x (tac:thm list->tactic) (xths:xthm list) : xtactic = let (ths,prfs) = unzip (map dest_xthm xths) in - tactic_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs)]) (tac ths);; + tactic_wrap0 (x, [Mllist (map (fun prf -> Mlthm prf) prfs)]) (tac ths);; let stringthm_tactic_wrap x (tac:string->thm->tactic) s (xth:xthm) : xtactic = let (th,prf) = dest_xthm xth in - tactic_wrap0 (Some x, [Fstring s; Fthm prf]) (tac s th);; + tactic_wrap0 (x, [Mlstring s; Mlthm prf]) (tac s th);; (* Meta-tactic wrapper *) @@ -243,27 +258,27 @@ let meta_tactic_wrap0 info0 (mtac:('a->thm)->tactic) (xr:'a->xthm) : xtactic = let infotac g = let (gst,f) = detect_rule_app (fun r -> mtac r g) xr in - let (x_,args0) = info0 in - let info = (x_, f::args0) in - (gst,info) in + let (x,args0) = info0 in + let obj = (x, f::args0) in + (gst,obj) in infotactic_wrap infotac;; let conv_tactic_wrap x (mtac:conv->tactic) (xc:xconv) : xtactic = - meta_tactic_wrap0 (Some x, []) mtac xc;; + meta_tactic_wrap0 (x, []) mtac xc;; let metameta_tactic_wrap info0 (mmtac:(('a->thm)->'b->thm)->tactic) (xmr:('a->xthm)->'b->xthm) : xtactic = let infotac g = let (gst,f) = detect_metarule_app (fun mr -> mmtac mr g) xmr in - let (x_,args0) = info0 in - let info = (x_, f::args0) in - (gst,info) in + let (x,args0) = info0 in + let obj = (x, f::args0) in + (gst,obj) in infotactic_wrap infotac;; let convconvthmlist_tactic_wrap x (mmtac:(conv->conv)->thm list->tactic) (xmc:xconv->xconv) (xths:xthm list) : xtactic = let (ths,prfs) = unzip (map dest_xthm xths) in - metameta_tactic_wrap (Some x, [Flist (map (fun prf -> Fthm prf) prfs)]) + metameta_tactic_wrap (x, [Mllist (map (fun prf -> Mlthm prf) prfs)]) (fun mc -> mmtac mc ths) xmc;; @@ -277,22 +292,22 @@ let convconvthmlist_tactic_wrap x (mmtac:(conv->conv)->thm list->tactic) (* already be promoted to work with xtactics and xgoals. This must done by *) (* hand for each tactical by trivially adjusting its original source code. *) -let tactical_wrap0 info (xttcl:'a->xtactic) (arg:'a) : xtactic = - let xinfotac xg = (xttcl arg xg, Tactical info) in +let tactical_wrap0 obj (xttcl:'a->xtactic) (arg:'a) : xtactic = + let xinfotac xg = (xttcl arg xg, Tactical obj) in infobox_wrap xinfotac;; let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic = - tactical_wrap0 (Some x, []) xttcl xtac;; + tactical_wrap0 (x,[]) xttcl xtac;; let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic = - tactical_wrap0 (Some x, []) (xttcl xtac1) xtac2;; + tactical_wrap0 (x,[]) (xttcl xtac1) xtac2;; let int_tactical_wrap x (xttcl:int->'a->xtactic) (n:int) (xtac:'a) : xtactic = - tactical_wrap0 (Some x, [Fint n]) (xttcl n) xtac;; + tactical_wrap0 (x, [Mlint n]) (xttcl n) xtac;; let list_tactical_wrap x (xttcl:('a->xtactic)->'a list->xtactic) (xtac:'a->xtactic) (l:'a list) : xtactic = - tactical_wrap0 (Some x, []) (xttcl xtac) l;; + tactical_wrap0 (x,[]) (xttcl xtac) l;; (* HILABEL *) @@ -319,11 +334,11 @@ let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (xg:xgoal) : xgoalstate = let (asl,_) = g in let g2 = (asl,tm) in - let finfo = (Some "SUBGOAL_THEN", - [Fterm tm; (finfo_as_meta_arg o gtree_tactic) gtr0]) in + let obj = ("SUBGOAL_THEN", + [Mlterm tm; (mldata_as_meta_arg o gtree_tactic) gtr0]) in let (gs0,ids0) = unzip (map dest_xgoal xgs0) in - let xgs = extend_gtree id (Gbox (Tactical finfo, gtr0, true)) (g2::gs0) in + let xgs = extend_gtree id (Gbox (Tactical obj, gtr0, true)) (g2::gs0) in let ids1 = map xgoal_id (tl xgs) in let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in (do_list externalise_gtree (zip ids0 ids1); diff --git a/hol-light/TacticRecording/xtactics.ml b/hol-light/TacticRecording/xtactics.ml index 79b81648..fb7028c7 100644 --- a/hol-light/TacticRecording/xtactics.ml +++ b/hol-light/TacticRecording/xtactics.ml @@ -381,9 +381,11 @@ let (xTAC_PROOF : goal * xtactic -> thm) = let xprove(t,tac) = let th = xTAC_PROOF(([],t),tac) in let t' = concl th in - if t' = t then th else - try EQ_MP (ALPHA t' t) th - with Failure _ -> failwith "prove: justification generated wrong theorem";; + let th' = + if t' = t then th else + try EQ_MP (ALPHA t' t) th + with Failure _ -> failwith "prove: justification generated wrong theorem" in + mk_xthm (th', ("",[])) (* ------------------------------------------------------------------------- *) (* Subgoal package for xgoals. *) @@ -439,7 +441,7 @@ let xtop_goal() = let xtop_thm() = let (_,[],f)::_ = !current_xgoalstack in - f null_inst [];; + mk_xthm (f null_inst [], ("",[]));; (* ------------------------------------------------------------------------- *) (* Install the goal-related printers. *) diff --git a/hol-light/TacticRecording/xthm.ml b/hol-light/TacticRecording/xthm.ml index 2619e03f..97fcec57 100644 --- a/hol-light/TacticRecording/xthm.ml +++ b/hol-light/TacticRecording/xthm.ml @@ -1,73 +1,40 @@ -(* ** DATATYPES ** *) - - -type farg = - Fint of int - | Fstring of string - | Fterm of term - | Ftype of hol_type - | Fthm of finfo - | Fpair of farg * farg - | Flist of farg list - | Ffn of finfo - -and finfo = - string option (* Function's name *) - * farg list;; (* Function's args *) - - -type label = - Tactical of finfo - | Label of string;; - - -(* Atomic tests *) - -let is_atomic_farg arg = - match arg with - Fthm (_,(_::_)) | Fpair _ -> false - | _ -> true;; - -let is_atomic_finfo ((x_,args):finfo) = (is_empty args);; - - -(* active_info *) - -let active_info = (Some "...", []);; +(* ** DATATYPE ** *) (* The 'xthm' datatype *) -(* This couples a theorem with an 'finfo' representation of its proof. For *) -(* named ML objects, this 'finfo' will simply be the ML name of the theorem. *) +(* This couples a theorem with an 'mldata' representation of its proof. For *) +(* named ML objects, this 'mldata' will simply be the ML name of the theorem. *) (* For rule applications, it will capture the rule and its arguments. *) -type xthm = thm * finfo;; +type xthm = thm * mldata;; type xconv = term -> xthm;; (* Constructors and destructors *) -let mk_xthm (xth:thm*finfo) : xthm = xth;; +let mk_xthm (xth:thm*mldata) : xthm = xth;; -let mk_xthm0 x th = mk_xthm (th, (Some x, []));; +let mk_xthm0 x th = mk_xthm (th, (x,[]));; -let dest_xthm ((th,info):xthm) : thm * finfo = (th,info);; +let dest_xthm ((th,prf):xthm) : thm * mldata = (th,prf);; let xthm_thm ((th,_):xthm) = th;; -let xthm_proof ((_,info):xthm) = info;; +let xthm_proof ((_,prf):xthm) = prf;; + +let name_xthm x ((th,_):xthm) : xthm = (th, (x,[]));; (* ** INSTALL PRINTERS ** *) -let print_xthm ((th,info):xthm) = print_thm th;; +let print_xthm ((th,_):xthm) = print_thm th;; #install_printer print_xthm;; -- cgit v1.2.3