equal
deleted
inserted
replaced
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 -> Proof.context -> typ * typ -> term |
5 val get_fun: flag -> Proof.context -> typ * typ -> term |
6 val make_def: mixfix -> Attrib.binding -> term -> term -> |
6 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
7 Proof.context -> (term * thm) * local_theory |
7 Proof.context -> (term * thm) * local_theory |
8 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
8 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
9 local_theory -> local_theory |
9 local_theory -> local_theory |
10 end; |
10 end; |
11 |
11 |
74 then mk_identity qty |
74 then mk_identity qty |
75 else raise (LIFT_MATCH "get_fun") |
75 else raise (LIFT_MATCH "get_fun") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
76 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
77 | _ => raise (LIFT_MATCH "get_fun") |
77 | _ => raise (LIFT_MATCH "get_fun") |
78 |
78 |
79 fun make_def mx attr lhs rhs lthy = |
79 (* interface and syntax setup *) |
|
80 |
|
81 (* the ML-interface takes a 4-tuple consisting of *) |
|
82 (* *) |
|
83 (* - the mixfix annotation *) |
|
84 (* - name and attributes of the meta eq *) |
|
85 (* - the new constant including its type *) |
|
86 (* - the rhs of the definition *) |
|
87 fun quotient_def mx attr lhs rhs lthy = |
80 let |
88 let |
81 val Free (lhs_str, lhs_ty) = lhs; |
89 val Free (lhs_str, lhs_ty) = lhs; |
82 val qconst_bname = Binding.name lhs_str; |
90 val qconst_bname = Binding.name lhs_str; |
83 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
91 val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
84 |> Syntax.check_term lthy |
92 |> Syntax.check_term lthy |
93 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
101 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
94 in |
102 in |
95 ((trm, thm), lthy'') |
103 ((trm, thm), lthy'') |
96 end |
104 end |
97 |
105 |
98 (* interface and syntax setup *) |
106 fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = |
99 |
|
100 (* the ML-interface takes a 5-tuple consisting of *) |
|
101 (* *) |
|
102 (* - the name of the constant to be lifted *) |
|
103 (* - its type *) |
|
104 (* - its mixfix annotation *) |
|
105 (* - a meta-equation defining the constant, *) |
|
106 (* and the attributes of for this meta-equality *) |
|
107 |
|
108 fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = |
|
109 let |
107 let |
110 val lhs = Syntax.read_term lthy lhsstr |
108 val lhs = Syntax.read_term lthy lhsstr |
111 val rhs = Syntax.read_term lthy rhsstr |
109 val rhs = Syntax.read_term lthy rhsstr |
112 in |
110 in |
113 make_def mx attr lhs rhs lthy |> snd |
111 quotient_def mx attr lhs rhs lthy |> snd |
114 end |
112 end |
115 |
113 |
116 val _ = OuterKeyword.keyword "as"; |
114 val _ = OuterKeyword.keyword "as"; |
117 |
115 |
118 val quotdef_parser = |
116 val quotdef_parser = |