1structure nomdatatype :> nomdatatype = 2struct 3 4 5open binderLib HolKernel Parse boolLib bossLib generic_termsTheory 6open nomsetTheory 7 8type coninfo = {con_termP : thm, con_def : thm} 9 10val cpm_ty = let val sty = stringSyntax.string_ty 11 in 12 listSyntax.mk_list_type (pairSyntax.mk_prod (sty, sty)) 13 end 14 15fun list_mk_icomb(f, args) = List.foldl (mk_icomb o swap) f args 16 17(* utility functions *) 18fun rpt_hyp_dest_conj th = let 19 fun foldthis (t, acc) = let 20 fun dc t = let 21 val (c1, c2) = dest_conj t 22 in 23 CONJ (dc c1) (dc c2) 24 end handle HOL_ERR _ => ASSUME t 25 in 26 PROVE_HYP (dc t) acc 27 end 28in 29 HOLset.foldl foldthis th (hypset th) 30end 31 32fun hCONJ th1 th2 = 33 case (hyp th1, hyp th2) of 34 ([h1], [h2]) => let 35 val h12 = ASSUME(mk_conj(h1,h2)) 36 in 37 CONJ th1 th2 38 |> PROVE_HYP (CONJUNCT1 h12) 39 |> PROVE_HYP (CONJUNCT2 h12) 40 end 41 | _ => CONJ th1 th2 42 43val FINITE_t = mk_thy_const{Name = "FINITE", Thy = "pred_set", 44 Ty = (stringSyntax.string_ty --> bool) --> bool} 45 46fun elim_unnecessary_atoms {finite_fv} fths = let 47 fun mainconv t = let 48 val (vs, bod) = strip_forall t 49 val (v,rest) = case vs of 50 [] => raise mk_HOL_ERR "nomdatatype" "elim_unnecessary_atoms" 51 "Not a forall" 52 | v::vs => (v,vs) 53 val _ = Type.compare(type_of v, stringSyntax.string_ty) = EQUAL orelse 54 raise mk_HOL_ERR "nomdatatype" "elim_unnecessary_atoms" 55 "Forall not of an atom" 56 val (h, c) = dest_imp bod 57 val _ = free_in v h andalso not (free_in v c) orelse 58 raise mk_HOL_ERR "nomdatatype" "elim_unnecessary_atoms" 59 "Uneliminable atom" 60 fun PROVE_FINITE t = let 61 open pred_setTheory pred_setSyntax 62 val (v, bod) = dest_exists t 63 val cs = strip_conj bod 64 fun getset t = let 65 val t0 = dest_neg t 66 in 67 if is_in t0 then rand t0 else mk_set [rhs t0] 68 end 69 val sets = map getset cs 70 val union = List.foldl (mk_union o swap) (hd sets) (tl sets) 71 val finite_t = mk_finite union 72 val finite_th = 73 REWRITE_CONV (FINITE_UNION::FINITE_INSERT::FINITE_EMPTY::finite_fv::fths) 74 finite_t 75 val fresh_exists = MATCH_MP basic_swapTheory.new_exists (EQT_ELIM finite_th) 76 |> REWRITE_RULE [IN_UNION, IN_INSERT, NOT_IN_EMPTY, 77 DE_MORGAN_THM, GSYM CONJ_ASSOC] 78 in 79 EQT_INTRO fresh_exists 80 end 81 82 val base = HO_REWR_CONV LEFT_FORALL_IMP_THM THENC 83 LAND_CONV (((CHANGED_CONV EXISTS_AND_REORDER_CONV THENC 84 RAND_CONV PROVE_FINITE) ORELSEC 85 PROVE_FINITE)) THENC 86 REWRITE_CONV [] 87 fun recurse t = ((SWAP_FORALL_CONV THENC BINDER_CONV recurse) ORELSEC base) t 88 in 89 recurse 90 end t 91in 92 CONV_RULE (ONCE_DEPTH_CONV mainconv) 93end 94 95 96 97val gterm_ty = mk_thy_type {Thy = "generic_terms", Tyop = "gterm", 98 Args = [beta,alpha]} 99 100local 101 val num_ty = numSyntax.num 102 val numlist_ty = listSyntax.mk_list_type num_ty 103 val string_ty = stringSyntax.string_ty 104in 105val genind_t = 106 mk_thy_const {Thy = "generic_terms", Name = "genind", 107 Ty = (num_ty --> alpha --> bool) --> 108 (num_ty --> beta --> numlist_ty --> numlist_ty --> bool) --> 109 num_ty --> gterm_ty --> bool} 110val GVAR_t = mk_thy_const {Thy = "generic_terms", Name = "GVAR", 111 Ty = string_ty --> alpha --> gterm_ty} 112end 113 114fun first2 l = 115 case l of 116 (x::y::_) => (x,y) 117 | _ => raise Fail "first2: list doesn't have at least two elements" 118 119fun new_type_step1 tyname n {vp, lp} = let 120 val list_mk_icomb = uncurry (List.foldl (mk_icomb o swap)) 121 val termP = 122 list_mk_icomb (genind_t, [vp,lp,numSyntax.mk_numeral (Arbnum.fromInt n)]) 123 fun termPf x = mk_comb(termP, x) 124 val (gtty,_) = dom_rng (type_of termP) 125 val x = mk_var("x",gtty) and y = mk_var("y", gtty) 126 val (glam_ty, gvar_ty) = first2 (#2 (dest_type gtty)) 127 val term_exists = 128 prove(mk_exists(x, mk_comb(termP, x)), 129 EXISTS_TAC (list_mk_icomb(inst [beta |-> glam_ty] GVAR_t, 130 [mk_arb stringSyntax.string_ty, 131 mk_arb gvar_ty])) THEN 132 MATCH_MP_TAC (genind_rules |> SPEC_ALL |> CONJUNCT1) THEN 133 BETA_TAC THEN REWRITE_TAC []) 134 val {absrep_id, newty, repabs_pseudo_id, termP, termP_exists, termP_term_REP, 135 term_ABS_t, term_ABS_pseudo11, 136 term_REP_t, term_REP_11} = 137 newtypeTools.rich_new_type (tyname, term_exists) 138in 139 {term_ABS_pseudo11 = term_ABS_pseudo11, term_REP_11 = term_REP_11, 140 term_REP_t = term_REP_t, term_ABS_t = term_ABS_t, absrep_id = absrep_id, 141 repabs_pseudo_id = repabs_pseudo_id, genind_term_REP = termP_term_REP, 142 genind_exists = termP_exists, newty = newty, termP = termP} 143end 144 145fun termP_removal (info as {elimth,absrep_id,tpm_def,termP,repty}) t = let 146 val (v, body) = dest_forall t 147 fun ELIM_HERE t = let 148 val (v,body) = dest_forall t 149 val (h,c) = dest_imp body 150 in 151 BINDER_CONV (LAND_CONV 152 (markerLib.move_conj_left (aconv (mk_comb(termP, v)))) THENC 153 TRY_CONV (REWR_CONV (GSYM AND_IMP_INTRO)) THENC 154 RAND_CONV (UNBETA_CONV v)) THENC 155 REWR_CONV elimth THENC BINDER_CONV BETA_CONV THENC 156 PURE_REWRITE_CONV [absrep_id, GSYM tpm_def] 157 end t 158 159in 160 if Type.compare(type_of v, repty) = EQUAL then 161 (SWAP_FORALL_CONV THENC BINDER_CONV (termP_removal info)) ORELSEC 162 ELIM_HERE 163 else NO_CONV 164end t 165 166fun lift_exfunction {repabs_pseudo_id, term_REP_t, cons_info} th = let 167 fun mk_conremove {con_termP, con_def} = 168 con_termP |> MATCH_MP repabs_pseudo_id 169 |> CONV_RULE (LAND_CONV (RAND_CONV (REWR_CONV (GSYM con_def)))) 170 |> SYM 171 val conremoves = map mk_conremove cons_info 172 val f_REP_o = let 173 val (d,r) = dom_rng (type_of term_REP_t) 174 val f = mk_var("f", r --> Type.gen_tyvar()) 175 val x = mk_var("x", d) 176 in 177 prove( 178 mk_eq(mk_comb(f, mk_comb(term_REP_t, x)), 179 mk_comb(combinSyntax.mk_o(f, term_REP_t), x)), 180 CONV_TAC (RAND_CONV (REWR_CONV combinTheory.o_THM)) THEN REFL_TAC) 181 end 182 183 fun fREPo_CONV t = let 184 val (v, bod) = dest_exists t 185 val o_t = combinSyntax.o_tm |> inst [alpha |-> Type.gen_tyvar()] 186 val fREPo = list_mk_icomb(o_t, [v, term_REP_t]) 187 in 188 BINDER_CONV (UNBETA_CONV fREPo) t 189 end 190 191 fun elimfREPo th = let 192 val (v,bod) = dest_exists (concl th) 193 val (vnm, _) = dest_var v 194 val bod_th = ASSUME bod 195 val (P, arg) = dest_comb bod 196 val newf = mk_var(vnm, type_of arg) 197 val newbod = mk_comb(P, newf) 198 in 199 CHOOSE (v, th) (EXISTS (mk_exists(newf, newbod), arg) bod_th) 200 |> CONV_RULE (BINDER_CONV BETA_CONV) 201 end 202in 203 th |> REWRITE_RULE (f_REP_o::conremoves) 204 |> CONV_RULE fREPo_CONV 205 |> elimfREPo 206end 207 208fun sort_uvars t = let 209 val (v, bod) = dest_forall t 210 val (v', _) = dest_forall bod 211 val (nm1, ty1) = dest_var v 212 val (nm2, ty2) = dest_var v' 213 fun tycmp (ty1,ty2) = 214 if Type.compare(ty1,ty2) = EQUAL then EQUAL 215 else if Type.compare(ty1,``:string``) = EQUAL then LESS 216 else if is_vartype ty2 andalso not (is_vartype ty1) then LESS 217 else Type.compare(ty1, ty2) 218in 219 if pair_compare(tycmp,String.compare) ((ty1,nm1), (ty2,nm2)) = GREATER then 220 SWAP_FORALL_CONV 221 else NO_CONV 222end t 223 224fun rename_vars alist t = let 225 val (bv, _) = dest_abs t 226 val (v, _) = dest_var bv 227in 228 case Lib.total (Lib.assoc v) alist of 229 NONE => NO_CONV 230 | SOME v' => RENAME_VARS_CONV [v'] 231end t 232 233fun prove_alpha_fcbhyp {ppm, alphas, rwts} th = let 234 open nomsetTheory 235 val th = rpt_hyp_dest_conj (UNDISCH th) 236 fun foldthis (h,th) = let 237 val h_th = 238 TAC_PROOF(([], h), 239 rpt gen_tac >> strip_tac >> 240 FIRST (map (match_mp_tac o GSYM) alphas) >> 241 match_mp_tac (GEN_ALL notinsupp_fnapp) >> 242 EXISTS_TAC ppm >> 243 srw_tac [] rwts) 244 in 245 PROVE_HYP h_th th 246 end 247in 248 HOLset.foldl foldthis th (hypset th) 249end 250 251val pi_t = mk_var("pi", cpm_ty) 252val gterm_ty = mk_thy_type {Tyop = "gterm", Thy = "generic_terms", 253 Args = [beta,alpha]} 254val pmact_t = prim_mk_const{Name = "pmact", Thy = "nomset"} 255val mk_pmact_t = prim_mk_const{Name = "mk_pmact", Thy = "nomset"} 256val raw_gtpm_t = 257 mk_thy_const{Name = "raw_gtpm", Thy = "generic_terms", 258 Ty = cpm_ty --> gterm_ty --> gterm_ty} 259val gtpm_t = mk_icomb(pmact_t, mk_icomb(mk_pmact_t, raw_gtpm_t)) 260 261fun defined_const th = th |> concl |> strip_forall |> #2 |> lhs |> repeat rator 262 263val pmact_absrep' = pmact_bijections |> CONJUNCT2 |> GSYM 264 265fun Save_thm(n, th) = save_thm(n,th) before BasicProvers.export_rewrites [n] 266 267fun define_permutation { name_pfx, name, term_ABS_t, term_REP_t, 268 absrep_id, repabs_pseudo_id, newty, 269 genind_term_REP, cons_info} = let 270 val tpm_name = name_pfx ^ "pm" 271 val raw_tpm_name = "raw_" ^ tpm_name 272 val raw_tpm_t = mk_var(raw_tpm_name, cpm_ty --> newty --> newty) 273 val t = mk_var("t", newty) 274 val raw_tpm_def = new_definition( 275 raw_tpm_name ^ "_def", 276 mk_eq(list_mk_comb(raw_tpm_t, [pi_t, t]), 277 mk_comb(term_ABS_t, 278 list_mk_icomb(gtpm_t, [pi_t, mk_comb(term_REP_t, t)])))) 279 val raw_tpm_t = defined_const raw_tpm_def 280 val t_pmact_name = name ^ "_pmact" 281 val t_pmact_t = mk_icomb(mk_pmact_t, raw_tpm_t) 282 val tpm_t = mk_icomb(pmact_t, t_pmact_t) 283 val _ = overload_on (t_pmact_name, t_pmact_t) 284 val _ = overload_on (tpm_name, tpm_t) 285 val (termP_t, REPg) = dest_comb (concl genind_term_REP) 286 val termP_gtpmREP = 287 mk_comb(termP_t, list_mk_icomb(gtpm_t, [pi_t, REPg])) 288 |> PURE_REWRITE_CONV [genind_gtpm_eqn] 289 |> SYM |> C EQ_MP genind_term_REP 290 val term_REP_raw_tpm = 291 raw_tpm_def |> SPEC_ALL |> AP_TERM term_REP_t 292 |> PURE_REWRITE_RULE [MATCH_MP repabs_pseudo_id termP_gtpmREP] 293 val tpm_raw = store_thm( 294 tpm_name ^ "_raw", 295 mk_eq(tpm_t, raw_tpm_t), 296 REWRITE_TAC[pmact_absrep', is_pmact_def, FUN_EQ_THM, raw_tpm_def, 297 pmact_nil, pmact_decompose, absrep_id] THEN 298 REPEAT CONJ_TAC THENL [ 299 REPEAT GEN_TAC THEN 300 NTAC 2 AP_TERM_TAC THEN CONV_TAC (REWR_CONV EQ_SYM_EQ) THEN 301 REWRITE_TAC [GSYM term_REP_raw_tpm, absrep_id], 302 REPEAT STRIP_TAC THEN 303 AP_TERM_TAC THEN AP_THM_TAC THEN 304 Q.ISPEC_THEN `gtpm` (fn is_pmact_def => 305 Q.ISPEC_THEN `gt_pmact` (fn is_pmact_pmact => 306 is_pmact_def |> C EQ_MP is_pmact_pmact 307 |> CONJUNCTS |> last 308 |> MATCH_MP_TAC) is_pmact_pmact) is_pmact_def THEN 309 POP_ASSUM ACCEPT_TAC 310 ]) 311 val term_REP_tpm = SUBS [GSYM tpm_raw] term_REP_raw_tpm 312 fun tpm_clause {con_termP, con_def} = 313 con_def |> SPEC_ALL 314 |> AP_TERM (mk_comb(tpm_t, pi_t)) 315 |> CONV_RULE (RAND_CONV (REWR_CONV 316 (SUBS [GSYM tpm_raw] raw_tpm_def))) 317 |> REWRITE_RULE [MATCH_MP repabs_pseudo_id con_termP, 318 gtpm_thm, listTheory.MAP, listpm_thm] 319 |> REWRITE_RULE [GSYM con_def, GSYM term_REP_tpm] 320 |> GEN_ALL 321 val tpm_thm = Save_thm(tpm_name ^ "_thm", 322 LIST_CONJ (map tpm_clause cons_info)) 323in 324 {term_REP_tpm = term_REP_tpm, tpm_thm = tpm_thm, t_pmact_t = t_pmact_t, 325 tpm_t = tpm_t} 326end 327 328 329 330 331end (* struct *) 332