28 (* Generation of the code certificate from the rsp theorem *) |
28 (* Generation of the code certificate from the rsp theorem *) |
29 |
29 |
30 open Lifting_Util |
30 open Lifting_Util |
31 |
31 |
32 infix 0 MRSL |
32 infix 0 MRSL |
33 |
|
34 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) |
|
35 | get_body_types (U, V) = (U, V) |
|
36 |
|
37 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) |
|
38 | get_binder_types _ = [] |
|
39 |
|
40 fun unabs_def ctxt def = |
|
41 let |
|
42 val (_, rhs) = Thm.dest_equals (cprop_of def) |
|
43 fun dest_abs (Abs (var_name, T, _)) = (var_name, T) |
|
44 | dest_abs tm = raise TERM("get_abs_var",[tm]) |
|
45 val (var_name, T) = dest_abs (term_of rhs) |
|
46 val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt |
|
47 val thy = Proof_Context.theory_of ctxt' |
|
48 val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T))) |
|
49 in |
|
50 Thm.combination def refl_thm |> |
|
51 singleton (Proof_Context.export ctxt' ctxt) |
|
52 end |
|
53 |
|
54 fun unabs_all_def ctxt def = |
|
55 let |
|
56 val (_, rhs) = Thm.dest_equals (cprop_of def) |
|
57 val xs = strip_abs_vars (term_of rhs) |
|
58 in |
|
59 fold (K (unabs_def ctxt)) xs def |
|
60 end |
|
61 |
|
62 val map_fun_unfolded = |
|
63 @{thm map_fun_def[abs_def]} |> |
|
64 unabs_def @{context} |> |
|
65 unabs_def @{context} |> |
|
66 Local_Defs.unfold @{context} [@{thm comp_def}] |
|
67 |
|
68 fun unfold_fun_maps ctm = |
|
69 let |
|
70 fun unfold_conv ctm = |
|
71 case (Thm.term_of ctm) of |
|
72 Const (@{const_name "map_fun"}, _) $ _ $ _ => |
|
73 (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm |
|
74 | _ => Conv.all_conv ctm |
|
75 val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) |
|
76 in |
|
77 (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm |
|
78 end |
|
79 |
|
80 fun prove_rel ctxt rsp_thm (rty, qty) = |
|
81 let |
|
82 val ty_args = get_binder_types (rty, qty) |
|
83 fun disch_arg args_ty thm = |
|
84 let |
|
85 val quot_thm = Quotient_Term.prove_quot_thm ctxt args_ty |
|
86 in |
|
87 [quot_thm, thm] MRSL @{thm apply_rspQ3''} |
|
88 end |
|
89 in |
|
90 fold disch_arg ty_args rsp_thm |
|
91 end |
|
92 |
|
93 exception CODE_CERT_GEN of string |
|
94 |
|
95 fun simplify_code_eq ctxt def_thm = |
|
96 Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm |
|
97 |
|
98 fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = |
|
99 let |
|
100 val quot_thm = Quotient_Term.prove_quot_thm ctxt (get_body_types (rty, qty)) |
|
101 val fun_rel = prove_rel ctxt rsp_thm (rty, qty) |
|
102 val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs} |
|
103 val abs_rep_eq = |
|
104 case (HOLogic.dest_Trueprop o prop_of) fun_rel of |
|
105 Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm |
|
106 | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} |
|
107 | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" |
|
108 val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm |
|
109 val unabs_def = unabs_all_def ctxt unfolded_def |
|
110 val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm |
|
111 val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} |
|
112 val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong} |
|
113 val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans} |
|
114 in |
|
115 simplify_code_eq ctxt code_cert |
|
116 end |
|
117 |
|
118 fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = |
|
119 let |
|
120 val quot_thm = Quotient_Term.prove_quot_thm lthy (get_body_types (rty, qty)) |
|
121 in |
|
122 if Quotient_Type.can_generate_code_cert quot_thm then |
|
123 let |
|
124 val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty) |
|
125 val add_abs_eqn_attribute = |
|
126 Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) |
|
127 val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); |
|
128 in |
|
129 lthy |
|
130 |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert]) |
|
131 end |
|
132 else |
|
133 lthy |
|
134 end |
|
135 |
|
136 fun define_code_eq code_eqn_thm_name def_thm lthy = |
|
137 let |
|
138 val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm |
|
139 val code_eq = unabs_all_def lthy unfolded_def |
|
140 val simp_code_eq = simplify_code_eq lthy code_eq |
|
141 in |
|
142 lthy |
|
143 |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) |
|
144 end |
|
145 |
|
146 fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = |
|
147 if body_type rty = body_type qty then |
|
148 define_code_eq code_eqn_thm_name def_thm lthy |
|
149 else |
|
150 define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy |
|
151 |
33 |
152 (* The ML-interface for a quotient definition takes |
34 (* The ML-interface for a quotient definition takes |
153 as argument: |
35 as argument: |
154 |
36 |
155 - an optional binding and mixfix annotation |
37 - an optional binding and mixfix annotation |