From 6ecd3be998c4d2a6d8dae8ec2f67c50305a251ef Mon Sep 17 00:00:00 2001 From: mark <> Date: Tue, 21 Feb 2012 14:46:38 +0000 Subject: Various small improvements to capability Whole of examples3 now processes Facility for adding manual labels to atomic/composite tactics --- hol-light/TacticRecording/examples3.ml | 67 ++++++- hol-light/TacticRecording/examples5.ml | 79 ++++++++ hol-light/TacticRecording/hiproofs.ml | 14 +- hol-light/TacticRecording/main.ml | 11 ++ hol-light/TacticRecording/mlexport.ml | 24 ++- hol-light/TacticRecording/promote.ml | 20 +- hol-light/TacticRecording/tacticrec.ml | 170 ++-------------- hol-light/TacticRecording/wrappers.ml | 344 +++++++++++++++++++++++++++++++++ hol-light/TacticRecording/xthm.ml | 130 +------------ 9 files changed, 557 insertions(+), 302 deletions(-) create mode 100644 hol-light/TacticRecording/examples5.ml create mode 100644 hol-light/TacticRecording/wrappers.ml (limited to 'hol-light') diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml index a8fcdb16..d0e181e2 100644 --- a/hol-light/TacticRecording/examples3.ml +++ b/hol-light/TacticRecording/examples3.ml @@ -5,6 +5,9 @@ needs "Library/products.ml";; prioritize_real();; +AIM: CONT_COMPOSE (Library/analysis.ml) +- used by John in his Proof Style paper + (* ** LEMMA1 from HOL Light's 100/arithmetic_geometric_mean.ml ** *) @@ -20,17 +23,50 @@ let LEMMA_1 = prove 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);; +let LEMMA_1 = prove + (`!x n. x pow (n + 1) - (&n + &1) * x + &n = + (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`, + 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 + [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));; + let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;; top_thm ();; print_executed_proof true;; -print_flat_proof true;; +print_flat_proof false;; print_packaged_proof ();; +print_thenl_proof ();; g `!x n. x pow (n + 1) - (&n + &1) * x + &n = (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`;; +e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));; +e (GEN_TAC);; +e (INDUCT_TAC);; +(* *** Subgoal 1 *** *) +e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);; +e (REAL_ARITH_TAC);; +(* *** Subgoal 2 *** *) +e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);; +e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);; +e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);; +e (REWRITE_TAC [real_pow;REAL_MUL_RID]);; +e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);; +e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);; +e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);; +e (REAL_ARITH_TAC);; -print_executed_proof ();; +print_executed_proof true;; +print_packaged_proof ();; +print_thenl_proof ();; (* LEMMA 2 *) @@ -108,3 +144,30 @@ let AGM = prove ARITH_RULE `i <= n ==> i <= n + 1`] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_RMUL THEN ASM_SIMP_TAC[LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]]);; + +g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i)) + ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;; +e (INDUCT_TAC);; +(* *** Subgoal 1 *** *) +e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);; +(* *** Subgoal 2 *** *) +e (REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG]);; +e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);; +e (X_GEN_TAC `x:num->real`);; +e (ASM_CASES_TAC `n = 0`);; +(* *** Subgoal 2.1 *** *) +e (ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG]);; +e (REAL_ARITH_TAC);; +(* *** Subgoal 2.2 *** *) +e (REWRITE_TAC [ADD1]);; +e (STRIP_TAC);; +e (MATCH_MP_TAC REAL_LE_TRANS);; +e (EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n`);; +e (ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]);; +e (GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM]);; +e (MATCH_MP_TAC REAL_LE_RMUL);; +e (ASM_SIMP_TAC [LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]);; + +g `!n a. 1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a(i)) + ==> product(1..n) a <= (sum(1..n) a / &n) pow n`;; +e (INDUCT_TAC THEN REWRITE_TAC [ARITH;PRODUCT_CLAUSES_NUMSEG] THEN REWRITE_TAC [ARITH_RULE `1 <= SUC n`] THEN X_GEN_TAC `x:num->real` THEN ASM_CASES_TAC `n = 0` THENL [ASM_REWRITE_TAC [PRODUCT_CLAUSES_NUMSEG;ARITH;SUM_SING_NUMSEG] THEN REAL_ARITH_TAC; REWRITE_TAC [ADD1] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x (n + 1) * (sum (1..n) x / &n) pow n` THEN ASM_SIMP_TAC [LEMMA_3; GSYM REAL_OF_NUM_ADD; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_RMUL THEN ASM_SIMP_TAC [LE_REFL; LE_1; ARITH_RULE `i <= n ==> i <= n + 1`]]);; diff --git a/hol-light/TacticRecording/examples5.ml b/hol-light/TacticRecording/examples5.ml new file mode 100644 index 00000000..6e34aaee --- /dev/null +++ b/hol-light/TacticRecording/examples5.ml @@ -0,0 +1,79 @@ +from Library/binomial.ml + +prioritize_num();; + +(* ------------------------------------------------------------------------- *) +(* Binomial coefficients. *) +(* ------------------------------------------------------------------------- *) + +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;; + +(* ------------------------------------------------------------------------- *) +(* More potentially useful lemmas. *) +(* ------------------------------------------------------------------------- *) + +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;; diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml index b48dd2da..41941cde 100644 --- a/hol-light/TacticRecording/hiproofs.ml +++ b/hol-light/TacticRecording/hiproofs.ml @@ -30,7 +30,7 @@ type hiproof = Hactive (* Active subgoal *) | Hatomic of (finfo * int) (* Atomic tactic + arity *) | Hidentity (* Null, for wiring *) - | Hlabelled of (finfo * hiproof) (* Box *) + | Hlabelled of (label * hiproof) (* Box *) | Hsequence of (hiproof * hiproof) (* Serial application *) | Htensor of hiproof list (* Parallel application *) | Hempty;; (* Completed goal *) @@ -87,9 +87,9 @@ type hitrace = let rec refactor_hiproof r foo h = let h' = match h with - Hlabelled (info,h0) + Hlabelled (l,h0) -> let h0' = refactor_hiproof r foo h0 in - Hlabelled (info,h0') + Hlabelled (l,h0') | Hsequence (h1,h2) -> let h1' = refactor_hiproof r foo h1 in let h2' = refactor_hiproof r foo h2 in @@ -169,7 +169,7 @@ let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);; let delabel_hiproof h = let delabel h = match h with - Hlabelled ((Some "SUBGOAL_THEN",_),h0) + Hlabelled (Tactical (Some "SUBGOAL_THEN",_), h0) -> h | Hlabelled (_,h0) -> h0 @@ -221,12 +221,12 @@ let thenise_hiproof h = match h with Hsequence (h1, Htensor (h2::h2s)) -> if (forall (fun h0 -> h0 = h2) h2s) - then Hlabelled ((Some "THEN", []), h) + 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 ((Some "THEN", []), + (Hlabelled (Tactical (Some "THEN", []), Hsequence (h1, Htensor (h2::h2s))), h3) else h | _ -> h in @@ -250,7 +250,7 @@ let rec hiproof_tactic_trace0 h = -> [info] | Hidentity -> [] - | Hlabelled (info,h0) + | Hlabelled (_,h0) -> hiproof_tactic_trace0 h0 | Hsequence (h1,h2) -> (hiproof_tactic_trace0 h1) @ (hiproof_tactic_trace0 h2) diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml index 2dd6e6ef..44c01951 100644 --- a/hol-light/TacticRecording/main.ml +++ b/hol-light/TacticRecording/main.ml @@ -1,14 +1,25 @@ +(* Library stuff *) #use "TacticRecording/lib.ml";; #use "TacticRecording/dltree.mli";; #use "TacticRecording/dltree.ml";; +(* Datatypes and recording mechanism *) + #use "TacticRecording/xthm.ml";; #use "TacticRecording/xtactics.ml";; #use "TacticRecording/tacticrec.ml";; +#use "TacticRecording/wrappers.ml";; + +(* Prooftree support *) + #use "TacticRecording/prooftree.ml";; +(* Hiproofs, refactoring and export *) + #use "TacticRecording/hiproofs.ml";; #use "TacticRecording/mlexport.ml";; +(* Overwriting the existing HOL Light objects *) + #use "TacticRecording/promote.ml";; diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml index ba26034a..d790deee 100644 --- a/hol-light/TacticRecording/mlexport.ml +++ b/hol-light/TacticRecording/mlexport.ml @@ -24,10 +24,10 @@ let rec gtree_to_hiproof gtr = | Gexecuted (gstp,gtrs) -> let h1 = match gstp with - Gatom info | Gbox (info,_,true) + Gatom info | Gbox (Tactical info, _, true) -> Hatomic (info, length gtrs) - | Gbox (info,gtr,false) - -> Hlabelled (info, gtree_to_hiproof gtr) in + | Gbox (l,gtr,false) + -> Hlabelled (l, gtree_to_hiproof gtr) in let h2 = Htensor (map gtree_to_hiproof gtrs) in Hsequence (h1,h2);; @@ -122,7 +122,7 @@ let print_hiproof0 pr br h = -> print_tactic br info | Hidentity -> print_string "ALL_TAC" - | Hlabelled (info,h0) + | Hlabelled (_,h0) -> pr br h0 | Hsequence (h1, Htensor h2s) -> (print_string_if br "("; @@ -154,20 +154,28 @@ let rec print_hiproof1 br h = print_hiproof0 print_hiproof1 br h;; let rec print_hiproof2 br h = match h with - Hlabelled ((Some "REPEAT", _), Hsequence (h1,h2)) (* only if repeats *) + Hlabelled (Tactical (Some "REPEAT", _), Hsequence (h1,h2)) (* if repeated *) -> (print_string_if br "("; print_string "REPEAT "; print_hiproof2 true h1; print_string_if br ")") - | Hlabelled ((Some "THEN", _), - Hsequence (h1, Htensor (h2::h2s))) (* only if tac2 used *) + | Hlabelled (Tactical (Some "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 (((Some "SUBGOAL_THEN", (Fterm tm)::[farg]) as info), _) + | Hlabelled (Tactical ((Some "SUBGOAL_THEN", (* special case *) + (Fterm tm)::[farg]) as info), + _) -> (print_tactic br info) + | Hlabelled (Label x, h) + -> (print_string_if br "("; + print_string "HILABEL "; + print_fstring x; print_string " "; + print_hiproof2 true h; + print_string_if br ")") | _ -> (print_hiproof0 print_hiproof2 br h);; diff --git a/hol-light/TacticRecording/promote.ml b/hol-light/TacticRecording/promote.ml index 0b40b5f9..cd711707 100644 --- a/hol-light/TacticRecording/promote.ml +++ b/hol-light/TacticRecording/promote.ml @@ -24,6 +24,8 @@ let ASSUME_TAC = thm_tactic_wrap "ASSUME_TAC" ASSUME_TAC;; let ACCEPT_TAC = thm_tactic_wrap "ACCEPT_TAC" ACCEPT_TAC;; +let CONV_TAC = conv_tactic_wrap "CONV_TAC" CONV_TAC;; + let REFL_TAC = tactic_wrap "REFL_TAC" REFL_TAC;; let ABS_TAC = tactic_wrap "ABS_TAC" ABS_TAC;; let MK_COMB_TAC = tactic_wrap "MK_COMB_TAC" MK_COMB_TAC;; @@ -65,7 +67,6 @@ let ANTS_TAC = tactic_wrap "ANTS_TAC" ANTS_TAC;; (* Special cases, already fully hand-promoted *) -let CONV_TAC = xCONV_TAC;; let SUBGOAL_THEN = xSUBGOAL_THEN;; @@ -218,6 +219,8 @@ let PURE_ASM_REWRITE_TAC = thmlist_tactic_wrap "PURE_ASM_REWRITE_TAC" PURE_ASM_REWRITE_TAC;; let ONCE_ASM_REWRITE_TAC = thmlist_tactic_wrap "ONCE_ASM_REWRITE_TAC" ONCE_ASM_REWRITE_TAC;; +let GEN_REWRITE_TAC = + convconvthmlist_tactic_wrap "GEN_REWRITE_TAC" GEN_REWRITE_TAC;; let SIMP_TAC = thmlist_tactic_wrap "SIMP_TAC" SIMP_TAC;; let PURE_SIMP_TAC = thmlist_tactic_wrap "PURE_SIMP_TAC" PURE_SIMP_TAC;; let ONCE_SIMP_TAC = thmlist_tactic_wrap "ONCE_SIMP_TAC" ONCE_SIMP_TAC;; @@ -241,12 +244,20 @@ let ASM_REAL_ARITH_TAC = tactic_wrap "ASM_REAL_ARITH_TAC" ASM_REAL_ARITH_TAC;; (* More rules *) +let RATOR_CONV = conv_conv_wrap "RATOR_CONV" RATOR_CONV;; +let RAND_CONV = conv_conv_wrap "RAND_CONV" RAND_CONV;; +let LAND_CONV = conv_conv_wrap "LAND_CONV" LAND_CONV;; +let ABS_CONV = conv_conv_wrap "ABS_CONV" ABS_CONV;; +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 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 num_CONV = conv_wrap "num_CONV" num_CONV;; let ARITH_RULE = conv_wrap "ARITH_RULE" ARITH_RULE;; let REAL_ARITH = conv_wrap "REAL_ARITH" REAL_ARITH;; @@ -262,9 +273,13 @@ 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_CLAUSES = theorem_wrap "ADD_CLAUSES" ADD_CLAUSES;; +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 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 FACT = theorem_wrap "FACT" FACT;; 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;; @@ -294,4 +309,5 @@ let SUM_ADD_SPLIT = theorem_wrap "SUM_ADD_SPLIT" SUM_ADD_SPLIT;; let SUM_POS_LE_NUMSEG = theorem_wrap "SUM_POS_LE_NUMSEG" SUM_POS_LE_NUMSEG;; let SUM_CLAUSES_NUMSEG = theorem_wrap "SUM_CLAUSES_NUMSEG" SUM_CLAUSES_NUMSEG;; let SUM_SING_NUMSEG = theorem_wrap "SUM_SING_NUMSEG" SUM_SING_NUMSEG;; -let PRODUCT_CLAUSES_NUMSEG = theorem_wrap "PRODUCT_CLAUSES_NUMSEG" PRODUCT_CLAUSES_NUMSEG;; \ No newline at end of file +let PRODUCT_CLAUSES_NUMSEG = + theorem_wrap "PRODUCT_CLAUSES_NUMSEG" PRODUCT_CLAUSES_NUMSEG;; \ No newline at end of file diff --git a/hol-light/TacticRecording/tacticrec.ml b/hol-light/TacticRecording/tacticrec.ml index 0836f87c..7df77fad 100644 --- a/hol-light/TacticRecording/tacticrec.ml +++ b/hol-light/TacticRecording/tacticrec.ml @@ -61,7 +61,7 @@ type ginfo = type gstep = Gatom of finfo (* Atomic tactic *) - | Gbox of (finfo * gtree * bool) (* Box for a tactical; flag for special *) + | Gbox of (label * gtree * bool) (* Box for a tactical; flag for special *) and gtree0 = Gactive (* Active goal *) @@ -80,7 +80,7 @@ and gtree = (* *) (* (_, ref *) (* Gexecuted *) -(* (Gbox (Some "T1") *) +(* (Gbox (Tactical (Some "T1")) *) (* (_, ref *) (* Gexecuted *) (* (Gatom (Some "T2"), *) @@ -88,7 +88,7 @@ and gtree = (* (_, ref Gexit _) ])), *) (* [ (_, ref *) (* Gexecuted *) -(* (Gbox (Some "DP") *) +(* (Gbox (Tactical (Some "DP")) *) (* (_, ref *) (* Gexecuted *) (* (Gatom (Some "Normalise"), *) @@ -125,7 +125,8 @@ let gtree_fproof ((info,_):gtree) = ginfo_fproof info;; let gstep_tactic (gstp:gstep) = match gstp with - Gatom info | Gbox (info,_,_) -> info;; + Gatom info | Gbox (Tactical info, _, true) -> info + | Gbox _ -> failwith "gstep_tactic: Not an atomic tactic";; let gtree_proof ((_,gtrm):gtree) = match (!gtrm) with @@ -206,8 +207,8 @@ let rec gtree_all_children gtr = and gstep_all_children gstp = match gstp with - Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr) - | Gatom _ | Gbox _ -> [];; + Gatom _ | Gbox (_,_,true) -> [] + | Gbox (_,gtr,false) -> gtr::(gtree_all_children gtr);; @@ -243,9 +244,9 @@ let extend_gtree (pid:goalid) (gstp:gstep) (gs':goal list) : xgoal list = with Assert_failure _ -> failwith "extend_gtree: Internal error - Not active" in let (ids',gtrs) = unzip (map (new_active_subgtree pid) gs') in - let gxs' = zip gs' ids' in + let xgs' = zip gs' ids' in (gtrm := Gexecuted (gstp,gtrs); - gxs');; + xgs');; (* Deletion *) @@ -276,153 +277,6 @@ let externalise_gtree ((id0,id):goalid*goalid) : unit = -(* ** WRAPPER FUNCTIONS ** *) - -(* These functions are for promoting existing tactics and tacticals. *) - - -(* Tactic wrapper *) - -(* 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 finfo (tac:tactic) (gx:xgoal) : xgoalstate = - let (g,id) = dest_xgoal gx in - let (meta,gs',just) = tac g in - let gxs' = extend_gtree id (Gatom finfo) gs' in - (meta,gxs',just);; - -let tactic_wrap x tac = - tactic_wrap0 (Some x, []) tac;; - -let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic = - tactic_wrap0 (Some x, [Fstring s]) (tac s);; - -let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic = - tactic_wrap0 (Some x, [Fterm 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));; - -let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic = - tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm 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);; - -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);; - -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);; - - -(* xCONV_TAC - a special case I think; not a tactical *) - -let t_tm = `T`;; - -let xCONV_TAC (cx:xconv) (gx:xgoal) : xgoalstate = - let (g,id) = dest_xgoal gx in - - let (asl,w) = g in - let thx = cx w in - let (th,proof) = dest_xthm thx in - let tm = concl th in - let finfo = (Some "CONV_TAC", [finfo_as_meta_arg proof]) in - - let tac g = - if (aconv tm w) - then (null_meta, [], fun i [] -> INSTANTIATE_ALL i th) - else let l,r = dest_eq tm in - if not (aconv l w) - then failwith "CONV_TAC: bad equation" - else if (r = t_tm) - then (null_meta, [], fun i [] -> INSTANTIATE_ALL i (EQT_ELIM th)) - else (null_meta, [(asl,r)], - fun i [th0] -> EQ_MP (INSTANTIATE_ALL i (SYM th)) th0) in - - let (meta,gs,just) = tac g in - let gxs = extend_gtree id (Gatom finfo) gs in - (meta,gxs,just);; - - -(* Tactical wrapper *) - -(* This is for wrapping around a tactical, to incorporate the results into a *) -(* box in an existing gtree, where the execution of the tactical's tactics is *) -(* captured inside the box, so that they can be stepped through and/or *) -(* refactored. Thus we cannot take the tactical as a black box; it must *) -(* 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 finfo (xttcl:'a->xtactic) (arg:'a) (gx:xgoal) : xgoalstate = - let (g,id) = dest_xgoal gx in - let (id0,gtr0) = new_active_subgtree id g in - let gx0 = mk_xgoal (g,id0) in - let (meta,gxs0,just) = xttcl arg gx0 in - let (gs0,ids0) = unzip (map dest_xgoal gxs0) in - let gxs = extend_gtree id (Gbox (finfo,gtr0,false)) gs0 in - let ids = map xgoal_id gxs in - (do_list externalise_gtree (zip ids0 ids); - (meta,gxs,just));; - -let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic = - tactical_wrap0 (Some x, []) xttcl xtac;; - -let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic = - tactical_wrap0 (Some 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;; - -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;; - - -(* xSUBGOAL_THEN - seems to be another special case *) - -let xASSUME = conv_wrap "ASSUME" ASSUME;; - -let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (gx:xgoal) : xgoalstate = - let arg = xASSUME tm in - - let (g,id) = dest_xgoal gx in - let (id0,gtr0) = new_active_subgtree id g in - let gx0 = mk_xgoal (g,id0) in - let (meta,gxs0,just) = ttac arg gx0 in - let (gs0,ids0) = unzip (map dest_xgoal gxs0) in - - 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 gxs = extend_gtree id (Gbox (finfo,gtr0,true)) (g2::gs0) in - let ids1 = map xgoal_id (tl gxs) in - let just' = fun i l -> PROVE_HYP (hd l) (just i (tl l)) in - (do_list externalise_gtree (zip ids0 ids1); - (meta,gxs,just'));; - - -(* -let SUBGOAL_TAC s tm prfs = - match prfs with - p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored"; - SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC]) - | [] -> failwith "SUBGOAL_TAC: no subproof given";; - -let (FREEZE_THEN :thm_tactical) = - fun ttac th (asl,w) -> - let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in - meta,gl,fun i l -> PROVE_HYP th (just i l);; -*) - - - (* ** SUBGOAL PACKAGE OPERATIONS FOR XGOALS ** *) (* A few of the xtactic subgoal package commands are adjusted here. *) @@ -470,12 +324,12 @@ let xg t = (* Undoing a tactic proof step *) -(* 'xb' needs to be adjusted to deleted the undone step in the goal tree. *) +(* 'xb' needs to be adjusted to delete the undone step in the goal tree. *) let xb () = let result = xb () in - let (_,gxs,_) = hd result in - let (_,id) = hd gxs in + let (_,xgs,_) = hd result in + let (_,id) = hd xgs in (delete_step id; result);; diff --git a/hol-light/TacticRecording/wrappers.ml b/hol-light/TacticRecording/wrappers.ml new file mode 100644 index 00000000..1244c89f --- /dev/null +++ b/hol-light/TacticRecording/wrappers.ml @@ -0,0 +1,344 @@ +(* ========================================================================== *) +(* WRAPPER FUNCTIONS (HOL LIGHT) *) +(* - Functions for promoting thm/goal-related ML objects for xthm/xgoal *) +(* *) +(* By Mark Adams *) +(* Copyright (c) Univeristy of Edinburgh, 2011-2012 *) +(* ========================================================================== *) + + + +(* ** THEOREM-RELATED WRAPPER FUNCTIONS ** *) + + +(* finfo_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 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";; + + +(* detect_rule_app *) + +(* Based on the assumption that the given meta function actually executes its *) +(* rule argument at some point, this utility detects such an execution during *) +(* the demotion of a given xrule argument to a rule. The meta function's *) +(* 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 r arg = let xth = xr arg in + let (th,info) = dest_xthm xth in + (temp := finfo_as_meta_arg info; + 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 mr marg arg = let xmarg arg0 = + let th = marg arg0 in + let info = (Some "", [Ffn (Some "",[])]) in + mk_xthm (th,info) in + let xth = xmr xmarg arg in + let (th,info) = dest_xthm xth in + (temp := finfo_as_meta2_arg info; + th) in + let th = mfunc mr in + (th,!temp);; + + +(* Theorem wrapper *) + +let theorem_wrap (x:string) (th:thm) : xthm = + (th, (Some x, []));; + + +(* Rule wrappers *) + +(* 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 th' = r arg in + mk_xthm (th',finfo);; + +let conv_wrap x (r:term->thm) (tm:term) : xthm = + rule_wrap0 (Some x, [Fterm 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;; + +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]) + (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;; + +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;; + +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);; + +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;; + +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;; + +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;; + +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;; + +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]) + (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]) + (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]) + (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]) + (r ths) 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 conv_conv_wrap x (mc:conv->conv) (xc:term->xthm) (tm:term) : xthm = + meta_rule_wrap0 (Some x, [Fterm tm]) mc xc tm;; + + + +(* ** TACTIC-RELATED WRAPPER FUNCTIONS ** *) + +(* These functions are for promoting existing tactics and tacticals. *) + + +(* Generic basic wrapper util *) + +(* Applies a tactic and incorproates the results into the goal tree. Takes *) +(* an "infotactic", i.e. like a normal tactic that works on 'goal' and *) +(* 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 (g,id) = dest_xgoal xg in + let ((meta,gs,just),info) = infotac g in + let xgs = extend_gtree id (Gatom info) gs in + (meta,xgs,just);; + + +(* Generic box wrapper util *) + +(* Sets up a box to apply an xtactic within, applies the xtactic (which *) +(* incorporates itself into the goal tree) and wires up the resulting *) +(* subgoals to external subgoals of the box. Note that this is not quite *) +(* generic enough for 'SUBGOAL_THEN' (because there is not a total surjection *) +(* between internal and external goals). *) + +let infobox_wrap (xinfotac:xgoal->xgoalstate*label) (xg:xgoal) : xgoalstate = + let (g,id) = dest_xgoal xg in + let (id0,gtr0) = new_active_subgtree id g in + let xg0 = mk_xgoal (g,id0) in + let ((meta,xgs0,just),l) = xinfotac xg0 in + let (gs0,ids0) = unzip (map dest_xgoal xgs0) in + let xgs = extend_gtree id (Gbox (l,gtr0,false)) gs0 in + let ids = map xgoal_id xgs in + (do_list externalise_gtree (zip ids0 ids); + (meta,xgs,just));; + + +(* Tactic wrapper *) + +(* 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 + infotactic_wrap infotac;; + +let tactic_wrap x tac = + tactic_wrap0 (Some x, []) tac;; + +let string_tactic_wrap x (tac:string->tactic) (s:string) : xtactic = + tactic_wrap0 (Some x, [Fstring s]) (tac s);; + +let term_tactic_wrap x (tac:term->tactic) (tm:term) : xtactic = + tactic_wrap0 (Some x, [Fterm 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));; + +let termlist_tactic_wrap x (tac:term list->tactic) tms : xtactic = + tactic_wrap0 (Some x, [Flist (map (fun tm -> Fterm 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);; + +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);; + +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);; + + +(* Meta-tactic wrapper *) + +(* For tactics that take rule arguments. *) + +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 + infotactic_wrap infotac;; + +let conv_tactic_wrap x (mtac:conv->tactic) (xc:xconv) : xtactic = + meta_tactic_wrap0 (Some 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 + 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)]) + (fun mc -> mmtac mc ths) + xmc;; + + +(* Tactical wrapper *) + +(* This is for wrapping around a tactical, to incorporate the results into a *) +(* box in an existing gtree, where the execution of the tactical's tactics is *) +(* captured inside the box, so that they can be stepped through and/or *) +(* refactored. Thus we cannot take the tactical as a black box; it must *) +(* 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 + infobox_wrap xinfotac;; + +let tactical_wrap x (xttcl:'a->xtactic) (xtac:'a) : xtactic = + tactical_wrap0 (Some x, []) xttcl xtac;; + +let btactical_wrap x (xttcl:'a->'b->xtactic) (xtac1:'a) (xtac2:'b) : xtactic = + tactical_wrap0 (Some 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;; + +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;; + + +(* HILABEL *) + +(* Command for putting the result of a tactic into a box and giving the box a *) +(* label (distinct from a tactical label). *) + +let HILABEL x (xtac:xtactic) : xtactic = + let xinfotac xg = (xtac xg, Label x) in + infobox_wrap xinfotac;; + + +(* xSUBGOAL_THEN - seems to be a special case *) + +let xASSUME = conv_wrap "ASSUME" ASSUME;; + +let xSUBGOAL_THEN (tm:term) (ttac:xthm_tactic) (xg:xgoal) : xgoalstate = + let arg = xASSUME tm in + + let (g,id) = dest_xgoal xg in + let (id0,gtr0) = new_active_subgtree id g in + let xg0 = mk_xgoal (g,id0) in + let (meta,xgs0,just) = ttac arg xg0 in + + 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 (gs0,ids0) = unzip (map dest_xgoal xgs0) in + let xgs = extend_gtree id (Gbox (Tactical finfo, 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); + (meta,xgs,just'));; + + +(* +let SUBGOAL_TAC s tm prfs = + match prfs with + p::ps -> (warn (ps <> []) "SUBGOAL_TAC: additional subproofs ignored"; + SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC]) + | [] -> failwith "SUBGOAL_TAC: no subproof given";; + +let (FREEZE_THEN :thm_tactical) = + fun ttac th (asl,w) -> + let meta,gl,just = ttac (ASSUME(concl th)) (asl,w) in + meta,gl,fun i l -> PROVE_HYP th (just i l);; +*) diff --git a/hol-light/TacticRecording/xthm.ml b/hol-light/TacticRecording/xthm.ml index 210530fa..2619e03f 100644 --- a/hol-light/TacticRecording/xthm.ml +++ b/hol-light/TacticRecording/xthm.ml @@ -19,13 +19,9 @@ and finfo = * farg list;; (* Function's args *) -(* finfo_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";; +type label = + Tactical of finfo + | Label of string;; (* Atomic tests *) @@ -60,127 +56,11 @@ let mk_xthm (xth:thm*finfo) : xthm = xth;; let mk_xthm0 x th = mk_xthm (th, (Some x, []));; -let dest_xthm ((th,x):xthm) : thm * finfo = (th,x);; +let dest_xthm ((th,info):xthm) : thm * finfo = (th,info);; let xthm_thm ((th,_):xthm) = th;; -let xthm_proof ((_,prf):xthm) = prf;; - - - -(* ** WRAPPER FUNCTIONS ** *) - - -(* Theorem wrapper *) - -let theorem_wrap (x:string) (th:thm) : xthm = - (th, (Some x, []));; - - -(* Rule wrappers *) - -(* 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 th' = r arg in - mk_xthm (th',finfo);; - -let conv_wrap x (r:term->thm) (tm:term) : xthm = - rule_wrap0 (Some x, [Fterm tm]) r tm;; - -let thm_conv_wrap x (r:thm->term->thm) (thx:xthm) tm : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;; - -let thmlist_conv_wrap x (r:thm list->term->thm) thxs (tm:term) : xthm = - let (ths,prfs) = unzip (map dest_xthm thxs) in - rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm]) - (r ths) tm;; - -let rule_wrap x (r:thm->thm) (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Fthm prf]) r th;; - -let drule_wrap x (r:thm->thm->thm) (thx1:xthm) (thx2:xthm) : xthm = - let (th1,prf1) = dest_xthm thx1 in - let (th2,prf2) = dest_xthm thx2 in - rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;; - -let prule_wrap x (r:thm*thm->thm) ((thx1:xthm),(thx2:xthm)) : xthm = - let (th1,prf1) = dest_xthm thx1 in - let (th2,prf2) = dest_xthm thx2 in - rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);; - -let trule_wrap x (r:thm->thm->thm->thm) - (thx1:xthm) (thx2:xthm) (thx3:xthm) : xthm = - let (th1,prf1) = dest_xthm thx1 in - let (th2,prf2) = dest_xthm thx2 in - let (th3,prf3) = dest_xthm thx3 in - rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;; - -let term_rule_wrap x (r:term->thm->thm) tm (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;; - -let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;; - -let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,thx0) (thx:xthm) : xthm = - let (th0,prf0) = dest_xthm thx0 in - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;; - -let termlist_rule_wrap x (r:term list->thm->thm) tms (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf]) - (r tms) th;; - -let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, - [Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta); - Fthm prf]) - (r theta) th;; - -let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm) - theta (thx:xthm) : xthm = - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, - [Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta); - Fthm prf]) - (r theta) th;; - -let thmlist_rule_wrap x (r:thm list->thm->thm) thxs (thx:xthm) : xthm = - let (ths,prfs) = unzip (map dest_xthm thxs) in - let (th,prf) = dest_xthm thx in - rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf]) - (r ths) th;; - - -(* Meta rule wrappers *) - -(* This works by ... *) -(* Fails to give a meta argument if it never gets executed. *) - -let meta_rule_wrap0 finfo0 (mr:('a->thm)->'b->thm) - (xr:'a->xthm) (arg:'b) : xthm = - let temp = ref ((Some "???", []) : finfo) in - let r arg0 = let thx = xr arg0 in - let (th,finfo) = dest_xthm thx in - ((match finfo with - (x_, (_::_ as args)) - -> (temp := (x_, front args)) - | _ -> ()); - th) in - let th' = mr r arg in - let (x_,args0) = finfo0 in - let finfo' = (x_, (Ffn !temp)::args0) in - (th',finfo');; - -let conv_conv_wrap x (mc:conv->conv) (c:term->xthm) (tm:term) : xthm = - meta_rule_wrap0 (Some x, [Fterm tm]) mc c tm;; +let xthm_proof ((_,info):xthm) = info;; -- cgit v1.2.3