7 |
7 |
8 signature QUOTIENT_TERM = |
8 signature QUOTIENT_TERM = |
9 sig |
9 sig |
10 exception LIFT_MATCH of string |
10 exception LIFT_MATCH of string |
11 |
11 |
12 datatype flag = absF | repF |
12 datatype flag = AbsF | RepF |
13 |
13 |
14 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
14 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
15 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
15 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
16 |
16 |
17 (* Allows Nitpick to represent quotient types as single elements from raw type *) |
17 (* Allows Nitpick to represent quotient types as single elements from raw type *) |
39 |
39 |
40 |
40 |
41 (*** Aggregate Rep/Abs Function ***) |
41 (*** Aggregate Rep/Abs Function ***) |
42 |
42 |
43 |
43 |
44 (* The flag repF is for types in negative position; absF is for types |
44 (* The flag RepF is for types in negative position; AbsF is for types |
45 in positive position. Because of this, function types need to be |
45 in positive position. Because of this, function types need to be |
46 treated specially, since there the polarity changes. |
46 treated specially, since there the polarity changes. |
47 *) |
47 *) |
48 |
48 |
49 datatype flag = absF | repF |
49 datatype flag = AbsF | RepF |
50 |
50 |
51 fun negF absF = repF |
51 fun negF AbsF = RepF |
52 | negF repF = absF |
52 | negF RepF = AbsF |
53 |
53 |
54 fun is_identity (Const (@{const_name "id"}, _)) = true |
54 fun is_identity (Const (@{const_name "id"}, _)) = true |
55 | is_identity _ = false |
55 | is_identity _ = false |
56 |
56 |
57 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
57 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
58 |
58 |
59 fun mk_fun_compose flag (trm1, trm2) = |
59 fun mk_fun_compose flag (trm1, trm2) = |
60 case flag of |
60 case flag of |
61 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
61 AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
62 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
62 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
63 |
63 |
64 fun get_mapfun ctxt s = |
64 fun get_mapfun ctxt s = |
65 let |
65 let |
66 val thy = ProofContext.theory_of ctxt |
66 val thy = ProofContext.theory_of ctxt |
67 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
67 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
132 let |
132 let |
133 val thy = ProofContext.theory_of ctxt |
133 val thy = ProofContext.theory_of ctxt |
134 val qty_name = Long_Name.base_name qty_str |
134 val qty_name = Long_Name.base_name qty_str |
135 in |
135 in |
136 case flag of |
136 case flag of |
137 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
137 AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
138 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
138 | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
139 end |
139 end |
140 |
140 |
141 (* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
141 (* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
142 fun absrep_const_chk flag ctxt qty_str = |
142 fun absrep_const_chk flag ctxt qty_str = |
143 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
143 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
618 |
618 |
619 Vars case cannot occur. |
619 Vars case cannot occur. |
620 *) |
620 *) |
621 |
621 |
622 fun mk_repabs ctxt (T, T') trm = |
622 fun mk_repabs ctxt (T, T') trm = |
623 absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm) |
623 absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) |
624 |
624 |
625 fun inj_repabs_err ctxt msg rtrm qtrm = |
625 fun inj_repabs_err ctxt msg rtrm qtrm = |
626 let |
626 let |
627 val rtrm_str = Syntax.string_of_term ctxt rtrm |
627 val rtrm_str = Syntax.string_of_term ctxt rtrm |
628 val qtrm_str = Syntax.string_of_term ctxt qtrm |
628 val qtrm_str = Syntax.string_of_term ctxt qtrm |