equal
deleted
inserted
replaced
1 signature QUOTIENT_TERM = |
1 signature QUOTIENT_TERM = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 datatype flag = absF | repF |
5 datatype flag = absF | repF |
|
6 |
|
7 val absrep_const_chk: flag -> Proof.context -> string -> term |
6 |
8 |
7 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
9 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
8 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
10 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
9 |
11 |
10 val equiv_relation: Proof.context -> typ * typ -> term |
12 val equiv_relation: Proof.context -> typ * typ -> term |
123 in |
125 in |
124 case flag of |
126 case flag of |
125 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
127 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
126 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
128 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
127 end |
129 end |
|
130 |
|
131 fun absrep_const_chk flag ctxt qty_str = |
|
132 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
128 |
133 |
129 fun absrep_match_err ctxt ty_pat ty = |
134 fun absrep_match_err ctxt ty_pat ty = |
130 let |
135 let |
131 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
136 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
132 val ty_str = Syntax.string_of_typ ctxt ty |
137 val ty_str = Syntax.string_of_typ ctxt ty |