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