1open HolKernel Parse boolLib
2
3val _ = new_theory "marker";
4
5(* ----------------------------------------------------------------------
6    stmarker
7
8    stmarker stands for "short term marker"; use this constant to mark
9    sub-terms for a short period (within a conversion, say) and be sure
10    to remove the marker soon after use.
11   ---------------------------------------------------------------------- *)
12
13val stmarker_def = new_definition("stmarker_def", ``stmarker (x:'a) = x``);
14val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="stmarker"},name=(["Unwanted"],"id")}
15
16(* the following move_<dir>_<op> theorems will loop if more than one term
17   is marked at the same level *)
18val move_left_conj = store_thm(
19  "move_left_conj",
20  ``!p q m. (p /\ stmarker m = stmarker m /\ p) /\
21            ((stmarker m /\ p) /\ q = stmarker m /\ (p /\ q)) /\
22            (p /\ (stmarker m /\ q) = stmarker m /\ (p /\ q))``,
23  REWRITE_TAC [stmarker_def, CONJ_ASSOC] THEN
24  REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
25  MATCH_ACCEPT_TAC CONJ_COMM);
26
27val move_right_conj = store_thm(
28  "move_right_conj",
29  ``!p q m. (stmarker m /\ p = p /\ stmarker m) /\
30            (p /\ (q /\ stmarker m) = (p /\ q) /\ stmarker m) /\
31            ((p /\ stmarker m) /\ q = (p /\ q) /\ stmarker m)``,
32  REWRITE_TAC [stmarker_def, GSYM CONJ_ASSOC] THEN
33  REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
34  MATCH_ACCEPT_TAC CONJ_COMM);
35
36val move_left_disj = store_thm(
37  "move_left_disj",
38  ``!p q m. (p \/ stmarker m = stmarker m \/ p) /\
39            ((stmarker m \/ p) \/ q = stmarker m \/ (p \/ q)) /\
40            (p \/ (stmarker m \/ q) = stmarker m \/ (p \/ q))``,
41  REWRITE_TAC [stmarker_def, DISJ_ASSOC] THEN
42  REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
43  MATCH_ACCEPT_TAC DISJ_COMM);
44
45val move_right_disj = store_thm(
46  "move_right_disj",
47  ``!p q m. (stmarker m \/ p = p \/ stmarker m) /\
48            (p \/ (q \/ stmarker m) = (p \/ q) \/ stmarker m) /\
49            ((p \/ stmarker m) \/ q = (p \/ q) \/ stmarker m)``,
50  REWRITE_TAC [stmarker_def, GSYM DISJ_ASSOC] THEN
51  REPEAT STRIP_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
52  MATCH_ACCEPT_TAC DISJ_COMM);
53
54(* Note, if you want to move a pair of things to the edge of a term,
55   you can move one of them, and then the second in two successive
56   passes.  Something like
57     find_and_move_left THENC RAND_CONV find_and_move_left
58   will result in a term
59     t1 /\ (t2 /\ ...)
60   rewriting with CONJ_ASSOC will even give you
61     (t1 /\ t2) /\ ...
62*)
63
64(* ----------------------------------------------------------------------
65    unint
66
67    unint stands for "uninterpreted", and can be used to mark and/or
68    breakup terms that represent "bad" situations.  One can be sure
69    that unint terms will never be written away, so that they will
70    persist and act as a signal to the user that something has gone wrong.
71
72    Just make sure that unint never appears on the LHS of a rewrite rule.
73    (Idea and name taken from Joe Hurd's development of the positive reals
74    with an infinity.)
75   ---------------------------------------------------------------------- *)
76
77val unint_def = new_definition(
78  "unint_def",
79  ``unint (x:'a) = x``);
80
81(* ----------------------------------------------------------------------
82    Abbrev
83
84    For wrapping up abbreviations in the assumption list.  This tag
85    protects equalities so that they can appear in assumptions and not
86    be eliminated or unduly messed with by other tactics
87   ---------------------------------------------------------------------- *)
88
89val Abbrev_def = new_definition("Abbrev_def", ``Abbrev (x:bool) = x``)
90val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Abbrev"},name=(["Unwanted"],"id")}
91
92
93(* ----------------------------------------------------------------------
94   For telling the simplifier to case-split on if-then-else terms in
95   the goal. Not used as yet.
96   ---------------------------------------------------------------------- *)
97
98val IfCases_def = new_definition("IfCases_def", ``IfCases = T``)
99
100
101(*---------------------------------------------------------------------------*)
102(* Support for the simplifier                                                *)
103(*---------------------------------------------------------------------------*)
104
105val AC_DEF = new_definition("AC_DEF", ``AC b1 b2 = b1 /\ b2``);
106val Cong_def = new_definition("Cong_def", ``Cong (x:bool) = x``);
107val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="AC"},name=(["Data","Bool"],"/\\")}
108val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="bool",Name="/\\"},name=(["Data","Bool"],"/\\")}
109val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Cong"},name=(["Unwanted"],"id")}
110
111
112(*---------------------------------------------------------------------------*)
113(* Support for random user-supplied labels.                                  *)
114(*---------------------------------------------------------------------------*)
115
116val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)),
117                   fixity = Infix(NONASSOC, 80),
118                   paren_style = OnlyIfNecessary,
119                   pp_elements = [HardSpace 1, TOK ":-", BreakSpace(1,0)],
120                   term_name = ":-"};
121
122val _ = Parse.temp_type_abbrev ("label", ``:ind``);
123
124val label_def = new_definition(
125  "label_def",
126  ``((lab:label) :- (argument:bool)) = argument``);
127
128val _ = export_theory();
129