(******************************************************************************) (* FILE : equalities.ml *) (* DESCRIPTION : Using equalities. *) (* *) (* READS FILES : *) (* WRITES FILES : *) (* *) (* AUTHOR : R.J.Boulton *) (* DATE : 19th June 1991 *) (* *) (* LAST MODIFIED : R.J.Boulton *) (* DATE : 7th August 1992 *) (* *) (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *) (* DATE : 2008 *) (******************************************************************************) (*----------------------------------------------------------------------------*) (* is_explicit_value_template : term -> bool *) (* *) (* Function to compute whether a term is an explicit value template. *) (* An explicit value template is a non-variable term composed entirely of *) (* T or F or variables or applications of shell constructors. *) (* A `bottom object' corresponds to an application to no arguments. I have *) (* also made numeric constants valid components of explicit value templates, *) (* since they are equivalent to some number of applications of SUC to 0. *) (*----------------------------------------------------------------------------*) let is_explicit_value_template tm = let rec is_explicit_value_template' constructors tm = (is_T tm) or (is_F tm) or ((is_const tm) & (type_of tm = `:num`)) or (is_var tm) or (is_numeral tm) or (let (f,args) = strip_comb tm in (try(mem (fst (dest_const f)) constructors) with Failure _ -> false) & (forall (is_explicit_value_template' constructors) args)) in (not (is_var tm)) & (is_explicit_value_template' (all_constructors ()) tm);; (*----------------------------------------------------------------------------*) (* subst_conv : thm -> conv *) (* *) (* Substitution conversion. Given a theorem |- l = r, it replaces all *) (* occurrences of l in the term with r. *) (*----------------------------------------------------------------------------*) let subst_conv th tm = SUBST_CONV [(th,lhs (concl th))] tm tm;; (*----------------------------------------------------------------------------*) (* use_equality_subst : bool -> bool -> thm -> conv *) (* *) (* Function to perform substitution when using equalities. The first argument *) (* is a Boolean that controls which side of an equation substitution is to *) (* take place on. The second argument is also a Boolean, indicating whether *) (* or not we have decided to cross-fertilize. The third argument is a *) (* substitution theorem of the form: *) (* *) (* t' = s' |- t' = s' *) (* *) (* If we are not cross-fertilizing, s' is substituted for t' throughout the *) (* term. If we are cross-fertilizing, the behaviour depends on the structure *) (* of the term, tm: *) (* *) (* (a) if tm is "l = r", substitute s' for t' in either r or l. *) (* (b) if tm is "~(l = r)", substitute s' for t' throughout tm. *) (* (c) otherwise, do not substitute. *) (*----------------------------------------------------------------------------*) (* The heuristic above is modified so that in case (c) a substitution does *) (* take place. This reduces the chances of an invalid subgoal (clause) being *) (* generated, and has been shown to be a better option for certain examples. *) let use_equality_subst right cross_fert th tm = try (if cross_fert then if (is_eq tm) then (if right then RAND_CONV (subst_conv th) tm else RATOR_CONV (RAND_CONV (subst_conv th)) tm) else if ((is_neg tm) & (try(is_eq (rand tm)) with Failure _ -> false)) then subst_conv th tm else (* ALL_CONV tm *) subst_conv th tm else subst_conv th tm ) with Failure _ -> failwith "use_equality_subst";; (*----------------------------------------------------------------------------*) (* EQ_EQ_IMP_DISJ_EQ = *) (* |- !x x' y y'. (x = x') /\ (y = y') ==> (x \/ y = x' \/ y') *) (*----------------------------------------------------------------------------*) let EQ_EQ_IMP_DISJ_EQ = prove (`!x x' y y'. (x = x') /\ (y = y') ==> ((x \/ y) = (x' \/ y'))`, REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);; (*----------------------------------------------------------------------------*) (* DISJ_EQ : thm -> thm -> thm *) (* *) (* |- x = x' |- y = y' *) (* ------------------------ *) (* |- (x \/ y) = (x' \/ y') *) (*----------------------------------------------------------------------------*) let DISJ_EQ th1 th2 = try (let (x,x') = dest_eq (concl th1) and (y,y') = dest_eq (concl th2) in MP (SPECL [x;x';y;y'] EQ_EQ_IMP_DISJ_EQ) (CONJ th1 th2) ) with Failure _ -> failwith "DISJ_EQ";; (*----------------------------------------------------------------------------*) (* use_equality_heuristic : (term # bool) -> ((term # bool) list # proof) *) (* *) (* Heuristic for using equalities, and in particular for cross-fertilizing. *) (* Given a clause, the function looks for a literal of the form ~(s' = t') *) (* where t' occurs in another literal and is not an explicit value template. *) (* If no such literal is present, the function looks for a literal of the *) (* form ~(t' = s') where t' occurs in another literal and is not an explicit *) (* value template. If a substitution literal of one of these two forms is *) (* found, substitution takes place as follows. *) (* *) (* If the clause is an induction step, and there is an equality literal *) (* mentioning t' on the RHS (or LHS if the substitution literal was *) (* ~(t' = s')), and s' is not an explicit value, the function performs a *) (* cross-fertilization. The substitution function is called for each literal *) (* other than the substitution literal. Each call results in a theorem of the *) (* form: *) (* *) (* t' = s' |- old_lit = new_lit *) (* *) (* If the clause is an induction step and s' is not an explicit value, the *) (* substitution literal is rewritten to F, and so will subsequently be *) (* eliminated. Otherwise this literal is unchanged. The theorems for each *) (* literal are recombined using the DISJ_EQ rule, and the new clause is *) (* returned. See the comments for the substitution heuristic for a *) (* description of how the original clause is proved from the new clause. *) (*----------------------------------------------------------------------------*) let use_equality_heuristic (tm,(ind:bool)) = try (let checkx (tml1,tml2) t' = (not (is_explicit_value_template t')) & ((exists (is_subterm t') tml1) or (exists (is_subterm t') tml2)) in let rec split_disjuncts side prevl tml = if (can (check (checkx (prevl,tl tml)) o side o dest_neg) (hd tml)) then (prevl,tml) else split_disjuncts side ((hd tml)::prevl) (tl tml) in let is_subterm_of_side side subterm tm = (try(is_subterm subterm (side tm)) with Failure _ -> false) in let literals = disj_list tm in let (right,(overs,neq'::unders)) = try (true,(hashI rev) (split_disjuncts rhs [] literals)) with Failure _ -> (false,(hashI rev) (split_disjuncts lhs [] literals)) in let side = if right then rhs else lhs in let flipth = if right then ALL_CONV neq' else RAND_CONV SYM_CONV neq' in let neq = rhs (concl flipth) in let eq = dest_neg neq in let (s',t') = dest_eq eq in let delete = ind & (not (is_explicit_value s')) in let cross_fert = delete & ((exists (is_subterm_of_side side t') overs) or (exists (is_subterm_of_side side t') unders)) in let sym_eq = mk_eq (t',s') in let sym_neq = mk_neg sym_eq in let ass1 = EQ_MP (SYM flipth) (NOT_EQ_SYM (ASSUME sym_neq)) and ass2 = ASSUME sym_eq in let subsfun = use_equality_subst right cross_fert ass2 in let overths = map subsfun overs and neqth = if delete then TRANS (RAND_CONV (RAND_CONV (subst_conv ass2)) neq) (ISPEC s' NOT_EQ_F) else ADD_ASSUM sym_eq (REFL neq) and underths = map subsfun unders in let neqth' = TRANS flipth neqth in let th1 = itlist DISJ2 overs (try DISJ1 ass1 (list_mk_disj unders) with Failure _ -> ass1) and th2 = itlist DISJ_EQ overths (end_itlist DISJ_EQ (neqth'::underths)) and th3 = SPEC sym_eq EXCLUDED_MIDDLE in let tm' = rhs (concl th2) in let proof th = DISJ_CASES th3 (EQ_MP (SYM th2) th) th1 in (proof_print_string_l "-> Use Equality Heuristic" () ; ([(tm',ind)],apply_proof (proof o hd) [tm'])) ) with Failure _ -> failwith "use_equality_heuristic`";