/usr/share/hol88-2.02.19940316/ml/ind.ml is in hol88-source 2.02.19940316-28.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 | %=============================================================================%
% HOL 88 Version 2.0 %
% %
% FILE NAME: ind.ml %
% %
% DESCRIPTION: General induction tactic for recursive types. %
% %
% AUTHOR: T. F. Melham (87.08.23) %
% %
% University of Cambridge %
% Hardware Verification Group %
% Computer Laboratory %
% New Museums Site %
% Pembroke Street %
% Cambridge CB2 3QG %
% England %
% %
% COPYRIGHT: T. F. Melham 1987 1990 %
% %
% REVISION HISTORY: 90.06.02 %
%=============================================================================%
begin_section INDUCT_THEN;;
% --------------------------------------------------------------------- %
% Internal function: %
% %
% BETAS "f" tm : returns a conversion that, when applied to a term with %
% the same structure as the input term tm, will do a %
% beta reduction at all top-level subterms of tm which %
% are of the form "f <arg>", for some argument <arg>. %
% %
% --------------------------------------------------------------------- %
letrec BETAS fn body =
if ((is_var body) or (is_const body)) then REFL else
if (is_abs body) then ABS_CONV (BETAS fn (snd(dest_abs body))) else
let (rt,ra) = dest_comb body in
if (rt = fn) then BETA_CONV else
let cnv1 = (BETAS fn rt) and cnv2 = (BETAS fn ra) in
(MK_COMB o ((cnv1 # cnv2) o dest_comb));;
% --------------------------------------------------------------------- %
% Internal function: GTAC %
% %
% !x. tm[x] %
% ------------ GTAC "y" (primes the "y" if necessary). %
% tm[y] %
% %
% NB: the x is always a genvar, so optimized for this case. %
% --------------------------------------------------------------------- %
let GTAC y (A,g) =
let x,body = dest_forall g and y' = (variant (freesl (g.A)) y) in
[(A,subst[y',x]body)],\[th]. GEN x (INST [(x,y')] th);;
% --------------------------------------------------------------------- %
% Internal function: TACF %
% %
% TACF is used to generate the subgoals for each case in an inductive %
% proof. The argument tm is formula which states one generalized %
% case in the induction. For example, the induction theorem for num is: %
% %
% |- !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n %
% %
% In this case, the argument tm will be one of: %
% %
% 1: "P 0" or 2: !n. P n ==> P(SUC n) %
% %
% TACF applied to each these terms to construct a parameterized tactic %
% which will be used to further break these terms into subgoals. The %
% resulting tactic takes a variable name x and a user supplied theorem %
% continuation ttac. For a base case, like case 1 above, the resulting %
% tactic just throws these parameters away and passes the goal on %
% unchanged (i.e. \x ttac. ALL_TAC). For a step case, like case 2, the %
% tactic applies GTAC x as many times as required. It then strips off %
% the induction hypotheses and applies ttac to each one. For example, %
% if tac is the tactic generated by: %
% %
% TACF "!n. P n ==> P(SUC n)" "x:num" ASSUME_TAC %
% %
% then applying tac to the goal A,"!n. P[n] ==> P[SUC n] has the same %
% effect as applying: %
% %
% GTAC "x:num" THEN DISCH_THEN ASSUME_TAC %
% %
% TACF is a strictly local function, used only to define TACS, below. %
% --------------------------------------------------------------------- %
let TACF =
letrec ctacs tm =
if (is_conj tm) then
let tac2 = ctacs (snd(dest_conj tm)) in
\ttac. CONJUNCTS_THEN2 ttac (tac2 ttac) else
\ttac.ttac in
\tm. let vs,body = strip_forall tm in
if (is_imp body) then
let TTAC = ctacs (fst(dest_imp body)) in
\x ttac. MAP_EVERY (GTAC o (K x)) vs THEN
DISCH_THEN (TTAC ttac) else
\x ttac. ALL_TAC;;
% --------------------------------------------------------------------- %
% Internal function: TACS %
% %
% TACS uses TACF to generate a paramterized list of tactics, one for %
% each conjunct in the hypothesis of an induction theorem. %
% %
% For example, if tm is the hypothesis of the induction thoerem for the %
% natural numbers---i.e. if: %
% %
% tm = "P 0 /\ (!n. P n ==> P(SUC n))" %
% %
% then TACS tm yields the paremterized list of tactics: %
% %
% \x ttac. [TACF "P 0" x ttac; TACF "!n. P n ==> P(SUC n)" x ttac] %
% %
% TACS is a strictly local function, used only in INDUCT_THEN. %
% --------------------------------------------------------------------- %
letrec TACS tm =
let cf,csf = ((TACF # TACS) (dest_conj tm) ? TACF tm,K(K[])) in
\x ttac. (cf x ttac) . (csf x ttac);;
% --------------------------------------------------------------------- %
% Internal function: GOALS %
% %
% GOALS generates the subgoals (and proof functions) for all the cases %
% in an induction. The argument A is the common assumption list for all %
% the goals, and tacs is a list of tactics used to generate subgoals %
% from these goals. %
% %
% GOALS is a strictly local function, used only in INDUCT_THEN. %
% --------------------------------------------------------------------- %
letrec GOALS A tacs tm =
if (null (tl tacs)) then
let sg,pf = (hd tacs) (A,tm) in [sg],[pf] else
let c,cs = dest_conj tm in
let sgs,pfs = GOALS A (tl tacs) cs in
let sg,pf = (hd tacs (A,c)) in
sg.sgs,pf.pfs;;
% --------------------------------------------------------------------- %
% Internal function: GALPH %
% %
% GALPH "!x1 ... xn. A ==> B": alpha-converts the x's to genvars. %
% --------------------------------------------------------------------- %
let GALPH =
let rule v =
let gv = genvar(type_of v) in
\eq. let th = FORALL_EQ v eq in
TRANS th (GEN_ALPHA_CONV gv (rhs(concl th))) in
\tm. let vs,hy = strip_forall tm in
if (is_imp hy) then itlist rule vs (REFL hy) else REFL tm;;
% --------------------------------------------------------------------- %
% Internal function: GALPHA %
% %
% Applies the conversion GALPH to each conjunct in a sequence. %
% --------------------------------------------------------------------- %
letrec GALPHA tm =
(let c,cs = (GALPH # GALPHA) (dest_conj tm) in
MK_COMB((AP_TERM "$/\" c),cs)) ? GALPH tm;;
% --------------------------------------------------------------------- %
% Internal function: mapshape %
% %
% Applies the functions in fl to argument lists obtained by splitting %
% the list l into sublists of lengths given by nl. %
% --------------------------------------------------------------------- %
letrec mapshape nl fl l =
if null nl then [] else
(let m,l = chop_list (hd nl) l in
(hd fl)m . mapshape(tl nl)(tl fl)l) ;;
% --------------------------------------------------------------------- %
% INDUCT_THEN : general induction tactic for concrete recursive types. %
% --------------------------------------------------------------------- %
let INDUCT_THEN th : (thm_tactic -> tactic) =
(let P,hy,_ = (I # dest_imp) (dest_forall (concl th)) in
let bconv = BETAS P hy and tacsf = TACS hy in
let v = genvar (type_of P) and bv = genvar ":bool" in
let eta_th = CONV_RULE(RAND_CONV ETA_CONV) (UNDISCH(SPEC v th)) in
let [asm],con = dest_thm eta_th in
let dis = ((DISCH asm) eta_th) in
let ind = GEN v (SUBST [GALPHA asm,bv] (mk_imp(bv,con)) dis) in
(\ttac.\(A,t).
(let lam = snd(dest_comb t) in
let spec = SPEC lam (INST_TYPE (snd(match v lam)) ind) in
let an,sp = dest_imp(concl spec) in
let beta = SUBST [bconv an,bv] (mk_imp(bv,sp)) spec in
let tacs = tacsf (fst(dest_abs lam)) ttac in
let gll,pl = GOALS A tacs (fst(dest_imp(concl beta))) in
let pf = ((MP beta) o LIST_CONJ) o mapshape(map length gll)pl in
(flat gll, pf)) ? failwith `INDUCT_THEN`)) ?
failwith `INDUCT_THEN: ill-formed induction theorem`;;
% Bind INDUCT_THEN to "it", so as to export it outside the section. %
INDUCT_THEN;;
end_section INDUCT_THEN;;
% Save the exported value. %
let INDUCT_THEN = it;;
|