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