1 |
1 |
2 signature QUOTIENT_DEF = |
2 signature QUOTIENT_DEF = |
3 sig |
3 sig |
4 datatype flag = absF | repF |
4 datatype flag = absF | repF |
5 val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term |
5 val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term |
6 val make_def: binding -> term -> typ -> mixfix -> Attrib.binding -> (typ * typ) list -> |
6 val make_def: binding -> typ -> mixfix -> Attrib.binding -> term -> |
7 Proof.context -> (term * thm) * local_theory |
7 Proof.context -> (term * thm) * local_theory |
8 |
8 |
9 val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) -> |
9 val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) -> |
10 local_theory -> (term * thm) * local_theory |
10 local_theory -> (term * thm) * local_theory |
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
70 end |
70 end |
71 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
71 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
72 | _ => error ("no type variables allowed")) |
72 | _ => error ("no type variables allowed")) |
73 end |
73 end |
74 |
74 |
75 fun make_def nconst_bname rhs qty mx attr qenv lthy = |
|
76 let |
|
77 val (arg_tys, res_ty) = strip_type qty |
|
78 |
|
79 val rep_fns = map (get_fun repF qenv lthy) arg_tys |
|
80 val abs_fn = (get_fun absF qenv lthy) res_ty |
|
81 |
|
82 fun mk_fun_map t s = |
|
83 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
|
84 |
|
85 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
|
86 |> Syntax.check_term lthy |
|
87 in |
|
88 define nconst_bname mx attr absrep_trm lthy |
|
89 end |
|
90 |
|
91 |
|
92 (* returns all subterms where two types differ *) |
75 (* returns all subterms where two types differ *) |
93 fun diff (T, S) Ds = |
76 fun diff (T, S) Ds = |
94 case (T, S) of |
77 case (T, S) of |
95 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
78 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
96 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
79 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
102 | diffs _ _ = error "Unequal length of type arguments" |
85 | diffs _ _ = error "Unequal length of type arguments" |
103 |
86 |
104 |
87 |
105 (* sanity check that the calculated quotient environment |
88 (* sanity check that the calculated quotient environment |
106 matches with the stored quotient environment. *) |
89 matches with the stored quotient environment. *) |
107 fun error_msg lthy (qty, rty) = |
90 fun sanity_chk qenv lthy = |
108 let |
|
109 val qtystr = quote (Syntax.string_of_typ lthy qty) |
|
110 val rtystr = quote (Syntax.string_of_typ lthy rty) |
|
111 in |
|
112 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
|
113 end |
|
114 |
|
115 fun sanity_chk lthy qenv = |
|
116 let |
91 let |
117 val global_qenv = Quotient_Info.mk_qenv lthy |
92 val global_qenv = Quotient_Info.mk_qenv lthy |
118 val thy = ProofContext.theory_of lthy |
93 val thy = ProofContext.theory_of lthy |
|
94 |
|
95 fun error_msg lthy (qty, rty) = |
|
96 let |
|
97 val qtystr = quote (Syntax.string_of_typ lthy qty) |
|
98 val rtystr = quote (Syntax.string_of_typ lthy rty) |
|
99 in |
|
100 error (implode ["Quotient type ", qtystr, " does not match with ", rtystr]) |
|
101 end |
119 |
102 |
120 fun is_inst (qty, rty) (qty', rty') = |
103 fun is_inst (qty, rty) (qty', rty') = |
121 if Sign.typ_instance thy (qty, qty') |
104 if Sign.typ_instance thy (qty, qty') |
122 then let |
105 then let |
123 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
106 val inst = Sign.typ_match thy (qty', qty) Vartab.empty |
132 else error_msg lthy (qty, rty) |
115 else error_msg lthy (qty, rty) |
133 in |
116 in |
134 map chk_inst qenv |
117 map chk_inst qenv |
135 end |
118 end |
136 |
119 |
|
120 fun make_def nconst_bname qty mx attr rhs lthy = |
|
121 let |
|
122 val (arg_tys, res_ty) = strip_type qty |
|
123 |
|
124 val rty = fastype_of rhs |
|
125 val qenv = distinct (op=) (diff (qty, rty) []) |
|
126 |
|
127 val _ = sanity_chk qenv lthy |
|
128 |
|
129 val rep_fns = map (get_fun repF qenv lthy) arg_tys |
|
130 val abs_fn = (get_fun absF qenv lthy) res_ty |
|
131 |
|
132 fun mk_fun_map t s = |
|
133 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
|
134 |
|
135 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
|
136 |> Syntax.check_term lthy |
|
137 in |
|
138 define nconst_bname mx attr absrep_trm lthy |
|
139 end |
|
140 |
|
141 (* interface and syntax setup *) |
|
142 |
|
143 (* the ML-interface takes a 5-tuple consisting of *) |
|
144 (* *) |
|
145 (* - the name of the constant to be lifted *) |
|
146 (* - its type *) |
|
147 (* - its mixfix annotation *) |
|
148 (* - a meta-equation defining the constant, *) |
|
149 (* and the attributes of for this meta-equality *) |
137 |
150 |
138 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
151 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
139 let |
152 let |
140 val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop |
153 val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop |
141 val (_, rhs) = PrimitiveDefs.abs_def prop' |
154 val (_, rhs) = PrimitiveDefs.abs_def prop' |
142 |
|
143 val rty = fastype_of rhs |
|
144 val qenv = distinct (op=) (diff (qty, rty) []) |
|
145 in |
155 in |
146 sanity_chk lthy qenv; |
156 make_def bind qty mx attr rhs lthy |
147 make_def bind rhs qty mx attr qenv lthy |
|
148 end |
157 end |
149 |
158 |
150 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
159 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
151 let |
160 let |
152 val qty = Syntax.read_typ lthy qtystr |
161 val qty = Syntax.read_typ lthy qtystr |