1(*---------------------------------------------------------------------------
2   Implementation of NOTES. A note is usually just a renaming of either
3   the I or K combinators. An example of an I-instance is something 
4   like NUMERAL. Other parts of the system are hardwired to know how to 
5   treat occurrences of NUMERAL, e.g., the parser and prettyprinter 
6   treat its argument as a number. In the following, we are going to
7   add a facility for naming assumptions in goals via a new logical 
8   constant NAMED, which is an instance of the K combinator. This allows
9   it to be semantically transparent.
10 ---------------------------------------------------------------------------*)
11
12infixr OR ;
13fun (P OR Q) x = P x orelse Q x;
14
15val _ = new_theory "named"
16
17val NAMED_ERR = mk_HOL_ERR "NAMED";
18 
19val NAMED_DEF = new_definition("NAMED", Term `NAMED x y = x`);
20
21(*---------------------------------------------------------------------------*)
22(* Not interpreted in the object language, but in the meta-language          *)
23(*---------------------------------------------------------------------------*)
24
25val named_tm = prim_mk_const{Name="NAMED", Thy="named"};
26
27fun mk_named (n,tm) =
28  let val v = mk_var(n,alpha)
29      val named = inst [alpha |-> type_of tm, beta |-> alpha] named_tm
30  in list_mk_comb(named,[tm,v])
31  end;
32
33datatype 'a named = NOT of term | NAMED of 'a * term;
34
35(*---------------------------------------------------------------------------
36    Try to take a term P of the form `NAMED M n` apart, returning 
37    the ML value NAMED(n,M). If that's not possible, return NOT P.
38 ---------------------------------------------------------------------------*)
39
40fun dest_named tm = 
41  case strip_comb tm
42   of (c,[x,y]) => 
43       if same_const c named_tm
44         then (case total dest_var y
45                of SOME (n,_) => NAMED(n,x)
46                 | otherwise => raise NAMED_ERR "dest_named"
47                        (String.concat ["expected ", 
48                                        Lib.quote "NAMED <term> <var>"]))
49         else NOT tm
50   | otherwise => NOT tm;
51
52fun is_named tm = 
53 (case dest_named tm 
54   of NOT _ => false
55    | NAMED _ => true) handle HOL_ERR _ => false;
56
57(*---------------------------------------------------------------------------
58    Lookup a term by name in a list of terms. If looking for
59    a term named "foo", and a term `NAMED <term> foo` is found
60    in the list, then 
61
62       SOME (`NAMED <term> foo`, ("foo",M))
63
64    is returned.
65 ---------------------------------------------------------------------------*)
66
67fun name_assoc s [] = NONE
68  | name_assoc s (tm::rst) = 
69     case dest_named tm 
70      of NOT _ => name_assoc s rst
71       | NAMED(n,tm') => if s=n then SOME(tm,(n,tm'))
72                                else name_assoc s rst;
73
74(*---------------------------------------------------------------------------
75    Lookup a term M in a list of terms. If M is an element of the
76    list, it is returned. If a term P = `NAMED M <name>` is an element
77    of the list (for some <name>), P is returned.
78 ---------------------------------------------------------------------------*)
79
80fun term_assoc M [] = NONE
81  | term_assoc M (N::rst) = 
82     case dest_named N 
83      of NOT _ => if aconv M N then SOME N else term_assoc M rst
84       | NAMED(_,tm') => if aconv M tm' then SOME N else term_assoc M rst;
85
86
87(*---------------------------------------------------------------------------
88    Attach and detach names and terms. Could make naming be idempotent.
89 ---------------------------------------------------------------------------*)
90
91fun NAME_CONV name tm = SYM (ISPECL [tm, mk_var(name,alpha)] NAMED_DEF)
92val UN_NAME_CONV = REWR_CONV (SPEC_ALL NAMED_DEF);
93
94val NAME = CONV_RULE o NAME_CONV;
95val UN_NAME = CONV_RULE UN_NAME_CONV;
96
97
98(*---------------------------------------------------------------------------
99      Some proof routines that can deal with named hypotheses. 
100 ---------------------------------------------------------------------------*)
101
102val ASSUME_NAMED = ASSUME o mk_named;
103
104(*===========================================================================
105    Fetch an assumption and stick a name on it before putting it back
106    in the assumptions. It will not in general be put back in the 
107    same spot, although it could be (with a little extra work). We 
108    also do not check that a name does not already occur free in the goal.
109 ===========================================================================*)
110
111fun NAME_ASSUM (s,tm) th =
112  if mem tm (hyp th)
113  then UNDISCH (CONV_RULE (LAND_CONV (NAME_CONV s)) (DISCH tm th))
114  else raise NAMED_ERR "NAME_ASSUM" "term is not in the assumptions";
115
116
117fun gen_name H0 vlist thm = 
118 let val (A,c) = dest_thm thm
119     val v = with_flag (Globals.priming,SOME "")
120                       (variant (free_varsl (H0::c::A) @ vlist))
121                        H0
122 in  fst(dest_var v)
123 end;
124     
125fun X_NAME_ASSUM H0 tm th =
126  NAME_ASSUM (gen_name H0 (free_vars tm) th,tm) th
127
128val NAME_ASSUM_AUTO = X_NAME_ASSUM (mk_var("H",alpha));
129
130fun ADD_ASSUM_NAMED th (s,tm) =
131  MP (DISCH (mk_named (s,tm)) th) 
132     (ASSUME_NAMED (s,tm));
133   
134(*===========================================================================
135       Discharge a term, and remove the name, if it has one. 
136 ===========================================================================*)
137
138local fun DISCH_TERM tm thm = 
139       CONV_RULE (TRY_CONV (LAND_CONV UN_NAME_CONV))
140                 (DISCH tm thm)
141in
142(*===========================================================================
143     Look up an assumption by name and discharge it.
144 ===========================================================================*)
145
146fun DISCH_NAMED name thm =
147  case name_assoc name (hyp thm)
148   of SOME (tm,_) => DISCH_TERM tm thm
149    | NONE => raise NAMED_ERR "DISCH_NAMED" 
150                 ("Couldn't find hypothesis named "^Lib.quote name);
151
152fun DISCHARGE tm thm =
153 DISCH_TERM 
154   (case term_assoc tm (hyp thm) of NONE => tm | SOME tm' => tm')
155    thm
156end (* local *);
157
158(*---------------------------------------------------------------------------
159    Use the conclusion of the first theorem to delete a named hypothesis 
160    of  the second theorem.
161 
162       A |- t1   B, NAMED t1 H |- t2
163       ------------------------------
164            A u B |- t2
165 ---------------------------------------------------------------------------*)
166
167fun PROVE_HYP_NAMED ath bth = MP (DISCHARGE (concl ath) bth) ath;
168
169(*****************************************************************************)
170(*   TACTICS                                                                 *)
171(*****************************************************************************)
172
173(*===========================================================================
174           A ?- M
175    -----------------------   ASSUME_NAMED_TAC (s, B|-N)
176    A, NAMED N s ?- M
177 ===========================================================================*)
178
179fun ASSUME_NAMED_TAC s bth : tactic = 
180 fn (asl,w) =>
181   ([(mk_named (s,concl bth)::asl,w)], 
182    (fn [th] => PROVE_HYP_NAMED bth th));
183
184val DISCH_NAMED_TAC = DISCH_THEN o ASSUME_NAMED_TAC;
185
186fun ASSUME_NAMED_AUTO_TAC th =
187  ASSUME_NAMED_TAC (gen_name (mk_var("H",alpha)) [] th) th;
188
189fun ASSUME_NAMED_AUTO_REF_TAC r th = 
190  let val list = !r
191      val name = gen_name (mk_var("H",alpha)) list th
192      val () = r := mk_var(name,alpha)::list
193  in ASSUME_NAMED_TAC name th
194  end;
195
196(* fun NAME_ASSUM_TAC P (g as (asl,w)) =
197 case filter P asl
198  of [x] => UNDISCH_THEN x ASSUME_NAMED_TAC 
199   | other => raise ERR "NAME_ASSUM_TAC" "predicate not satisfied"
200*)
201
202(*---------------------------------------------------------------------------
203    A version of UNDISCH_THEN that uses names to index hypotheses
204 ---------------------------------------------------------------------------*)
205
206fun WITH_ASSUM s ttac : tactic = 
207 fn (asl,w) =>
208   case name_assoc s asl
209    of NONE => raise NAMED_ERR "NAMED_THEN" 
210                ("Can't find term named by "^Lib.quote s^" in assumptions")
211     | SOME(named_tm,(_,core)) 
212         => ttac (UN_NAME(ASSUME_NAMED (s,core)))
213                 (op_set_diff aconv asl [named_tm],w);
214
215(*---------------------------------------------------------------------------
216        STRIP_NAMED_TAC: strip a goal, attaching names to each new 
217        element added to the hypotheses
218 ---------------------------------------------------------------------------*)
219
220fun STRIP_NAMED_TAC (g as (asl,w)) = 
221 let val vars = ref (free_varsl(w::asl))
222     fun CHECK_ASSUME_NAMED_TAC th =
223        FIRST [CONTR_TAC th, 
224               ACCEPT_TAC th, 
225               DISCARD_TAC th, 
226               ASSUME_NAMED_AUTO_REF_TAC vars th]
227     val STRIP_ASSUME_NAMED_TAC = 
228         REPEAT_TCL STRIP_THM_THEN CHECK_ASSUME_NAMED_TAC
229 in
230   STRIP_GOAL_THEN STRIP_ASSUME_NAMED_TAC g
231 end;
232
233fun RULE_ASSUM_NAMED_TAC f = 
234  let fun wrap f th = 
235       (case dest_named (concl th)
236         of NOT _ => f th
237          | NAMED(n,_) => NAME n (f (UN_NAME th))) 
238       handle e as HOL_ERR _ => raise (wrap_exn "RULE_ASSUM_NAMED_TAC" "" e)
239  in RULE_ASSUM_TAC (wrap f)
240  end;
241
242
243fun NAMED_ASSUM_TAC s f = WITH_ASSUM s (ASSUME_NAMED_TAC s o f);
244
245(*---------------------------------------------------------------------------
246      Robust POP_ASSUM
247 ---------------------------------------------------------------------------*)
248
249fun POP_ASSUM_NAMED ttac = 
250  POP_ASSUM (ttac o CONV_RULE (TRY_CONV UN_NAME_CONV));
251
252
253to do: STRIP_ASSUME_TAC
254       ASSUM_LIST
255       PROVE_TAC 
256       WEAKEN_TAC
257       SIMP_TAC
258Some of these are for backwards compatibility, and others provide
259new functionality. For PROVE_TAC and SIMP_TAC, we can use WEAKEN_TAC
260to get rid of any non-named hypotheses.
261
262idea: dualization, so that all non-named hypotheses get named, and 
263all named hypotheses have their names removed.
264
265idea: NAME_ASSUMS_TAC, UN_NAME_ASSUMS_TAC
266
267
268idea: MATCH_STRIP_TAC takes a goal 
269
270           A ?- M ==> N
271
272and a pattern M' and matches M to M'. The resulting instantiations will
273get turned into named assumptions.
274
275   MATCH_STRIP_TAC 
276
277(*---------------------------------------------------------------------------*)
278(*  Example
279  open arithmeticTheory;
280
281 val EXP_2 = Q.prove
282(`!n:num. n**2 = n*n`,
283 RW_TAC arith_ss [EXP,MULT_CLAUSES,TWO,ONE]);
284
285val EXP2_LEM = Q.prove
286(`!x y:num. ((2*x)**2 = 2*(y**2)) = (2*(x**2) = y**2)`,
287 RW_TAC arith_ss [EXP_2,TWO,GSYM MULT_ASSOC] 
288 THEN PROVE_TAC [MULT_ASSOC,MULT_SYM]);
289
290val lemma = Q.prove
291(`!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`,
292 completeInduct_on `m` THEN NTAC 2 STRIP_TAC THEN
293  `?k. m = 2*k` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS] 
294                THEN VAR_EQ_TAC THEN
295  `?p. n = 2*p` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS,EXP2_LEM] 
296                THEN VAR_EQ_TAC THEN
297  `k**2 = 2*(p**2)` by PROVE_TAC [EXP2_LEM] THEN
298  `(k=0) \/ k < 2*k` by numLib.ARITH_TAC
299 THENL [FULL_SIMP_TAC arith_ss [EXP_2],
300        PROVE_TAC [MULT_EQ_0, DECIDE (Term `~(2 = 0n)`)]]);
301
302g `!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`;
303e (completeInduct_on `m`);
304
305
306*)
307(*---------------------------------------------------------------------------*)
308