1(* wlogLib.sml - Without loss of generality tacticals 2 3 by Mario Castel��n Castro UOK 4 (see doc/copyrights/public-domain-contributions.txt) 5*) 6 7structure wlogLib :> wlogLib = 8struct 9 10open HolKernel Parse boolLib 11 12val ERR = mk_HOL_ERR "wlogLib" 13 14fun LIST_SPLICE l = 15 case l of 16 [] => raise ERR "LIST_SPLICE" "Empty list" 17 | [t1] => REFL t1 18 | [t1, t2] => QCONV (SPLICE_CONJ_CONV) (mk_conj (t1, t2)) 19 | (t::l) => 20 let 21 val deep_thm = LIST_SPLICE l 22 (* If ���deep_thm��� is ��l ��� r��, ���lifted_deep_thm��� is ��t ��� l ��� t ��� r��. UOK *) 23 val lifted_deep_thm = AP_TERM (mk_comb (conjunction, t)) deep_thm 24 in 25 RIGHT_CONV_RULE SPLICE_CONJ_CONV lifted_deep_thm 26 end 27 28fun DISCH_CONJ l thm = 29 let 30 fun loop l conj_thm thm = 31 case l of 32 [x] => 33 PROVE_HYP conj_thm thm 34 | [] => 35 thm 36 | (x::rest) => 37 loop rest (CONJUNCT2 conj_thm) (PROVE_HYP (CONJUNCT1 conj_thm) thm) 38 in 39 case l of 40 [] => thm 41 | [x] => DISCH x thm 42 | _ => let val t = list_mk_conj l in DISCH t (loop l (ASSUME t) thm) end 43 end 44 45fun UNDISCH_CONJ l thm = 46 let 47 fun fold_rator (t, acc) = 48 CONJ (ASSUME t) acc 49 in 50 case l of 51 [] => thm 52 | [t] => MP thm (ASSUME t) 53 | _ => 54 let 55 val l = rev l 56 in 57 MP thm (foldl fold_rator (ASSUME (hd l)) (tl l)) 58 end 59 end 60 handle HOL_ERR _ => raise ERR "UNDISCH_CONJ" "" 61 62(* Proves 63 ��� (��P ��� (���(vars). P_hyp ��� t) ��� t) ��� (* ���wlog_thm���. *) UOK 64 (���(vars). P ��� hyp ��� t) ��� (* ���new_sg_thm���. *) UOK 65 hyp ��� UOK 66 t�� UOK 67except that when "hyp" is "NONE", it is omitted the obvious way. If "hyp" is 68none then "p_hyp" is just "hyp" else it is the splice of "p" with "hyp". The 69tuple returned is the aforementioned theorem and "P_hyp". *) 70fun wlog_rule vars p hyp t = 71 let 72 (* val the = liteLib.the (broken in mosml) *) 73 fun the (SOME x) = x 74 | the _ = failwith "the: can't take \"the\" of NONE" 75 76 fun forall vars t = list_mk_forall (vars, t) 77 fun implies t1 t2 = mk_imp (t1, t2) 78 val new_sg_t = forall vars (implies (case hyp of 79 SOME hyp_t => mk_conj (p, hyp_t) 80 | NONE => p) 81 t) 82 val new_sg_thm = ASSUME new_sg_t 83 val thm_p = MP (SPECL vars new_sg_thm) 84 (case hyp of 85 SOME hyp_t => CONJ (ASSUME p) (ASSUME hyp_t) 86 | NONE => (ASSUME p)) 87 val wlog_ant = ref NONE 88 val splice_thm = ref NONE 89 val _ = 90 case hyp of 91 NONE => 92 wlog_ant := SOME new_sg_t 93 | SOME hyp_t => 94 case SOME (SPLICE_CONJ_CONV (mk_conj (p, hyp_t))) 95 handle UNCHANGED => NONE of 96 NONE => 97 wlog_ant := SOME new_sg_t 98 | SOME thm => 99 (wlog_ant := SOME (forall vars (implies (rhs (concl thm)) t)); 100 splice_thm := SOME thm) 101 val wlog_t = implies (mk_neg p) (implies (the (!wlog_ant)) t) 102 val wlog_thm = ASSUME wlog_t 103 val (new_sg_thm2, wlog_hyp) = 104 case !splice_thm of 105 NONE => (new_sg_thm, new_sg_t) 106 | SOME thm => 107 let 108 val gen_thm = GEN_ABS (SOME universal) 109 vars 110 (AP_THM (AP_TERM implication thm) t) 111 val new_sg_thm2 = EQ_MP gen_thm new_sg_thm 112 in 113 (new_sg_thm2, concl new_sg_thm2) 114 end 115 val thm_not_p = MP (UNDISCH wlog_thm) new_sg_thm2 116 val em_thm = SPEC p EXCLUDED_MIDDLE 117 val merged_thm = DISJ_CASES em_thm thm_p thm_not_p 118 val final_thm = (case hyp of 119 SOME hyp_t => DISCH hyp_t merged_thm 120 | NONE => merged_thm) |> 121 DISCH new_sg_t |> 122 DISCH wlog_t 123 in 124 (final_thm, wlog_hyp) 125 end 126 127fun wlog_then q vars_q (ttac :thm_tactic) (g as (asm, c)) = 128 let 129 open Parse 130 val mem = curry HOLset.member 131 val lconst = FVL asm empty_tmset 132 val context = HOLset.listItems (FVL [c] lconst) 133 val p = typed_parse_in_context bool context q 134 val extra_vars = map (parse_in_context context) vars_q 135 val extra_var_set = HOLset.addList (empty_varset, extra_vars) 136 val efv = filter (fn t => not (mem lconst t orelse mem extra_var_set t)) 137 (* The conjunction is just an arbitrary way to put p and 138 c into a single term. *) 139 (free_vars_lr (mk_conj (p, c))) 140 val gen_vars = extra_vars @ efv 141 val marked_asm = filter (fn t => exists (mem extra_var_set) (free_vars t)) 142 asm 143 val (splice_info_opt, ant, (lemma, wlog_hyp)) = 144 if null marked_asm then 145 (NONE, 146 p, 147 wlog_rule gen_vars p NONE c) 148 else 149 let 150 val thm = LIST_SPLICE marked_asm 151 val (unspliced_t, spliced_t) = dest_eq (concl thm) 152 in 153 (SOME {thm = thm, unspliced_t = unspliced_t, spliced_t = spliced_t}, 154 mk_conj (p, spliced_t), 155 wlog_rule gen_vars p (SOME spliced_t) c) 156 end 157 val not_p = mk_neg p 158 val sg1 = (not_p::wlog_hyp::asm, c) 159 val (ttac_sg, ttac_verify) = ttac (ASSUME p) (asm, c) 160 fun verify (thm1::thm_l) = 161 let 162 val ttac_thm = ttac_verify thm_l 163 (* Corresponds to the subgoal we added in this tactical. *) 164 val wlog_thm = DISCH not_p (DISCH wlog_hyp thm1) 165 in 166 case splice_info_opt of 167 SOME splice_info => 168 let 169 val (imp_splice, imp_unsplice) = 170 EQ_IMP_RULE (#thm splice_info) 171 (* Corresponds to the original subgoal processed by the 172 user-provided theorem-tactic. *) 173 val other_thm = 174 MP (DISCH_CONJ marked_asm ttac_thm) (UNDISCH imp_unsplice) |> 175 DISCH_CONJ [p, #spliced_t splice_info] |> 176 GENL gen_vars 177 in 178 UNDISCH_CONJ marked_asm (MP (MP lemma wlog_thm) other_thm) 179 end 180 | NONE => 181 let 182 val other_thm = GENL gen_vars (DISCH p ttac_thm) 183 in 184 MP (MP lemma wlog_thm) other_thm 185 end 186 end 187 | verify _ = raise ERR "wlog_then" "Verification" 188 in 189 (sg1::ttac_sg, verify) 190 end 191 192(* Convenience entry points for var_wlog_then. *) 193fun wlog_tac q vars = wlog_then q vars STRIP_ASSUME_TAC 194 195end (* struct *) 196