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
92val Abbrev_CONG = store_thm(
93  "Abbrev_CONG",
94  ���r1 = r2 ==> Abbrev(v = r1) = Abbrev (v = r2)���,
95  STRIP_TAC THEN ASM_REWRITE_TAC[]);
96
97
98(* ----------------------------------------------------------------------
99   For telling the simplifier to case-split on if-then-else terms in
100   the goal. Not used as yet.
101   ---------------------------------------------------------------------- *)
102
103val IfCases_def = new_definition("IfCases_def", ``IfCases = T``)
104
105
106(*---------------------------------------------------------------------------*)
107(* Support for the simplifier                                                *)
108(*---------------------------------------------------------------------------*)
109
110val AC_DEF = new_definition("AC_DEF", ``AC b1 b2 <=> b1 /\ b2``);
111val Req0_def = new_definition("Req0_def", ���Req0 = T���);
112val ReqD_def = new_definition("ReqD_def", ���ReqD = T���);
113val Cong_def = new_definition("Cong_def", ``Cong (x:bool) = x``);
114val Exclude_def = new_definition("Exclude_def", ���Exclude (x:'a) = T���);
115val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="AC"},name=(["Data","Bool"],"/\\")}
116val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="bool",Name="/\\"},name=(["Data","Bool"],"/\\")}
117val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="Cong"},name=(["Unwanted"],"id")}
118
119
120(*---------------------------------------------------------------------------*)
121(* Support for random user-supplied labels.                                  *)
122(*---------------------------------------------------------------------------*)
123
124val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)),
125                   fixity = Infix(NONASSOC, 80),
126                   paren_style = OnlyIfNecessary,
127                   pp_elements = [HardSpace 1, TOK ":-", BreakSpace(1,0)],
128                   term_name = ":-"};
129
130Type label[local] = ���:ind���
131
132val label_def = new_definition(
133  "label_def",
134  ``((lab:label) :- (argument:bool)) = argument``);
135
136(* ----------------------------------------------------------------------
137    The 'using' label
138   ---------------------------------------------------------------------- *)
139
140val using_def = new_definition("using_def", ���using (x:label) = T���);
141val usingThm_def = new_definition("usingThm_def", ���usingThm (b:bool) = b���);
142
143val _ = remove_ovl_mapping  "using" {Name = "using", Thy = "marker"}
144val _ = remove_ovl_mapping  "usingThm" {Name = "usingThm", Thy = "marker"}
145
146(*---------------------------------------------------------------------------*)
147(* Case                                                                      *)
148(*                                                                           *)
149(* For marking the current case in case divisions and inductive proofs       *)
150(*---------------------------------------------------------------------------*)
151
152val Case_def = new_definition(
153  "Case_def",
154  ``Case X = T``);
155
156val add_Case = store_thm (
157  "add_Case",
158  ``!X. P <=> (Case X ==> P)``,
159  REWRITE_TAC [Case_def]);
160
161val elim_Case = store_thm (
162  "elim_Case",
163  ``(Case X /\ Y) = Y /\
164    (Y /\ Case X) = Y /\
165    (Case X ==> Y) = Y``,
166  REWRITE_TAC [Case_def]
167  );
168
169val _ = export_theory();
170