1structure newtypeTools :> newtypeTools = 2struct 3 4open Abbrev HolKernel boolLib 5 6infixr 6 /\ 7infixr 5 ==> 8infix 9 == 9fun t1 /\ t2 = mk_conj(t1, t2) 10fun t1 ==> t2 = mk_imp (t1,t2) 11fun t1 == t2 = mk_eq(t1,t2) 12 13 14fun rich_new_type (tyname, exthm) = let 15 val bij_ax = new_type_definition(tyname, exthm) 16 val (termP, oldty) = let 17 val (bvar, exthm_body) = exthm |> concl |> dest_exists 18 in 19 (rator exthm_body, type_of bvar) 20 end 21 fun termPf x = mk_comb(termP, x) 22 val oldty = exthm |> concl |> dest_exists |> #1 |> type_of 23 val x = mk_var("x", oldty) and y = mk_var("y", oldty) 24 val newty = bij_ax |> concl |> dest_exists |> #1 |> type_of |> dom_rng |> #1 25 val term_ABSREP = 26 define_new_type_bijections { ABS = tyname ^ "_ABS", REP = tyname ^ "_REP", 27 name = tyname ^ "_ABSREP", tyax = bij_ax} 28 val absrep_id = term_ABSREP |> CONJUNCT1 29 val (term_ABS_t, term_REP_t) = let 30 val eqn1_lhs = absrep_id|> concl |> strip_forall |> #2 |> lhs 31 val (a, x) = dest_comb eqn1_lhs 32 in 33 (a, rator x) 34 end 35 fun term_ABSf x = mk_comb(term_ABS_t, x) 36 fun term_REPf x = mk_comb(term_REP_t, x) 37 val g = mk_var("g", newty) and h = mk_var("h", newty) 38 val term_ABS_pseudo11 = prove( 39 termPf x /\ termPf y ==> (term_ABSf x == term_ABSf y) == (x == y), 40 STRIP_TAC THEN EQ_TAC THENL [ 41 ALL_TAC, DISCH_THEN SUBST1_TAC THEN REFL_TAC] THEN 42 DISCH_THEN (MP_TAC o AP_TERM term_REP_t) THEN 43 REPEAT (POP_ASSUM (SUBST1_TAC o 44 CONV_RULE (REWR_CONV (CONJUNCT2 term_ABSREP)))) THEN 45 REWRITE_TAC []) 46 val term_REP_11 = prove( 47 (term_REPf g == term_REPf h) == (g == h), 48 EQ_TAC THENL [ALL_TAC, DISCH_THEN SUBST1_TAC THEN REFL_TAC] THEN 49 DISCH_THEN (MP_TAC o AP_TERM term_ABS_t) THEN REWRITE_TAC [absrep_id]) 50 val termP_term_REP = prove( 51 termPf (term_REPf g), 52 CONV_TAC (REWR_CONV (CONJUNCT2 term_ABSREP) THENC 53 LAND_CONV (RAND_CONV (REWR_CONV absrep_id))) THEN 54 REFL_TAC) 55 val termP_exists = prove( 56 termPf x == mk_exists(g, x == term_REPf g), 57 EQ_TAC THENL [ 58 REWRITE_TAC [CONJUNCT2 term_ABSREP] THEN 59 DISCH_THEN (SUBST1_TAC o SYM) THEN 60 EXISTS_TAC (term_ABSf x) THEN REFL_TAC, 61 DISCH_THEN (X_CHOOSE_THEN g SUBST1_TAC) THEN 62 CONV_TAC (REWR_CONV (EQT_INTRO termP_term_REP)) 63 ]) 64 val repabs_pseudo_id = 65 term_ABSREP |> CONJUNCT2 |> SPEC_ALL |> EQ_IMP_RULE |> #1 |> GEN_ALL 66in 67 {term_ABS_pseudo11 = term_ABS_pseudo11, 68 term_REP_11 = term_REP_11, repabs_pseudo_id = repabs_pseudo_id, 69 absrep_id = absrep_id, 70 termP_term_REP = termP_term_REP, 71 termP_exists = termP_exists, 72 newty = newty, 73 termP = termP, 74 term_REP_t = term_REP_t, term_ABS_t = term_ABS_t} 75end 76 77 78end (* struct *) 79