1(*****************************************************************************) 2(* File: translateLib.sml *) 3(* Author: James Reynolds *) 4(* *) 5(* Provides tools to assist in proving theorems about translation between *) 6(* s-expressions and native HOL *) 7(*****************************************************************************) 8 9structure translateLib :> translateLib = 10struct 11 12open Feedback Lib Type Term boolSyntax Thm Drule Tactical Thm_cont Tactic Conv; 13 14(*****************************************************************************) 15(* DOUBLE_MATCH: Like PART_MATCH but matches variables in the term as well *) 16(*****************************************************************************) 17 18local 19 val match = mk_HOL_ERR "translateLib" "DOUBLE_MATCH" "Couldn't match terms" 20 21 fun inst_it a b = ((* print_term a ; print " --> " ; print_term b ; print "\n" ; *) inst (match_type (type_of a) (type_of b))) 22 23 (* fun subst a = (app (fn {redex,residue} => (print_term redex ; print " |-> " ; print_term residue ; print "\n")) a ; Term.subst a); *) 24 25 (* Matches instantiating free variables to terms if possible, or instantiating t1 |-> t2 if not *) 26 fun tmatch (t1,t2) = 27 case (strip_comb t1) 28 of (fx,x::xs) => (case (strip_comb t2) 29 of (fy,y::ys) => 30 let val diff = length (y::ys) - length (x::xs) 31 val (fy',ys,fx',xs) = if 0 < diff then (list_mk_comb(fy,(List.take(y::ys,diff))),List.drop(y::ys,diff),fx,x::xs) 32 else (fy,y::ys,list_mk_comb(fx,(List.take(x::xs,~diff))),List.drop(x::xs,~diff)) 33 in 34 (fn f' => foldl (fn (m,f) => tmatch ((f ## f) m) o f) f' (map (f' ## f') (zip xs ys))) 35 (if is_var fx' then (subst [inst_it fx' fy' fx' |-> fy']) 36 else (if same_const fx' fy' then I 37 else (if is_var fy' then (subst [inst_it fy' fx' fy' |-> fx'] o inst_it fy' fx') else raise match))) 38 end 39 | (fy,[]) => if is_var fy then subst [inst_it fy t1 fy |-> t1] o inst_it fy t1 else raise match) 40 | (fx,[]) => 41 if is_var fx then (subst [inst_it fx t2 fx |-> t2]) else 42 (if same_const fx t2 then I else (if is_var t2 then (subst [inst_it t2 fx t2 |-> fx] o inst_it t2 fx) else raise match)) 43in 44 fun DOUBLE_MATCH opr1 opr2 term thm = 45 let val t1 = (opr1 o concl o SPEC_ALL) thm 46 in PART_MATCH opr1 (SPEC_ALL thm) (tmatch (opr2 t1,opr2 term) term) 47 end 48end; 49 50 51(*****************************************************************************) 52(* CHOOSEP: Tactic to choose values if a predicate exists *) 53(*****************************************************************************) 54 55local 56fun snd_to_last_imp term = 57 case (strip_imp term) of ([],a) => a | (xs,a) => last xs; 58fun last_two_imps term = 59 case (strip_imp term) of ([],a) => a | (xs,a) => mk_imp(last xs,a); 60fun MATCH opr1 opr2 de_thms a = 61 tryfind (DOUBLE_MATCH opr1 opr2 a o DISCH_ALL o SPEC_ALL o UNDISCH_ALL) 62 de_thms 63 64fun fix_hyps de_thms thm = 65let val hs = mapfilter (fn x => (x,(fn (a,b) => 66 (GENL a o MATCH last_two_imps I de_thms) b) (strip_forall x))) 67 (filter is_forall (hyp thm)) 68in if null hs then thm else 69 fix_hyps de_thms (foldl (uncurry PROVE_HYP o (snd ## I)) 70 (foldl (uncurry INST_TY_TERM) thm 71 (map (uncurry match_term o (I ## concl)) hs)) hs) 72end; 73val sexp_to_term = rand o lhs o concl 74val var = rhs o concl 75fun exist L thm = 76let val new_var = 77 if is_var (var thm) 78 then mk_var(prime((fst o dest_var o var) thm), 79 (type_of o sexp_to_term) thm) 80 else variant (free_varsl L) 81 (mk_var("x",(type_of o sexp_to_term) thm)) 82in EXISTS (Psyntax.mk_exists(new_var, 83 subst [sexp_to_term thm |-> new_var] (concl thm)),sexp_to_term thm) thm 84end 85in 86fun CHOOSEP decode_encode_thms x = 87 DISCH_ALL (fix_hyps decode_encode_thms 88 (MATCH_MP ( 89 (DISCH x o UNDISCH_ALL o 90 MATCH snd_to_last_imp (rator o rand) decode_encode_thms) x) 91 (ASSUME x))) 92fun CHOOSEP_TAC decode_encode_thms (assums,goal) = 93 MAP_EVERY 94 (CHOOSE_THEN SUBST_ALL_TAC o GSYM) 95 (mapfilter (fn x => exist (goal::assums) 96 (fix_hyps decode_encode_thms 97 (MATCH_MP ((DISCH x o UNDISCH_ALL o MATCH snd_to_last_imp 98 rand decode_encode_thms) x) (ASSUME x)))) assums) 99 (assums,goal) 100end; 101 102(*****************************************************************************) 103(* DISJ_CASES_UNIONL: Like DISJ_CASES_UNION but with a list *) 104(*****************************************************************************) 105 106fun DISJ_CASES_UNIONL nchotomy thms = 107let val concls = map concl thms 108 fun make_or (n,t) = 109 let val (pre,post) = (I ## tl) (split_after n concls); 110 in foldl (uncurry DISJ2) (if not (null post) then DISJ1 t (list_mk_disj post) else t) (rev pre) 111 end 112in 113 DISJ_CASESL nchotomy (map make_or (enumerate 0 thms)) 114end; 115 116(*****************************************************************************) 117(* Some common destructors / constructors *) 118(*****************************************************************************) 119 120fun raise_error a b = raise (mk_HOL_ERR "translateLib" a b) 121 122(* Create and destruct acl2_cond *) 123val ite_tm = ``ite``; 124 125fun mk_acl2_cond (p,a,b) = 126 if not (type_of a = ``:sexp`` andalso type_of b = ``:sexp`` andalso type_of p = ``:sexp``) then raise_error "mk_acl2_cond" "Arguments not of type :sexp" 127 else mk_comb(mk_comb(mk_comb(ite_tm,p),a),b); 128 129fun dest_acl2_cond term = 130 case strip_comb term 131 of (ite,[p,a,b]) => 132 if same_const ite ite_tm 133 then (p,a,b) 134 else raise_error "dest_acl2_cond" "not an application of \"ite\"" 135 | _ => raise_error "dest_acl2_cond" "not an application of \"ite\"" 136 137fun is_acl2_cond term = 138 case strip_comb term 139 of (ite,[p,a,b]) => same_const ite ite_tm | _ => false; 140 141 142(* Create and destruct acl2_cons *) 143val acl2_cons_tm = ``cons``; 144 145fun mk_acl2_cons (a,b) = 146 if not (type_of a = ``:sexp`` andalso type_of b = ``:sexp``) then raise_error "mk_acl2_cons" "Arguments not of type :sexp" 147 else mk_comb(mk_comb(acl2_cons_tm,a),b); 148 149fun dest_acl2_cons term = 150 case strip_comb term 151 of (acl2_cons,[a,b]) => if same_const acl2_cons acl2_cons_tm then (a,b) else raise_error "dest_acl2_cons" "not an application of \"cons\"" 152 | _ => raise_error "dest_acl2_cons" "not an application of \"cons\""; 153 154fun strip_cons term = 155 case (strip_comb term) 156 of (a,[l,r]) => if same_const a ``cons`` then (strip_cons l) @ (strip_cons r) else [term] 157 | _ => [term]; 158 159(* Create and destruct acl2_true *) 160val acl2_true_tm = ``$|=``; 161 162val mk_acl2_true = curry mk_comb acl2_true_tm; 163 164fun dest_acl2_true term = 165 case strip_comb term 166 of (acl2_true,[a]) => if same_const acl2_true acl2_true_tm then a else raise_error "dest_acl2_true" "Not an application of \"|=\"" 167 | _ => raise_error "dest_acl2_true" "Not an application of \"|=\""; 168 169fun is_acl2_true term = 170 case strip_comb term of (acl2_true,[a]) => same_const acl2_true acl2_true_tm | _ => false; 171 172(*****************************************************************************) 173(* RAT_CONG_TAC: *) 174(* *) 175(* Abbreviates as x = rep_rat (abs_rat (abs_frac (a,b))) and adds the *) 176(* rational equivalence: *) 177(* |- frac_nmr x * frac_dnm (abs_frac (a,b)) = *) 178(* frac_nmr (abs_frac (a,b)) * frac_dnm x *) 179(* *) 180(*****************************************************************************) 181 182val RAT_CONG_TAC = 183 REPEAT (POP_ASSUM MP_TAC) THEN 184 REPEAT (Q.PAT_ABBREV_TAC 185 `x = rep_rat (abs_rat (abs_frac (a''''',b''''')))`) THEN 186 REPEAT (DISCH_TAC) THEN 187 EVERY_ASSUM (fn th => 188 (ASSUME_TAC o Rewrite.REWRITE_RULE [ratTheory.RAT] o 189 AP_TERM ``abs_rat``) 190 (Rewrite.REWRITE_RULE [markerTheory.Abbrev_def] th) 191 handle e => ALL_TAC) THEN 192 RULE_ASSUM_TAC (Rewrite.REWRITE_RULE [ratTheory.RAT_EQ]); 193 194(*****************************************************************************) 195(* A ?- ?m. P m /\ (m = A) /\ .... *) 196(* -------------------------------- EQUAL_EXISTS_TAC *) 197(* A ?- P A /\ .... *) 198(*****************************************************************************) 199 200fun EQUAL_EXISTS_TAC (a,g) = 201let val (v,body) = dest_exists g 202 val eq_thms = filter is_eq (strip_conj body) 203 val term = first (curry op= v o lhs) eq_thms 204in 205 EXISTS_TAC (rhs term) (a,g) 206end; 207 208(*****************************************************************************) 209(* A u {!a b... P ==> !c d ... Q ==> ... ==> X} ?- G *) 210(* ------------------------------------------------- FIX_CI_TAC *) 211(* A u {!a b c d ... . P /\ Q /\ ... ==> X} ?- G *) 212(* *) 213(* Allows an assumption generated by completeInduct_on to be used by *) 214(* FIRST_ASSUM MATCH_MP_TAC. *) 215(* *) 216(*****************************************************************************) 217 218val FIX_CI_TAC = 219 RULE_ASSUM_TAC (CONV_RULE (REPEATC ( 220 (STRIP_QUANT_CONV RIGHT_IMP_FORALL_CONV) ORELSEC 221 (STRIP_QUANT_CONV (REWR_CONV boolTheory.AND_IMP_INTRO))))); 222 223 224end