1(* ========================================================================== *) 2(* FILE : ttt_demoScript.sml *) 3(* DESCRIPTION : TacticToe demo *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2018 *) 6(* ========================================================================== *) 7 8(* --------------------------------------------------------------------------- 9 Requirement: 10 HOL version later than 16 February 2018 11 (Reconfigure (poly --script tools/smart-configure.sml) 12 and rebuild if your previous version was older.) 13 -------------------------------------------------------------------------- *) 14 15open HolKernel boolLib bossLib tacticToe; 16 17val _ = new_theory "ttt_demo"; 18 19(* --------------------------------------------------------------------------- 20 Record ancestries of the current theory. Takes a while. 21 To rebuild tactictoe for a theory, delete the corresponding ttt.sml file. 22 -------------------------------------------------------------------------- *) 23 24val () = ttt_record (); 25 26(* --------------------------------------------------------------------------- 27 Example 1 28 -------------------------------------------------------------------------- *) 29 30val ex1 = store_thm("ex1", 31 ``x > 9 ==> x > 8``, 32 (* Run this tactic first, to generate the one below: 33 ttt ([],``x > 9 ==> x > 8``); *) 34 (ASM_SIMP_TAC (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss)) []); 35 36(* --------------------------------------------------------------------------- 37 Example 2 38 -------------------------------------------------------------------------- *) 39 40val ex2 = store_thm("ex2", 41 ``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``, 42 (* ttt ([],``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``); *) 43 (ASM_SIMP_TAC (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss)) 44 [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_REPLICATE] THEN 45 SRW_TAC [] [listTheory.EL_MAP]); 46 47(* --------------------------------------------------------------------------- 48 Example 3 49 -------------------------------------------------------------------------- *) 50 51val ex3 = store_thm("ex3", 52 ``!n. EVEN n ==> ~(?m. n = 2 * m + 1)``, 53 (* ttt ([],``!n. EVEN n ==> ~(?m. n = 2 * m + 1)``); *) 54 SIMP_TAC bool_ss [GSYM arithmeticTheory.ADD1] THEN 55 PROVE_TAC [arithmeticTheory.EVEN_ODD, arithmeticTheory.ODD_DOUBLE]); 56 57(* --------------------------------------------------------------------------- 58 Example 4 59 -------------------------------------------------------------------------- *) 60 61val ex4 = store_thm("ex4", 62 ``count n SUBSET count (n+m)``, 63 (* ttt ([],``count n SUBSET count (n+m)``); *) 64 ASM_SIMP_TAC numLib.std_ss 65 [pred_setTheory.SUBSET_DEF, 66 pred_setTheory.count_def, 67 pred_setTheory.GSPECIFICATION] THEN 68 METIS_TAC [arithmeticTheory.LESS_IMP_LESS_ADD] 69); 70 71(* --------------------------------------------------------------------------- 72 Example 5 73 -------------------------------------------------------------------------- *) 74 75val ex5 = store_thm("ex5", 76 ``count (n+m) DIFF count n = IMAGE ($+n) (count m)``, 77 (* ttt ([],``count (n+m) DIFF count n = IMAGE ($+n) (count m)``); *) 78 SRW_TAC [ARITH_ss] [pred_setTheory.EXTENSION, EQ_IMP_THM] THEN 79 Q.EXISTS_TAC `x - n` THEN 80 SRW_TAC [ARITH_ss] [] 81); 82 83(* --------------------------------------------------------------------------- 84 Example 6 85 -------------------------------------------------------------------------- *) 86 87val ex6 = store_thm("ex6", 88 ``(MAP f1 ls = MAP f2 ls) /\ MEM x ls ==> (f1 x = f2 x)``, 89 (* ttt ([],``(MAP f1 ls = MAP f2 ls) /\ MEM x ls ==> (f1 x = f2 x)``); *) 90 SRW_TAC [] [listTheory.MAP_EQ_f]); 91 92(* --------------------------------------------------------------------------- 93 Example 7: failure 94 -------------------------------------------------------------------------- *) 95 96(* 97val () = set_timeout 10.0; 98val ex7 = store_thm("ex7", 99 ``countable (UNIV:num list set)`` 100 ttt ([],``countable (UNIV:num list set)``); (* times out *)); 101*) 102 103(* --------------------------------------------------------------------------- 104 Feel free to add your own test examples to contribute to the improvement of 105 TacticToe. 106 -------------------------------------------------------------------------- *) 107 108val _ = export_theory(); 109