67 val { mapper, variances, ... } = lookup tyco; |
70 val { mapper, variances, ... } = lookup tyco; |
68 val args = maps (fn (arg_pattern, (T, T')) => |
71 val args = maps (fn (arg_pattern, (T, T')) => |
69 constructs is_contra arg_pattern T T') |
72 constructs is_contra arg_pattern T T') |
70 (variances ~~ (Ts ~~ Ts')); |
73 (variances ~~ (Ts ~~ Ts')); |
71 val (U, U') = if is_contra then (T', T) else (T, T'); |
74 val (U, U') = if is_contra then (T', T) else (T, T'); |
72 in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end |
75 in list_comb (term_with_typ (ProofContext.init_global thy) (map fastype_of args ---> U --> U') mapper, args) end |
73 | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); |
76 | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); |
74 in construct end; |
77 in construct end; |
75 |
78 |
76 |
79 |
77 (* mapper properties *) |
80 (* mapper properties *) |
|
81 |
|
82 val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss; |
78 |
83 |
79 fun make_comp_prop ctxt variances (tyco, mapper) = |
84 fun make_comp_prop ctxt variances (tyco, mapper) = |
80 let |
85 let |
81 val sorts = map fst variances |
86 val sorts = map fst variances |
82 val (((vs3, vs2), vs1), _) = ctxt |
87 val (((vs3, vs2), vs1), _) = ctxt |
106 if not is_contra then |
111 if not is_contra then |
107 HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) |
112 HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) |
108 else |
113 else |
109 HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) |
114 HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) |
110 ) contras (args21 ~~ args32) |
115 ) contras (args21 ~~ args32) |
111 fun mk_mapper T T' args = list_comb (Const (mapper, |
116 fun mk_mapper T T' args = list_comb (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args); |
112 map fastype_of args ---> T --> T'), args); |
117 val mapper21 = mk_mapper T2 T1 (map Free args21); |
113 val lhs = HOLogic.mk_comp (mk_mapper T2 T1 (map Free args21), mk_mapper T3 T2 (map Free args32)); |
118 val mapper32 = mk_mapper T3 T2 (map Free args32); |
114 val rhs = mk_mapper T3 T1 args31; |
119 val mapper31 = mk_mapper T3 T1 args31; |
115 in fold_rev Logic.all (map Free (args21 @ args32)) ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end; |
120 val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (HOLogic.mk_comp (mapper21, mapper32), mapper31); |
|
121 val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3) |
|
122 val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (mapper21 $ (mapper32 $ x), mapper31 $ x); |
|
123 val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1; |
|
124 val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2; |
|
125 fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop |
|
126 (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]] |
|
127 THEN' Simplifier.asm_lr_simp_tac compositionality_ss |
|
128 THEN_ALL_NEW (Goal.assume_rule_tac ctxt)))); |
|
129 in (comp_prop, prove_compositionality) end; |
|
130 |
|
131 val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss; |
116 |
132 |
117 fun make_id_prop ctxt variances (tyco, mapper) = |
133 fun make_id_prop ctxt variances (tyco, mapper) = |
118 let |
134 let |
119 val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt; |
135 val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt; |
120 val Ts = map TFree vs; |
136 val Ts = map TFree vs; |
121 fun bool_num b = if b then 1 else 0; |
137 fun bool_num b = if b then 1 else 0; |
122 fun mk_argT (T, (_, (co, contra))) = |
138 fun mk_argT (T, (_, (co, contra))) = |
123 replicate (bool_num co + bool_num contra) (T --> T) |
139 replicate (bool_num co + bool_num contra) T |
124 val Ts' = maps mk_argT (Ts ~~ variances) |
140 val arg_Ts = maps mk_argT (Ts ~~ variances) |
125 val T = Type (tyco, Ts); |
141 val T = Type (tyco, Ts); |
126 val lhs = list_comb (Const (mapper, Ts' ---> T --> T), |
142 val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper; |
127 map (HOLogic.id_const o domain_type) Ts'); |
143 val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); |
128 in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end; |
144 val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); |
129 |
145 val rhs = HOLogic.id_const T; |
130 val comp_apply = Simpdata.mk_eq @{thm o_apply}; |
146 val (id_prop, identity_prop) = pairself (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); |
131 val id_def = Simpdata.mk_eq @{thm id_def}; |
147 fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop |
132 |
148 (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss))); |
133 fun make_compositionality ctxt thm = |
149 in (id_prop, prove_identity) end; |
134 let |
|
135 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt; |
|
136 val thm'' = @{thm fun_cong} OF [thm']; |
|
137 val thm''' = |
|
138 (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o Conv.rewr_conv) comp_apply thm''; |
|
139 in singleton (Variable.export ctxt' ctxt) thm''' end; |
|
140 |
|
141 fun args_conv k conv = |
|
142 if k <= 0 then Conv.all_conv |
|
143 else Conv.combination_conv (args_conv (k - 1) conv) conv; |
|
144 |
|
145 fun make_identity ctxt variances thm = |
|
146 let |
|
147 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt; |
|
148 fun bool_num b = if b then 1 else 0; |
|
149 val num_args = Integer.sum |
|
150 (map (fn (_, (co, contra)) => bool_num co + bool_num contra) variances); |
|
151 val thm'' = |
|
152 (Conv.fconv_rule o Conv.arg_conv o Conv.arg1_conv o args_conv num_args o Conv.rewr_conv) id_def thm'; |
|
153 in singleton (Variable.export ctxt' ctxt) thm'' end; |
|
154 |
150 |
155 |
151 |
156 (* analyzing and registering mappers *) |
152 (* analyzing and registering mappers *) |
157 |
153 |
158 fun consume eq x [] = (false, []) |
154 fun consume eq x [] = (false, []) |
175 fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T); |
171 fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T); |
176 val (Ts, T1, T2) = split_mapper_typ tyco T |
172 val (Ts, T1, T2) = split_mapper_typ tyco T |
177 handle List.Empty => bad_typ (); |
173 handle List.Empty => bad_typ (); |
178 val _ = pairself |
174 val _ = pairself |
179 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) |
175 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) |
|
176 handle TYPE _ => bad_typ (); |
180 val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) |
177 val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) |
181 handle TYPE _ => bad_typ (); |
178 handle TYPE _ => bad_typ (); |
182 val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) |
179 val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) |
183 then bad_typ () else (); |
180 then bad_typ () else (); |
184 fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = |
181 fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = |
195 val _ = if null left_variances then () else bad_typ (); |
192 val _ = if null left_variances then () else bad_typ (); |
196 in variances end; |
193 in variances end; |
197 |
194 |
198 fun gen_type_lifting prep_term some_prfx raw_t thy = |
195 fun gen_type_lifting prep_term some_prfx raw_t thy = |
199 let |
196 let |
200 val (mapper, T) = case prep_term thy raw_t |
197 val mapper_fixT = prep_term thy raw_t; |
201 of Const cT => cT |
198 val T = fastype_of mapper_fixT; |
202 | t => error ("No constant: " ^ Syntax.string_of_term_global thy t); |
|
203 val _ = Type.no_tvars T; |
199 val _ = Type.no_tvars T; |
|
200 val mapper = singleton (Variable.polymorphic (ProofContext.init_global thy)) mapper_fixT; |
204 fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
201 fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
205 | add_tycos _ = I; |
202 | add_tycos _ = I; |
206 val tycos = add_tycos T []; |
203 val tycos = add_tycos T []; |
207 val tyco = if tycos = ["fun"] then "fun" |
204 val tyco = if tycos = ["fun"] then "fun" |
208 else case remove (op =) "fun" tycos |
205 else case remove (op =) "fun" tycos |
209 of [tyco] => tyco |
206 of [tyco] => tyco |
210 | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T); |
207 | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T); |
211 val prfx = the_default (Long_Name.base_name tyco) some_prfx; |
208 val prfx = the_default (Long_Name.base_name tyco) some_prfx; |
212 val variances = analyze_variances thy tyco T; |
209 val variances = analyze_variances thy tyco T; |
213 val ctxt = ProofContext.init_global thy; |
210 val ctxt = ProofContext.init_global thy; |
214 val comp_prop = make_comp_prop ctxt variances (tyco, mapper); |
211 val (comp_prop, prove_compositionality) = make_comp_prop ctxt variances (tyco, mapper); |
215 val id_prop = make_id_prop ctxt variances (tyco, mapper); |
212 val (id_prop, prove_identity) = make_id_prop ctxt variances (tyco, mapper); |
|
213 val _ = Thm.cterm_of thy id_prop; |
216 val qualify = Binding.qualify true prfx o Binding.name; |
214 val qualify = Binding.qualify true prfx o Binding.name; |
217 fun after_qed [single_comp, single_id] lthy = |
215 fun after_qed [single_comp_thm, single_id_thm] lthy = |
218 lthy |
216 lthy |
219 |> Local_Theory.note ((qualify compN, []), single_comp) |
217 |> Local_Theory.note ((qualify compN, []), single_comp_thm) |
220 ||>> Local_Theory.note ((qualify idN, []), single_id) |
218 ||>> Local_Theory.note ((qualify idN, []), single_id_thm) |
221 |-> (fn ((_, [comp]), (_, [id])) => fn lthy => |
219 |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy => |
222 lthy |
220 lthy |
223 |> Local_Theory.note ((qualify compositionalityN, []), [make_compositionality lthy comp]) |
221 |> Local_Theory.note ((qualify compositionalityN, []), [prove_compositionality lthy comp_thm]) |
224 |> snd |
222 |> snd |
225 |> Local_Theory.note ((qualify identityN, []), [make_identity lthy variances id]) |
223 |> Local_Theory.note ((qualify identityN, []), [prove_identity lthy id_thm]) |
226 |> snd |
224 |> snd |
227 |> (Local_Theory.background_theory o Data.map) |
225 |> (Local_Theory.background_theory o Data.map) |
228 (Symtab.update (tyco, { mapper = mapper, variances = variances, |
226 (Symtab.update (tyco, { mapper = mapper, variances = variances, |
229 comp = comp, id = id }))); |
227 comp = comp_thm, id = id_thm }))); |
230 in |
228 in |
231 thy |
229 thy |
232 |> Named_Target.theory_init |
230 |> Named_Target.theory_init |
233 |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) |
231 |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) |
234 end |
232 end |