(******************************************************************************) (* FILE : struct_equal.ml *) (* DESCRIPTION : Proof procedure for simplifying an equation between two *) (* data-structures of the same type. *) (* *) (* READS FILES : <none> *) (* WRITES FILES : <none> *) (* *) (* AUTHOR : R.J.Boulton & T.F.Melham *) (* DATE : 4th June 1992 *) (* *) (* LAST MODIFIED : R.J.Boulton *) (* DATE : 14th October 1992 *) (* *) (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *) (* DATE : 2008 *) (******************************************************************************) let subst_occs = let rec subst_occs slist tm = let applic,noway = partition (fun (i,(t,x)) -> aconv tm x) slist in let sposs = map (fun (l,z) -> let l1,l2 = partition ((=) 1) l in (l1,z),(l2,z)) applic in let racts,rrest = unzip sposs in let acts = filter (fun t -> not (fst t = [])) racts in let trest = map (fun (n,t) -> (map (C (-) 1) n,t)) rrest in let urest = filter (fun t -> not (fst t = [])) trest in let tlist = urest @ noway in if acts = [] then if is_comb tm then let l,r = dest_comb tm in let l',s' = subst_occs tlist l in let r',s'' = subst_occs s' r in mk_comb(l',r'),s'' else if is_abs tm then let bv,bod = dest_abs tm in let gv = genvar(type_of bv) in let nbod = vsubst[gv,bv] bod in let tm',s' = subst_occs tlist nbod in alpha bv (mk_abs(gv,tm')),s' else tm,tlist else let tm' = (fun (n,(t,x)) -> subst[t,x] tm) (hd acts) in tm',tlist in fun ilist slist tm -> fst(subst_occs (zip ilist slist) tm);; let GSUBS substfn ths th = let ls = map (lhs o concl) ths in let vars = map (genvar o type_of) ls in let w = substfn (List.combine ls vars) (concl th) in SUBST (List.combine ths vars) w th ;; let SUBS_OCCS nlths th = try (let (nll, ths) = unzip nlths in GSUBS (subst_occs nll) ths th ) with Failure _ -> failwith "SUBS_OCCS";; (*----------------------------------------------------------------------------*) (* VAR_NOT_EQ_STRUCT_OF_VAR_CONV : (thm # thm list # thm list) -> conv *) (* *) (* Proof method developed through discussion between *) (* R. Boulton, T. Melham and A. Pitts. *) (* *) (* This conversion can be used to prove that a variable is not equal to a *) (* structure containing that variable as a proper subterm. The structures are *) (* restricted to applications of constructors from a single recursive type. *) (* The leaf nodes must be either variables or 0-ary constructors of the type. *) (* *) (* The theorems taken as arguments are the induction, distinctness and *) (* injectivity theorems for the recursive type, as proved by the functions: *) (* *) (* prove_induction_thm *) (* prove_constructors_distinct *) (* prove_constructors_one_one *) (* *) (* Since the latter two functions may fail, the distinctness and injectivity *) (* theorems are passed around as lists of conjuncts, so that a failure *) (* results in an empty list. *) (* *) (* Examples of input terms: *) (* *) (* ~(l = CONS h l) *) (* ~(CONS h1 (CONS h2 l) = l) *) (* ~(n = SUC(SUC(SUC n))) *) (* ~(t = TWO (ONE u) (THREE v (ONE t) (TWO u (ONE t)))) *) (* *) (* where the last example is for the type defined by: *) (* *) (* test = ZERO | ONE test | TWO test test | THREE test test test *) (* *) (* The procedure works by first generalising the structure to eliminate any *) (* irrelevant substructures. If the variable occurs more than once in the *) (* structure the more deeply nested occurrences are replaced by new variables *) (* because multiple occurrences of the variable prevent the induction from *) (* working. The generalised term for the last example is: *) (* *) (* TWO a (THREE v (ONE t) b) *) (* *) (* The procedure then forms a conjunction of the inequalities for this term *) (* and all of its `rotations': *) (* *) (* !t. (!a v b. ~(t = TWO a (THREE v (ONE t) b))) /\ *) (* (!a v b. ~(t = THREE v (ONE (TWO a t)) b)) /\ *) (* (!a v b. ~(t = ONE (TWO a (THREE v t b)))) *) (* *) (* This can be proved by a straightforward structural induction. The reason *) (* for including the rotations is that the induction hypothesis required for *) (* the proof of the original generalised term is the rotation of it. *) (* *) (* The procedure could be optimised by detecting duplicated rotations. For *) (* example it is not necessary to prove: *) (* *) (* !n. ~(n = SUC(SUC(SUC n))) /\ *) (* ~(n = SUC(SUC(SUC n))) /\ *) (* ~(n = SUC(SUC(SUC n))) *) (* *) (* in order to prove "~(n = SUC(SUC(SUC n)))" because the structure is its *) (* own rotations. It is sufficient to prove: *) (* *) (* !n. ~(n = SUC(SUC(SUC n))) *) (* *) (* The procedure currently uses backwards proof. It would probably be more *) (* efficient to use forwards proof. *) (*----------------------------------------------------------------------------*) let VAR_NOT_EQ_STRUCT_OF_VAR_CONV = try( let number_list l = let rec number_list' n l = if (l = []) then [] else (hd l,n)::(number_list' (n + 1) (tl l)) in number_list' 1 l in let name = fst o dest_const in let occurrences constrs v st = let rec occurrences' v st path = if (not (type_of st = type_of v)) then [] else if (st = v) then [rev path] else if (is_var st) then [] else let (f,args) = (check ( ((can (C assoc constrs)) o name o fst) )) (strip_comb st) (* Boulton was using hashI here... but I don't know why *) in flat (map (fun (arg,n) -> occurrences' v arg (n::path)) (number_list args)) in occurrences' v st [] in let min_length l = let rec min_length' (x,n) l = if (l = []) then x else if (length (hd l) < n) then min_length' (hd l,length (hd l)) (tl l) else min_length' (x,n) (tl l) in if (l = []) then failwith "min_length" else min_length' (hd l,length (hd l)) (tl l) in let rec generalise (st,occ) = let rec replace_side_structs (n,argn',binding) m args = if (args = []) then ([],[]) else let m' = m + 1 and arg = hd args in let (rest,bind) = replace_side_structs (n,argn',binding) m' (tl args) in if (m' = n) then ((argn'::rest),(binding @ bind)) else if (is_var arg) then ((arg::rest),((arg,arg)::bind)) else let var = genvar (type_of arg) in ((var::rest),((var,arg)::bind)) in if (occ = []) then (st,[]) else let (f,args) = strip_comb st and (n::occ') = occ in let (argn',binding) = generalise (el (n-1) args,occ') in let (args',bind) = replace_side_structs (n,argn',binding) 0 args in (list_mk_comb (f,args'),bind) in let rec constr_apps v (st,occ) = let rec replace_argn (n,argn') m args = if (args = []) then [] else let m' = m + 1 in if (m' = n) then argn'::(tl args) else (hd args)::(replace_argn (n,argn') m' (tl args)) in if (occ = []) then [] else let (f,args) = strip_comb st and (n::occ') = occ in let args' = replace_argn (n,v) 0 args in (list_mk_comb (f,args'))::(constr_apps v (el (n-1) args,occ')) in let rotations l = let rec rotations' l n = if (n < 1) then [] else l::(rotations' ((tl l) @ [hd l]) (n - 1)) in rotations' l (length l) in let two_constrs = (hash (fst o strip_comb) (fst o strip_comb)) o dest_eq o dest_neg o snd o strip_forall o concl in let flip (x,y) = (y,x) in let DEPTH_SYM = GEN_ALL o NOT_EQ_SYM o SPEC_ALL in let rec arg_types ty = try (match (dest_type ty) with | ("fun",[argty;rest]) -> argty::(arg_types rest) | _ -> []) with Failure _ -> [] in let name_and_args = ((hash I) arg_types) o dest_const in fun (induction,distincts,oneOnes) -> let half_distincts = map (fun th -> ((hash name) name) (two_constrs th), th) distincts in let distincts = half_distincts @ (map ((hash flip) DEPTH_SYM) half_distincts) in let ind_goals = (conjuncts o fst o dest_imp o snd o dest_forall o concl) induction in let constrs = map (name_and_args o fst o strip_comb o rand o snd o strip_forall o snd o (splitlist dest_imp) o snd o strip_forall) ind_goals in fun tm -> (let (l,r) = dest_eq (dest_neg tm) in let (flipped,v,st) = if (is_var l) then if (is_var r) then failwith "" else (false,l,r) else if (is_var r) then (true,r,l) else failwith "" in let occ = min_length (occurrences constrs v st) in let (st',bind) = generalise (st,occ) in let (vars,subterms) = List.split bind in let apps = constr_apps v (st',occ) in let rotats = map (end_itlist (fun t1 t2 -> subst [(t2,v)] t1)) (rotations apps) in let uneqs = map (mk_neg o (curry mk_eq v)) rotats in let conj = mk_forall (v,list_mk_conj (map (curry list_mk_forall vars) uneqs)) in; (*----------------------------------------------------------------------------*) (* CONJS_CONV : conv -> conv *) (* *) (* Written by T.F.Melham. *) (* Modified by R.J.Boulton. *) (* *) (* Apply a given conversion to a sequence of conjuncts. *) (* *) (* * need to check T case *) (* * need to flatten conjuncts on RHS *) (*----------------------------------------------------------------------------*) let CONJS_CONV = try( let is st th = try(fst(dest_const(rand(concl th))) = st) with Failure _ -> false in let v1 = genvar `:bool` and v2 = genvar `:bool` in let fthm1 = let th1 = ASSUME (mk_eq(v1,`F`)) in let cnj = mk_conj(v1,v2) in let th1 = DISCH cnj (EQ_MP th1 (CONJUNCT1 (ASSUME cnj))) in let th2 = DISCH `F` (CONTR cnj (ASSUME `F`)) in DISCH (mk_eq(v1,`F`)) (IMP_ANTISYM_RULE th1 th2) in let fthm2 = CONV_RULE(ONCE_DEPTH_CONV(REWR_CONV CONJ_SYM)) fthm1 in let fandr th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] fthm1) th in let fandl th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] fthm2) th in let tthm1 = let th1 = ASSUME (mk_eq(v1,`T`)) in let th2 = SUBS_OCCS [[2],th1] (REFL (mk_conj(v1,v2))) in DISCH (mk_eq(v1,`T`)) (ONCE_REWRITE_RULE [] th2) in let tthm2 = CONV_RULE(ONCE_DEPTH_CONV(REWR_CONV CONJ_SYM)) tthm1 in let tandr th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] tthm1) th in let tandl th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] tthm2) th in let rec cconv conv tm = (let (c,cs) = dest_conj tm in let cth = conv c in if (is "F" cth) then fandr cth cs else let csth = cconv conv cs in if (is "F" csth) then fandl csth c else if (is "T" cth) then TRANS (tandr cth cs) csth else if (is "T" csth) then TRANS (tandl csth c) cth else try (MK_COMB((AP_TERM `(/\)` cth),csth)) with Failure _ -> conv tm ) in fun conv tm -> cconv conv tm) with Failure _ -> failwith "CONJS_CONV";; (*----------------------------------------------------------------------------*) (* ONE_STEP_RECTY_EQ_CONV : (thm # thm list # thm list) -> conv -> conv *) (* *) (* Single step conversion for equality between structures of a single *) (* recursive type. *) (* *) (* Based on code written by T.F.Melham. *) (* *) (* The theorems taken as arguments are the induction, distinctness and *) (* injectivity theorems for the recursive type, as proved by the functions: *) (* *) (* prove_induction_thm *) (* prove_constructors_distinct *) (* prove_constructors_one_one *) (* *) (* Since the latter two functions may fail, the distinctness and injectivity *) (* theorems are passed around as lists of conjuncts. *) (* *) (* If one side of the equation is a variable and that variable appears in the *) (* other side (nested in a structure) the equation is proved false. *) (* *) (* If the top-level constructors on the two sides of the equation are *) (* distinct the equation is proved false. *) (* *) (* If the top-level constructors on the two sides of the equation are the *) (* same a conjunction of equations is generated, one equation for each *) (* argument of the constructor. The conversion given as argument is then *) (* applied to each conjunct. If any of the applications of this conversion *) (* fail, so will the entire call. *) (* *) (* In other conditions the function fails. *) (*----------------------------------------------------------------------------*) (* Taken from HOL90 *) let ONE_STEP_RECTY_EQ_CONV (induction,distincts,oneOnes) = let NOT_EQ_CONV = EQF_INTRO o EQT_ELIM o (VAR_NOT_EQ_STRUCT_OF_VAR_CONV (induction,distincts,oneOnes)) o mk_neg in let INJ_REW = GEN_REWRITE_CONV I oneOnes (* Deleted empty_rewrites - GEN_REWRITE_CONV different in hol light - hope it works *) in let ths1 = map SPEC_ALL distincts in let ths2 = map (GEN_ALL o EQF_INTRO o NOT_EQ_SYM) ths1 in let dths = ths2 @ (map (GEN_ALL o EQF_INTRO) ths1) in let DIST_REW = GEN_REWRITE_CONV I dths in fun conv -> NOT_EQ_CONV ORELSEC DIST_REW ORELSEC (INJ_REW THENC (CONJS_CONV conv)) ORELSEC (fun tm -> failwith "ONE_STEP_RECTY_EQ_CONV") (*----------------------------------------------------------------------------*) (* RECTY_EQ_CONV : (thm # thm list # thm list) -> conv *) (* *) (* Function to simplify as far as possible an equation between two structures *) (* of some type, the type being specified by the triple of theorems. The *) (* structures may involve variables. The result may be a conjunction of *) (* equations simpler than the original. *) (*----------------------------------------------------------------------------*) let RECTY_EQ_CONV (induction,distincts,oneOnes) = try ( let one_step_conv = ONE_STEP_RECTY_EQ_CONV (induction,distincts,oneOnes) and REFL_CONV tm = let (l,r) = dest_eq tm in if (l = r) then EQT_INTRO (REFL l) else failwith "REFL_CONV" in let rec conv tm = (one_step_conv conv ORELSEC REFL_CONV ORELSEC ALL_CONV) tm in fun tm -> conv tm ) with Failure _ -> failwith "RECTY_EQ_CONV";;let th1 = prove (conj,INDUCT_TAC_ induction THEN ASM_REWRITE_TAC (oneOnes @ (map snd distincts))) in let th2 = (hd o CONJUNCTS o (SPEC v)) th1 in let th3 = SPECL subterms th2 in let th4 = if flipped then (NOT_EQ_SYM th3) else th3 in EQT_INTRO (CONV_RULE (C ALPHA tm) th4) )) with Failure _ -> failwith "VAR_NOT_EQ_STRUCT_OF_VAR_CONV";