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