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