1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Apr 10 17:48:18 2014 +0200
1.3 @@ -0,0 +1,353 @@
1.4 +(* Title: HOL/Tools/Transfer/transfer_bnf.ML
1.5 + Author: Ondrej Kuncar, TU Muenchen
1.6 +
1.7 +Setup for Transfer for types that are BNF.
1.8 +*)
1.9 +
1.10 +signature TRANSFER_BNF =
1.11 +sig
1.12 + val base_name_of_bnf: BNF_Def.bnf -> binding
1.13 + val type_name_of_bnf: BNF_Def.bnf -> string
1.14 + val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
1.15 + val map_local_theory: (local_theory -> local_theory) -> theory -> theory
1.16 + val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
1.17 +end
1.18 +
1.19 +structure Transfer_BNF : TRANSFER_BNF =
1.20 +struct
1.21 +
1.22 +open BNF_Util
1.23 +open BNF_Def
1.24 +open BNF_FP_Def_Sugar
1.25 +
1.26 +(* util functions *)
1.27 +
1.28 +fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
1.29 +fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
1.30 +
1.31 +fun mk_Domainp P =
1.32 + let
1.33 + val PT = fastype_of P
1.34 + val argT = hd (binder_types PT)
1.35 + in
1.36 + Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
1.37 + end
1.38 +
1.39 +fun mk_pred pred_def args T =
1.40 + let
1.41 + val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
1.42 + |> head_of |> fst o dest_Const
1.43 + val argsT = map fastype_of args
1.44 + in
1.45 + list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
1.46 + end
1.47 +
1.48 +fun mk_eq_onp arg =
1.49 + let
1.50 + val argT = domain_type (fastype_of arg)
1.51 + in
1.52 + Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
1.53 + $ arg
1.54 + end
1.55 +
1.56 +fun subst_conv thm =
1.57 + Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
1.58 +
1.59 +fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
1.60 +
1.61 +fun is_Type (Type _) = true
1.62 + | is_Type _ = false
1.63 +
1.64 +fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global
1.65 +
1.66 +fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
1.67 +
1.68 +fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
1.69 +
1.70 +fun fp_sugar_only_type_ctr f fp_sugar =
1.71 + if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
1.72 +
1.73 +(* relation constraints - bi_total & co. *)
1.74 +
1.75 +fun mk_relation_constraint name arg =
1.76 + (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
1.77 +
1.78 +fun side_constraint_tac bnf constr_defs ctxt i =
1.79 + let
1.80 + val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
1.81 + rel_OO_of_bnf bnf]
1.82 + in
1.83 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
1.84 + THEN_ALL_NEW atac) i
1.85 + end
1.86 +
1.87 +fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
1.88 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
1.89 + CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
1.90 +
1.91 +fun generate_relation_constraint_goal ctxt bnf constraint_def =
1.92 + let
1.93 + val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
1.94 + |> head_of |> fst o dest_Const
1.95 + val live = live_of_bnf bnf
1.96 + val (((As, Bs), Ds), ctxt) = ctxt
1.97 + |> mk_TFrees live
1.98 + ||>> mk_TFrees live
1.99 + ||>> mk_TFrees (dead_of_bnf bnf)
1.100 +
1.101 + val relator = mk_rel_of_bnf Ds As Bs bnf
1.102 + val relsT = map2 mk_pred2T As Bs
1.103 + val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
1.104 + val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
1.105 + val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
1.106 + val goal = Logic.list_implies (assms, concl)
1.107 + in
1.108 + (goal, ctxt)
1.109 + end
1.110 +
1.111 +fun prove_relation_side_constraint ctxt bnf constraint_def =
1.112 + let
1.113 + val old_ctxt = ctxt
1.114 + val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
1.115 + val thm = Goal.prove ctxt [] [] goal
1.116 + (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
1.117 + in
1.118 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
1.119 + end
1.120 +
1.121 +fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
1.122 + let
1.123 + val old_ctxt = ctxt
1.124 + val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
1.125 + val thm = Goal.prove ctxt [] [] goal
1.126 + (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
1.127 + in
1.128 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
1.129 + end
1.130 +
1.131 +val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
1.132 + ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
1.133 +
1.134 +fun prove_relation_constraints bnf lthy =
1.135 + let
1.136 + val transfer_attr = @{attributes [transfer_rule]}
1.137 + val Tname = base_name_of_bnf bnf
1.138 + fun qualify suffix = Binding.qualified true suffix Tname
1.139 +
1.140 + val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
1.141 + val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
1.142 + [snd (nth defs 0), snd (nth defs 1)]
1.143 + val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
1.144 + [snd (nth defs 2), snd (nth defs 3)]
1.145 + val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
1.146 + val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
1.147 + in
1.148 + notes
1.149 + end
1.150 +
1.151 +(* relator_eq *)
1.152 +
1.153 +fun relator_eq bnf =
1.154 + [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
1.155 +
1.156 +(* predicator definition and Domainp and eq_onp theorem *)
1.157 +
1.158 +fun define_pred bnf lthy =
1.159 + let
1.160 + fun mk_pred_name c = Binding.prefix_name "pred_" c
1.161 + val live = live_of_bnf bnf
1.162 + val Tname = base_name_of_bnf bnf
1.163 + val ((As, Ds), lthy) = lthy
1.164 + |> mk_TFrees live
1.165 + ||>> mk_TFrees (dead_of_bnf bnf)
1.166 + val T = mk_T_of_bnf Ds As bnf
1.167 + val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
1.168 + val argTs = map mk_pred1T As
1.169 + val args = mk_Frees_free "P" argTs lthy
1.170 + val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
1.171 + val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
1.172 + val pred_name = mk_pred_name Tname
1.173 + val headT = argTs ---> (T --> HOLogic.boolT)
1.174 + val head = Free (Binding.name_of pred_name, headT)
1.175 + val lhs = list_comb (head, args)
1.176 + val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
1.177 + val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
1.178 + ((Binding.empty, []), def)) lthy
1.179 + in
1.180 + (pred_def, lthy)
1.181 + end
1.182 +
1.183 +fun Domainp_tac bnf pred_def ctxt i =
1.184 + let
1.185 + val n = live_of_bnf bnf
1.186 + val set_map's = set_map_of_bnf bnf
1.187 + in
1.188 + EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
1.189 + in_rel_of_bnf bnf, pred_def]), rtac iffI,
1.190 + REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
1.191 + CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
1.192 + etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
1.193 + hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
1.194 + etac @{thm DomainPI}]) set_map's,
1.195 + REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
1.196 + rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
1.197 + map_id_of_bnf bnf]),
1.198 + REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
1.199 + rtac @{thm fst_conv}]), rtac CollectI,
1.200 + CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
1.201 + REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
1.202 + dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
1.203 + ] i
1.204 + end
1.205 +
1.206 +fun prove_Domainp_rel ctxt bnf pred_def =
1.207 + let
1.208 + val live = live_of_bnf bnf
1.209 + val old_ctxt = ctxt
1.210 + val (((As, Bs), Ds), ctxt) = ctxt
1.211 + |> mk_TFrees live
1.212 + ||>> mk_TFrees live
1.213 + ||>> mk_TFrees (dead_of_bnf bnf)
1.214 +
1.215 + val relator = mk_rel_of_bnf Ds As Bs bnf
1.216 + val relsT = map2 mk_pred2T As Bs
1.217 + val T = mk_T_of_bnf Ds As bnf
1.218 + val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
1.219 + val lhs = mk_Domainp (list_comb (relator, args))
1.220 + val rhs = mk_pred pred_def (map mk_Domainp args) T
1.221 + val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
1.222 + val thm = Goal.prove ctxt [] [] goal
1.223 + (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
1.224 + in
1.225 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
1.226 + end
1.227 +
1.228 +fun pred_eq_onp_tac bnf pred_def ctxt i =
1.229 + (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
1.230 + @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
1.231 + THEN' rtac (rel_Grp_of_bnf bnf)) i
1.232 +
1.233 +fun prove_rel_eq_onp ctxt bnf pred_def =
1.234 + let
1.235 + val live = live_of_bnf bnf
1.236 + val old_ctxt = ctxt
1.237 + val ((As, Ds), ctxt) = ctxt
1.238 + |> mk_TFrees live
1.239 + ||>> mk_TFrees (dead_of_bnf bnf)
1.240 + val T = mk_T_of_bnf Ds As bnf
1.241 + val argTs = map mk_pred1T As
1.242 + val (args, ctxt) = mk_Frees "P" argTs ctxt
1.243 + val relator = mk_rel_of_bnf Ds As As bnf
1.244 + val lhs = list_comb (relator, map mk_eq_onp args)
1.245 + val rhs = mk_eq_onp (mk_pred pred_def args T)
1.246 + val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
1.247 + val thm = Goal.prove ctxt [] [] goal
1.248 + (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
1.249 + in
1.250 + Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
1.251 + end
1.252 +
1.253 +fun predicator bnf lthy =
1.254 + let
1.255 + val (pred_def, lthy) = define_pred bnf lthy
1.256 + val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
1.257 + val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
1.258 + val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
1.259 + fun qualify defname suffix = Binding.qualified true suffix defname
1.260 + val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
1.261 + val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
1.262 + val pred_data = {rel_eq_onp = rel_eq_onp}
1.263 + val type_name = type_name_of_bnf bnf
1.264 + val relator_domain_attr = @{attributes [relator_domain]}
1.265 + val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
1.266 + ((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
1.267 + val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
1.268 + (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) lthy
1.269 + in
1.270 + (notes, lthy)
1.271 + end
1.272 +
1.273 +(* BNF interpretation *)
1.274 +
1.275 +fun transfer_bnf_interpretation bnf lthy =
1.276 + let
1.277 + val constr_notes = if dead_of_bnf bnf > 0 then []
1.278 + else prove_relation_constraints bnf lthy
1.279 + val relator_eq_notes = if dead_of_bnf bnf > 0 then []
1.280 + else relator_eq bnf
1.281 + val (pred_notes, lthy) = predicator bnf lthy
1.282 + in
1.283 + snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
1.284 + end
1.285 +
1.286 +val _ = Context.>> (Context.map_theory (bnf_interpretation
1.287 + (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
1.288 +
1.289 +(* simplification rules for the predicator *)
1.290 +
1.291 +fun lookup_defined_pred_data lthy name =
1.292 + case (Transfer.lookup_pred_data lthy name) of
1.293 + SOME data => data
1.294 + | NONE => (error "lookup_pred_data: something went utterly wrong")
1.295 +
1.296 +fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
1.297 + let
1.298 + val involved_types = distinct op= (
1.299 + map type_name_of_bnf (#nested_bnfs fp_sugar)
1.300 + @ map type_name_of_bnf (#nesting_bnfs fp_sugar)
1.301 + @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
1.302 + val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
1.303 + val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
1.304 + val old_lthy = lthy
1.305 + val (As, lthy) = mk_TFrees live lthy
1.306 + val predTs = map mk_pred1T As
1.307 + val (preds, lthy) = mk_Frees "P" predTs lthy
1.308 + val args = map mk_eq_onp preds
1.309 + val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
1.310 + val cts = map (SOME o certify lthy) args
1.311 + fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
1.312 + fun is_eqn thm = can get_rhs thm
1.313 + fun rel2pred_massage thm =
1.314 + let
1.315 + fun pred_eq_onp_conj 0 = error "not defined"
1.316 + | pred_eq_onp_conj 1 = @{thm eq_onp_same_args}
1.317 + | pred_eq_onp_conj n =
1.318 + let
1.319 + val conj_cong = @{thm arg_cong2[of _ _ _ _ "op \<and>"]}
1.320 + val start = @{thm eq_onp_same_args} RS conj_cong
1.321 + in
1.322 + @{thm eq_onp_same_args} RS (funpow (n - 2) (fn thm => start RS thm) start)
1.323 + end
1.324 + val n = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj |> length else 0
1.325 + in
1.326 + thm
1.327 + |> Drule.instantiate' cTs cts
1.328 + |> Local_Defs.unfold lthy eq_onps
1.329 + |> (fn thm => if n > 0 then @{thm box_equals}
1.330 + OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj n]
1.331 + else thm RS (@{thm eq_onp_same_args} RS iffD1))
1.332 + end
1.333 + val rel_injects = #rel_injects fp_sugar
1.334 + in
1.335 + rel_injects
1.336 + |> map rel2pred_massage
1.337 + |> Variable.export lthy old_lthy
1.338 + |> map Drule.zero_var_indexes
1.339 + end
1.340 +
1.341 +(* fp_sugar interpretation *)
1.342 +
1.343 +fun transfer_fp_sugar_interpretation fp_sugar lthy =
1.344 + let
1.345 + val pred_injects = prove_pred_inject lthy fp_sugar
1.346 + fun qualify defname suffix = Binding.qualified true suffix defname
1.347 + val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
1.348 + val simp_attrs = @{attributes [simp]}
1.349 + in
1.350 + snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
1.351 + end
1.352 +
1.353 +val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
1.354 + (fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
1.355 +
1.356 +end