equal
deleted
inserted
replaced
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 |
|
17 (* Allows Nitpick to represent quotient types as single elements from raw type *) |
|
18 val absrep_const_chk: flag -> Proof.context -> string -> term |
16 |
19 |
17 val equiv_relation: Proof.context -> typ * typ -> term |
20 val equiv_relation: Proof.context -> typ * typ -> term |
18 val equiv_relation_chk: Proof.context -> typ * typ -> term |
21 val equiv_relation_chk: Proof.context -> typ * typ -> term |
19 |
22 |
20 val regularize_trm: Proof.context -> term * term -> term |
23 val regularize_trm: Proof.context -> term * term -> term |
130 in |
133 in |
131 case flag of |
134 case flag of |
132 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
135 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
133 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
136 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
134 end |
137 end |
|
138 |
|
139 (* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
|
140 fun absrep_const_chk flag ctxt qty_str = |
|
141 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
135 |
142 |
136 fun absrep_match_err ctxt ty_pat ty = |
143 fun absrep_match_err ctxt ty_pat ty = |
137 let |
144 let |
138 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
145 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
139 val ty_str = Syntax.string_of_typ ctxt ty |
146 val ty_str = Syntax.string_of_typ ctxt ty |