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