380 fun mk_type typ = typ |> Logic.mk_type |> cterm_of thy |> Drule.mk_term |
380 fun mk_type typ = typ |> Logic.mk_type |> cterm_of thy |> Drule.mk_term |
381 in |
381 in |
382 Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty] |
382 Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty] |
383 end |
383 end |
384 |
384 |
|
385 exception DECODE |
|
386 |
385 fun decode_code_eq thm = |
387 fun decode_code_eq thm = |
386 let |
388 if nprems_of thm > 0 then raise DECODE |
387 val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm |
389 else |
388 val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq |
390 let |
389 fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type |
391 val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm |
390 in |
392 val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq |
391 (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) |
393 fun dest_type typ = typ |> Drule.dest_term |> term_of |> Logic.dest_type |
392 end |
394 in |
|
395 (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) |
|
396 end |
393 |
397 |
394 fun register_encoded_code_eq thm thy = |
398 fun register_encoded_code_eq thm thy = |
395 let |
399 let |
396 val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm |
400 val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm |
397 in |
401 in |
398 register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy |
402 register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy |
399 end |
403 end |
|
404 handle DECODE => thy |
400 |
405 |
401 val register_code_eq_attribute = Thm.declaration_attribute |
406 val register_code_eq_attribute = Thm.declaration_attribute |
402 (fn thm => Context.mapping (register_encoded_code_eq thm) I) |
407 (fn thm => Context.mapping (register_encoded_code_eq thm) I) |
403 val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute) |
408 val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute) |
404 |
409 |