1(*---------------------------------------------------------------------------*
2 * Theory of pairs and associated support.                                   *
3 *---------------------------------------------------------------------------*)
4
5structure pairLib :> pairLib =
6struct
7
8local open pairTheory pairSimps pairTools PairRules in end;
9
10open HolKernel boolLib pairSyntax PairedLambda pairTools simpLib;
11
12fun pairLib_ERR src msg = mk_HOL_ERR "pairLib" src msg
13
14val _ = Rewrite.add_implicit_rewrites pairTheory.pair_rws;
15
16(* Implementation of new_specification as a rule derived from
17   gen_new_specification. This occurs here because the derivation
18   depends on pairs. *)
19
20(* given (��(x,y,...) ...) arg                            (UOK)
21  produces an assumption:
22  arg = (x,y,...)
23  where the variables may be primed if necessary *)
24fun split_uncurry_arg_tac tm =
25  let
26    val (f,p) = dest_comb tm
27    val (x,b) = pairSyntax.dest_pabs f
28    val (x,s) = variant_of_term (free_vars p) x
29    val xs = pairSyntax.strip_pair x
30    val g = list_mk_exists(xs,mk_eq(p,x))
31    (* ?x y z ... .  arg = (x,y,z,...) *)
32    val th =
33        prove(g, simpLib.SIMP_TAC boolSimps.bool_ss
34                                  [GSYM pairTheory.EXISTS_PROD])
35  in
36    strip_assume_tac th
37  end
38
39local
40  val find_and_split_pair =
41      partial(pairLib_ERR"find_and_split_pair""not found")
42             (bvk_find_term
43                (fn (ls,tm) =>
44                    is_comb tm andalso
45                    List.all (not o
46                              curry HOLset.member(FVL[rand tm]empty_tmset)) ls)
47                split_uncurry_arg_tac)
48in
49val pairarg_tac =
50    (fn g => find_and_split_pair (#2 g) g) ORELSE
51    first_assum(find_and_split_pair o concl)
52end (* local *)
53
54local
55  exception Not_pair_case
56  fun loop tm vs =
57    let
58      val _ = assert is_pair_case tm
59      val (f,x) = dest_comb tm
60    in
61      let
62        val (v,b) = dest_abs x
63        val vs = v::vs
64      in
65        case total dest_abs b of
66          NONE => (vs,tm)
67        | SOME (v,tm) => loop tm vs
68          handle Not_pair_case => (v::vs,tm)
69      end handle HOL_ERR _ => (vs,tm)
70    end handle HOL_ERR _ => raise Not_pair_case
71in
72fun strip_pair_case tm =
73    (case loop tm [] of (vs,b) => (lhand tm,rev vs,b))
74    handle Not_pair_case =>
75           raise pairLib_ERR "strip_pair_case" "not a pair case"
76
77fun split_pair_case0_tac tm =
78  let
79    open boolSimps simpLib
80    val (p,vs,b) = strip_pair_case tm
81    val vs = map (variant (free_vars p)) vs
82    val g = list_mk_exists(vs,mk_eq(p,pairSyntax.list_mk_pair vs))
83    val th = prove(g, SIMP_TAC bool_ss [GSYM pairTheory.EXISTS_PROD])
84  in
85    strip_assume_tac th
86  end
87end (* local *)
88
89
90local
91open pairSyntax
92fun find_split t g =
93      partial(pairLib_ERR"split_pair_case_tac" "not found")
94        (bvk_find_term
95           (fn (ls,tm) =>
96               is_pair_case tm andalso
97               let val fvs = FVL [lhand tm] empty_tmset
98               in
99                 List.all (fn bv => not(HOLset.member(fvs,bv))) ls
100               end)
101           split_pair_case0_tac) t g
102in
103fun split_pair_case_tac (g as (_,w)) =
104  (find_split w ORELSE first_assum (find_split o concl)) g
105
106end (* local *)
107
108local
109  open Term Thm
110
111  (* given a varstruct (possibly nested pairs of variables) vs, return a list
112     of equations equating each variable to the corresponding projection of tm
113     e.g. varstruct_to_eqs tm ((p,q),r) =
114          [r = SND tm,
115           q = SND (FST tm),
116           p = FST (FST tm)] *)
117  fun varstruct_to_eqs tm =
118    let
119      fun f tm ac vs =
120        if is_var vs
121          then (mk_eq(vs, tm))::ac
122        else
123          let
124            val (a,d) = dest_pair vs
125            val ac = f (mk_fst tm) ac a
126            val ac = f (mk_snd tm) ac d
127          in ac end
128    in
129      f tm []
130    end
131
132  val strip_n_exists =
133    let
134      fun f a n tm =
135        if n = 0 then (List.rev a,tm)
136        else let
137          val (x,tm) = dest_exists tm
138        in
139          f (x::a) (n-1) tm
140        end
141    in f [] end
142
143  fun nconv 0 c = ALL_CONV
144    | nconv 1 c = c
145    | nconv n c = c THENC (nconv (n-1) c)
146
147  open Lib PairRules pairSyntax
148
149  in
150
151  fun new_specification (name,cnames,th) = let
152    val n = List.length cnames in if n = 0 then
153      Theory.Definition.gen_new_specification (name,th)
154    else let
155    val th1 =
156      (* CONV_RULE (RENAME_VARS_CONV cnames) th
157         is not good enough since it doesn't guarantee the cnames will be used
158        - primed variants could be used if they clash with existing constant names
159      *)
160      let
161        val tm1 = concl th
162        val (vs1,body1) = strip_n_exists n tm1
163        val tys = map type_of vs1
164        val vs2 = map2 (curry mk_var) cnames tys
165        val body2 = Term.subst (map2 (curry op |->) vs1 vs2) body1
166        val tm2 = list_mk_exists(vs2,body2)
167        val th2 = ALPHA tm1 tm2
168      in EQ_MP th2 th end
169    (* turn it into a single paired existential *)
170    val th2 = CONV_RULE (nconv (n-1) UNCURRY_EXISTS_CONV) th1
171    val (vs,body) = dest_pexists (concl th2)
172    val witness = mk_pselect (vs,body)
173    val eqs = varstruct_to_eqs witness vs
174    val th3 = CONV_RULE PEXISTS_CONV th2
175    val th4 = PURE_REWRITE_RULE (List.map (SYM o ASSUME) eqs) th3
176    (* ensure that even totally unconstrained constants get defined *)
177    val th5 = List.foldl (Lib.uncurry ADD_ASSUM) th4 eqs
178    in
179      Theory.Definition.gen_new_specification (name,th5)
180    end end
181
182end
183
184val add_pair_compset = computeLib.add_thms
185  (List.map computeLib.lazyfy_thm
186     let open pairTheory in
187       [CLOSED_PAIR_EQ,FST,SND,pair_case_thm,SWAP_def,
188        CURRY_DEF,UNCURRY_DEF,PAIR_MAP_THM]
189     end)
190
191val () = add_pair_compset computeLib.the_compset
192
193end
194