1structure pairTools :> pairTools =
2struct
3
4open HolKernel Parse boolLib pairSyntax pairTheory PairRules;
5
6val PERR = mk_HOL_ERR "pairTools";
7
8(* recursively expand variables with pair type *)
9local
10  val name_of = fst o dest_var
11  fun rename_tac v1 v2 =
12    FULL_STRUCT_CASES_TAC
13      (EXISTS (mk_exists(v2,(mk_eq(v1,v2))),v1) (REFL v1))
14  fun split_tac p a d =
15    FULL_STRUCT_CASES_TAC
16      (CONV_RULE (RENAME_VARS_CONV [name_of a, name_of d])
17         (ISPEC p pair_CASES))
18  fun PairCases_common v fvs g = let
19    val mk_var = variant fvs o mk_var
20    val (sv,ty) = dest_var v
21    val n = let val n = ref 0 in fn()=> !n before n := !n+1 end
22    fun split_tacs v tya tyd = let
23      fun try_split s ty = let
24        val v = mk_var((name_of v)^s,ty)
25      in (v,
26          case total dest_prod ty of
27            NONE =>
28              (fn()=> rename_tac v (mk_var(sv^(Int.toString(n())),ty)))
29          | SOME (tya, tyd) =>
30              (fn()=> split_tacs v tya tyd))
31      end
32      val (va,ka) = try_split "a" tya
33      val (vd,kd) = try_split "d" tyd
34    in
35      split_tac v va vd
36      THEN ka() THEN kd()
37    end
38  in
39    case total dest_prod (type_of v) of
40      NONE => raise PERR "PairCases_on" "Not of pair type"
41    | SOME (tya, tyd) => split_tacs v tya tyd
42  end g
43in
44  fun PairCases (g as (hyps, w)) = let
45    val fvs = free_varsl (w::hyps)
46    val (v, _) = dest_forall w
47    (* From gen_tac: *)
48    val v' = gen_variant Parse.is_constname "" fvs v
49  in
50    X_GEN_TAC v' THEN PairCases_common v' fvs
51  end g
52
53  fun PairCases_on q (g as (hyps, w)) = let
54    val fvs = free_varsl (w::hyps)
55    val v = parse_in_context fvs q
56  in
57    if is_var v then
58      PairCases_common v fvs g
59    else
60      raise PERR "PairCases_on" "Not a variable"
61  end
62end
63
64(*---------------------------------------------------------------------------
65 *
66 *     (x = (v1,...,vn))       |- M[(v1,...,vn)]
67 *    ---------------------------------------------
68 *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
69 *
70 *---------------------------------------------------------------------------*)
71
72fun VSTRUCT_ABS bind th =
73  let fun CHOOSER v (tm,thm) =
74        let val ex_tm = mk_exists(v,tm)
75        in (ex_tm, CHOOSE(v, ASSUME ex_tm) thm)
76        end
77      val L = strip_pair (rand bind)
78  in snd(itlist CHOOSER L (bind, SUBS[SYM(ASSUME bind)] th))
79  end;
80
81
82(*---------------------------------------------------------------------------
83 *
84 *              `x`   `<varstruct>`
85 *        --------------------------------
86 *          |- ?v1..vn. x = <varstruct>
87 *
88 *---------------------------------------------------------------------------*)
89
90local val pthm = GSYM pairTheory.PAIR
91in
92fun PAIR_EX x vstruct =
93 let fun pair_exists node value thm =
94      if Term.is_var value
95      then EXISTS (mk_exists(value,subst[node|->value] (concl thm)), node) thm
96      else
97      let val (V,(l,r)) = (I##dest_eq)(strip_exists(concl thm))
98          val v = genvar(type_of node)
99          val template = list_mk_exists(V,mk_eq(l, subst[node|->v] r))
100          val expansion = ISPEC node pthm
101          val pthm' = Thm.SUBST[v |-> expansion] template thm
102          val (node1, node2) = dest_pair(rhs(concl expansion))
103          val (value1,value2) = dest_pair value
104      in pair_exists node1 value1 (pair_exists node2 value2 pthm')
105      end
106      handle HOL_ERR _ => raise PERR "PAIR_EX" ""
107 in
108   pair_exists x vstruct (REFL x)
109 end
110end
111
112
113
114(*---------------------------------------------------------------------------
115 * Generalize a free tuple (vstr) into a universally quantified variable (a).
116 * There must be a faster way! Note however that the notion of "freeness" for
117 * a tuple is different than for a variable: if variables in the tuple also
118 * occur in any other place than an occurrences of the tuple, they aren't
119 * "free" (which is thus probably the wrong word to use).
120 *---------------------------------------------------------------------------*)
121
122fun PGEN a vstr th =
123   GEN a (if is_var vstr
124          then Thm.INST [vstr |-> a] th
125          else PROVE_HYP (PAIR_EX a vstr) (VSTRUCT_ABS (mk_eq(a,vstr)) th))
126
127fun PGEN_TAC vars (asl:Term.term list,tm) =
128 let val (v,_) = dest_forall tm
129     val tm'   = beta_conv(mk_comb(rand tm,vars))
130 in
131   ([(asl,tm')], fn [th] => PGEN v vars th
132                     | _ => raise PERR "PGEN_TAC" "validation")
133 end;
134
135(*---------------------------------------------------------------------------
136       |- f <vstr> = g <vstr>
137      ------------------------ PFUN_EQ_RULE
138              |- f = g
139 ---------------------------------------------------------------------------*)
140
141local val expected = PERR "PFUN_EQ_RULE" "expected f <vstruct> = g <vstruct>"
142      val SIMP = Rewrite.PURE_ONCE_REWRITE_RULE[GSYM FUN_EQ_THM]
143in
144fun PFUN_EQ_RULE th =
145 let val ((_,v1),(_,v2))
146       = with_exn ((dest_comb##dest_comb) o dest_eq o concl) th expected
147 in
148   if aconv v1 v2 then SIMP (PGEN (genvar (type_of v1)) v1 th)
149   else raise expected
150 end
151end;
152
153
154(*---------------------------------------------------------------------------*
155 *            v    (|- !v_1...v_n. M[v_1...v_n])                             *
156 *   TUPLE   -------------------------------------------------               *
157 *              !v. M[FST v, FST(SND v), ... SND(SND ... v)]                 *
158 *---------------------------------------------------------------------------*)
159
160local fun trav tm A =
161         trav (mk_fst tm) (trav (mk_snd tm) A) handle HOL_ERR _ => (tm::A)
162      fun hd1 [th] = th
163        | hd1 _ = raise Bind
164in
165fun TUPLE v thm = GEN v (SPECL (trav v []) thm)
166
167fun TUPLE_TAC vtuple:tactic = fn (asl,w) =>
168   let val (Bvar,Body) = dest_forall w
169       val w1 = subst [Bvar |-> vtuple] Body
170       val w2 = list_mk_forall(strip_pair vtuple,w1)
171   in ([(asl,w2)],
172       PURE_REWRITE_RULE[pairTheory.PAIR] o TUPLE Bvar o hd1)
173   end
174end;
175
176
177(*---------------------------------------------------------------------------
178 * Builds a list of projection terms for "rhs", based on structure
179 * of "tuple".
180
181       fun flat_vstruct0 tuple rhs =
182          if (is_var tuple) then [rhs]
183          else let val {fst,snd} = dest_pair tuple
184               in flat_vstruct0 fst (mk_fst rhs) @
185                  flat_vstruct0 snd (mk_snd rhs)
186               end;
187
188 * That was the clean implementation. Now for the one that gets used, we
189 * add an extra field to the return value, so that it can be made into
190 * an equality.
191 *---------------------------------------------------------------------------*)
192
193fun flat_vstruct tuple rhs =
194  let
195    (* behaviour of mk_fst and mk_snd should match PairedLambda.GEN_BETA_CONV in LET_INTRO *)
196    val mk_fst = fn tm => if is_pair tm then #1 (dest_pair tm) else mk_fst tm
197    val mk_snd = fn tm => if is_pair tm then #2 (dest_pair tm) else mk_snd tm
198    fun flat tuple (v,rhs) =
199      if is_var tuple then [(tuple, rhs)]
200      else let val (fst,snd) = dest_pair tuple
201           in  flat fst (v, mk_fst rhs) @
202               flat snd (v, mk_snd rhs)
203           end
204  in map mk_eq (flat tuple (genvar alpha,rhs))
205  end;
206
207
208(*---------------------------------------------------------------------------
209 *
210 *              Gamma |- (<vstruct> = M) ==> N
211 *     --------------------------------------------------
212 *              Gamma |- let <vstruct> = M in N
213 *
214 *---------------------------------------------------------------------------*)
215
216local val LET_THM1 = GSYM LET_THM
217      val PAIR_RW = PURE_REWRITE_RULE [pairTheory.PAIR]
218      fun lhs_repl th = (lhs(concl th) |-> th)
219in
220fun LET_INTRO thm =
221  let val (ant,conseq) = dest_imp(concl thm)
222      val (lhs,rhs) = dest_eq ant
223      val bindings = flat_vstruct lhs rhs
224      val thl = map ASSUME bindings
225      val th0 = UNDISCH thm
226      val th1 = SUBS thl th0
227      val Bredex = mk_comb(mk_pabs(lhs,conseq),rhs)
228      val th2 = EQ_MP (GSYM(PairedLambda.GEN_BETA_CONV Bredex)) th1
229      val th3 = PURE_ONCE_REWRITE_RULE[LET_THM1] th2
230      val vstruct_thm = SUBST_CONV (map lhs_repl thl) lhs lhs;
231      val th4 = PROVE_HYP (PAIR_RW vstruct_thm) th3
232  in
233  rev_itlist (fn bind => fn th =>
234                 let val th' = DISCH bind th
235                     val (lhs,rhs) = dest_eq bind
236                 in MP (Thm.INST [lhs |-> rhs] th') (REFL rhs) end)
237               bindings th4
238  end
239end;
240
241
242(*---------------------------------------------------------------------------
243 * Returns the variants and the "away" list augmented with the variants.
244 *---------------------------------------------------------------------------*)
245
246fun unpabs tm =
247   let val (vstr,body) = dest_pabs tm
248       val V = free_vars_lr vstr
249   in list_mk_abs(V,body)
250   end;
251
252
253local
254fun dot 0 vstr tm away = (vstr,tm)
255  | dot n vstr tm away =
256    let val (Bvar,Body) = dest_abs tm
257        val v' = variant away Bvar
258        val tm'  = beta_conv(mk_comb(tm, v'))
259        val vstr' = subst[Bvar |-> v'] vstr
260    in dot (n-1) vstr' tm' (v'::away)
261    end
262in
263(*---------------------------------------------------------------------------
264 * Alpha convert to ensure that variables bound by the "let" are not
265 * free in the assumptions of the goal. Alpha-convert in reverse on way
266 * back from achieving the goal.
267 *---------------------------------------------------------------------------*)
268
269val LET_INTRO_TAC :tactic =
270fn  (asl,w) =>
271  let val (func,arg) = dest_let w
272      val func' = unpabs func
273      val (vstr,body) = dest_pabs func
274      val away0 = Lib.op_union aconv (free_vars func) (free_varsl asl)
275      val (vstr', body') = dot (length (free_vars vstr)) vstr func' away0
276      val bind = mk_eq(vstr', arg)
277  in
278  ([(asl,mk_imp(bind,body'))],
279   fn ths => let val let_thm = LET_INTRO (hd ths)
280               in EQ_MP (ALPHA (concl let_thm) w) let_thm end)
281  end
282end;
283
284(*---------------------------------------------------------------------------
285 * Test.
286 *
287    set_goal([Term`x:bool`, Term`x':bool`],
288             Term`let (x':bool,(x:bool)) = M in x'' x x' : bool`);
289 *
290 *
291 *  g`!P x M N. (!x. x=M ==> P(N x)) ==> P(let (x = M) in N)`;
292 *
293 *---------------------------------------------------------------------------*)
294
295
296fun LET_EQ_TAC thml =
297  Ho_Rewrite.PURE_REWRITE_TAC thml
298  THEN REPEAT (LET_INTRO_TAC THEN DISCH_TAC);
299
300(*---------------------------------------------------------------------------
301 * Eliminate PABS
302 *
303
304       -----------------------------------  PABS_ELIM_CONV (\<vstr>. P vstr)
305       |- \<vstr>. P <vstr> = \x. P x
306 *
307 *---------------------------------------------------------------------------*)
308
309local
310   fun UNCURRY_ELIM_CONV t =
311      ((REWR_CONV ELIM_UNCURRY) THENC
312       (ABS_CONV (
313          RATOR_CONV (
314             ((RATOR_CONV UNCURRY_ELIM_CONV) THENC
315             BETA_CONV THENC
316             UNCURRY_ELIM_CONV)) THENC
317          BETA_CONV))) t
318      handle HOL_ERR _ => raise UNCHANGED;
319in
320
321fun PABS_ELIM_CONV t =
322  if (pairSyntax.is_pabs t) then (UNCURRY_ELIM_CONV t) else raise UNCHANGED;
323
324end
325
326
327(*---------------------------------------------------------------------------
328 * Introduces PABS
329 *
330
331       -----------------------------------  PABS_ELIM_CONV <vstr> (\x. P x)
332       |- \x. P x = \<vstr>. P vstr
333 *
334 *---------------------------------------------------------------------------*)
335
336fun PABS_INTRO_CONV vstruct tt = let
337   val (vstruct', _) = variant_of_term (free_vars tt) vstruct
338   val new_t = mk_comb (tt, vstruct')
339   val thm0 = (BETA_CONV THENC
340               REWRITE_CONV[pairTheory.FST, pairTheory.SND]) new_t
341
342   val thm1 = PairRules.PABS vstruct' thm0
343   val thm2 = CONV_RULE (LHS_CONV PairRules.PETA_CONV) thm1
344in
345   thm2
346end;
347
348(*---------------------------------------------------------------------------
349   Eliminate tupled quantification
350
351       -----------------------------------  TUPLED_QUANT_CONV `<Q><vstr>. P`
352       |- <Q><vstr>. P = <Q> v1 ... vn. P
353
354   where <Q> is one of {?,!} and <vstruct> is a varstruct made
355   from the variables v1,...,vn.
356 ---------------------------------------------------------------------------*)
357
358
359val is_uncurry_tm  = same_const pairSyntax.uncurry_tm
360val is_universal   = same_const boolSyntax.universal
361val is_existential = same_const boolSyntax.existential;
362
363local
364  val ELIM_PEXISTS2 = prove (``(?p:('a#'b). P (FST p) (SND p) p) = ?p1 p2. P p1 p2 (p1,p2)``,
365                         CONV_TAC (LHS_CONV (HO_REWR_CONV EXISTS_PROD)) THEN
366                         REWRITE_TAC[FST, SND])
367  val ELIM_PFORALL2 = prove (``(!p:('a#'b). P (FST p) (SND p) p) = !p1 p2. P p1 p2 (p1,p2)``,
368                         CONV_TAC (LHS_CONV (HO_REWR_CONV FORALL_PROD)) THEN
369                         REWRITE_TAC[FST, SND]);
370
371  val ELIM_PEXISTS_CONV = HO_REWR_CONV ELIM_PEXISTS2;
372  val ELIM_PFORALL_CONV = HO_REWR_CONV ELIM_PFORALL2;
373
374  fun dest_tupled_quant tm =
375    case total dest_comb tm
376     of NONE => NONE
377      | SOME(f,x) =>
378        if is_comb x andalso is_uncurry_tm (rator x)
379        then if is_existential f then SOME ELIM_PEXISTS_CONV else
380             if is_universal f   then SOME ELIM_PFORALL_CONV
381             else NONE
382        else NONE
383
384  fun PQUANT_ELIM_CONV quant_elim vc =
385      if (is_var vc) then (RAND_CONV (ALPHA_CONV vc)) else
386      let
387         val (vc1, vc2) = pairSyntax.dest_pair vc;
388         val conv = (quant_elim THENC
389                    (QUANT_CONV (PQUANT_ELIM_CONV quant_elim vc2)) THENC
390                    (PQUANT_ELIM_CONV quant_elim vc1));
391      in
392         conv
393      end;
394in
395   fun ELIM_TUPLED_QUANT_CONV tm =
396      case dest_tupled_quant tm
397         of NONE => raise PERR "TUPLED_QUANT_CONV" ""
398          | SOME (quant_elim) =>
399               ((RAND_CONV PABS_ELIM_CONV) THENC
400                PQUANT_ELIM_CONV quant_elim (fst (dest_pabs(rand tm)))) tm
401
402   fun SPLIT_QUANT_CONV vc tm =
403      let
404         val quant_elim =
405                 if is_universal (rator tm) then ELIM_PFORALL_CONV else
406                 if is_existential (rator tm) then ELIM_PEXISTS_CONV else
407                 raise PERR "SPLIT_QUANT_CONV" ""
408         val (v, _) = dest_abs (rand tm) handle HOL_ERR _ => raise PERR "SPLIT_QUANT_CONV" ""
409         val _ = if (type_of vc = type_of v) then () else raise PERR "SPLIT_QUANT_CONV" "";
410      in
411         PQUANT_ELIM_CONV quant_elim vc tm
412      end;
413end;
414
415
416
417local
418  val PFORALL_THM2 = prove (
419    ``!P:'a->'b->bool. (!x. $! (P x)) = $! (UNCURRY P)``,
420    GEN_TAC THEN
421    Q.SUBGOAL_THEN `P = (\x y. P x y)`
422       (fn thm => ONCE_ASM_REWRITE_TAC [thm])
423    THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC[]) THEN
424    BETA_TAC THEN REWRITE_TAC [PFORALL_THM]);
425
426  val PEXISTS_THM2 = prove (
427    ``!P:'a->'b->bool. (?x. $? (P x)) = $? (UNCURRY P)``,
428    GEN_TAC THEN
429    Q.SUBGOAL_THEN `P = (\x y. P x y)`
430       (fn thm => ONCE_ASM_REWRITE_TAC [thm])
431    THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC[]) THEN
432    BETA_TAC THEN REWRITE_TAC [PEXISTS_THM]);
433in
434  fun PEXISTS_INTRO_CONV tm =
435      (((TRY_CONV ELIM_TUPLED_QUANT_CONV) THENC
436        (QUANT_CONV PEXISTS_INTRO_CONV) THENC
437        (HO_REWR_CONV PEXISTS_THM2)) tm) handle HOL_ERR _ => raise UNCHANGED
438
439  fun PFORALL_INTRO_CONV tm =
440      (((TRY_CONV ELIM_TUPLED_QUANT_CONV) THENC
441        (QUANT_CONV PFORALL_INTRO_CONV) THENC
442        (HO_REWR_CONV PFORALL_THM2)) tm) handle HOL_ERR _ => raise UNCHANGED
443
444  fun INTRO_TUPLED_QUANT_CONV tm =
445      if is_universal (rator tm) then PFORALL_INTRO_CONV tm else
446      if is_existential (rator tm) then PEXISTS_INTRO_CONV tm else
447         raise PERR "INTRO_TUPLED_QUANT_CONV" ""
448end;
449
450
451end
452