79 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
79 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
80 | _ => raise (LIFT_MATCH "get_fun") |
80 | _ => raise (LIFT_MATCH "get_fun") |
81 |
81 |
82 fun make_def qconst_bname qty mx attr rhs lthy = |
82 fun make_def qconst_bname qty mx attr rhs lthy = |
83 let |
83 let |
84 val rty = fastype_of rhs |
84 val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs |
85 val (arg_rtys, res_rty) = strip_type rty |
|
86 val (arg_qtys, res_qty) = strip_type qty |
|
87 |
|
88 val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys) |
|
89 val abs_fn = get_fun absF lthy (res_rty, res_qty) |
|
90 |
|
91 fun mk_fun_map t s = |
|
92 Const (@{const_name "fun_map"}, dummyT) $ t $ s |
|
93 |
|
94 val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs) |
|
95 |> Syntax.check_term lthy |
85 |> Syntax.check_term lthy |
96 |
86 |
97 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
87 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
98 |
88 |
99 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
89 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |