1structure Rules :> Rules = 2struct 3 4open HolKernel boolLib pairLib wfrecUtils; 5 6 7val ERR = mk_HOL_ERR "Rules"; 8 9fun sthat P x = P x handle Interrupt => raise Interrupt 10 | _ => false; 11 12fun simpl_conv thl = 13 let open RW 14 val RWC = Rewrite Fully 15 (Simpls(std_simpls,thl), 16 Context([],DONT_ADD), 17 Congs[boolTheory.IMP_CONG], 18 Solver always_fails) 19 fun simpl tm = 20 let val th = Conv.THENC(RWC,Conv.DEPTH_CONV GEN_BETA_CONV) tm 21 val (lhs,rhs) = dest_eq(concl th) 22 in if aconv lhs rhs then th else TRANS th (simpl rhs) 23 end 24 in simpl 25 end; 26 27fun is_triv_rw tm = uncurry aconv (dest_eq tm) handle HOL_ERR _ => false; 28 29fun non_triv thl = filter (not o is_triv_rw o concl) thl 30 31(*---------------------------------------------------------------------------*) 32(* PURE_REWRITE_RULE plus generalized beta conversion. *) 33(*---------------------------------------------------------------------------*) 34 35fun simplify thl = 36 let val rewrite = PURE_REWRITE_RULE (non_triv thl) (* PURE_ONCE_REWRITE_RULE *) 37 fun simpl th = 38 let val th' = GEN_BETA_RULE (rewrite th) 39 val (_,c1) = dest_thm th 40 val (_,c2) = dest_thm th' 41 in if aconv c1 c2 then th else simpl th' 42 end 43 in simpl 44 end; 45 46val RIGHT_ASSOC = PURE_REWRITE_RULE [GSYM boolTheory.DISJ_ASSOC]; 47 48fun FILTER_DISCH_ALL P th = itlist DISCH (filter (sthat P) (Thm.hyp th)) th; 49 50(*---------------------------------------------------------------------------- 51 * 52 * A |- M 53 * ------------------- [v_1,...,v_n] 54 * A |- ?v1...v_n. M 55 * 56 *---------------------------------------------------------------------------*) 57 58fun EXISTL vlist thm = 59 itlist (fn v => fn thm => EXISTS(mk_exists(v,concl thm),v) thm) 60 vlist thm; 61 62(*---------------------------------------------------------------------------- 63 * 64 * A |- M[x_1,...,x_n] 65 * ---------------------------- [(x |-> y)_1,...,(x |-> y)_n] 66 * A |- ?y_1...y_n. M 67 * 68 *---------------------------------------------------------------------------*) 69 70fun IT_EXISTS theta thm = 71 itlist (fn (b as {redex,residue}) => fn thm => 72 EXISTS(mk_exists(residue, subst [b] (concl thm)), redex) thm) 73 theta thm; 74 75(*---------------------------------------------------------------------------- 76 * 77 * A1 |- M1, ..., An |- Mn 78 * --------------------------------------------------- 79 * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn] 80 * 81 *---------------------------------------------------------------------------*) 82 83fun EVEN_ORS thms = 84 let fun blue ldisjs [] _ = [] 85 | blue ldisjs (th::rst) rdisjs = 86 let val rdisj_tl = list_mk_disj(Lib.trye tl rdisjs) 87 in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) 88 :: blue (ldisjs@[concl th]) rst (Lib.trye tl rdisjs) 89 end 90 handle HOL_ERR _ => [itlist DISJ2 ldisjs th] 91 in 92 blue [] thms (map concl thms) 93 end; 94 95(*---------------------------------------------------------------------------*) 96(* *) 97(* v = pat[v1,...,vn] |- M[x] *) 98(* ------------------------------------------ *) 99(* ?v1 ... vn. v = pat[v1,...,vn] |- M[x] *) 100(* *) 101(*---------------------------------------------------------------------------*) 102 103fun CHOOSER v (tm,thm) = 104 let val ex_tm = mk_exists(v,tm) 105 in (ex_tm, CHOOSE(v, ASSUME ex_tm) thm) 106 end; 107 108fun LEFT_ABS_VSTRUCT thm = 109 let open boolSyntax 110 val veq = Lib.trye hd (filter (can dest_eq) (Thm.hyp thm)) 111 val pat = rhs veq 112 in snd(itlist CHOOSER (free_vars_lr pat) (veq,thm)) 113 end; 114 115(*---------------------------------------------------------------------------*) 116(* *) 117(* Gamma, (x = pat[v1,...,vn]) /\ constraints |- M[x] *) 118(* ------------------------------------------------------------------ *) 119(* Gamma, ?v1 ... vn. (x = pat[v1,...,vn]) /\ constraints |- M[x] *) 120(* *) 121(*---------------------------------------------------------------------------*) 122 123fun LEFT_EXISTS thm = 124 case filter (can (dest_eq o hd o strip_conj)) (Thm.hyp thm) 125 of [] => raise ERR "LEFT_EXISTS" "expected an eqn in hyps" 126 | veq_conj :: _ => 127 let val (_,pat) = dest_eq (hd (strip_conj veq_conj)) 128 in snd (itlist CHOOSER (free_vars_lr pat) (veq_conj,thm)) 129 end; 130 131end (* Rules *) 132