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