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