1(* Title: HOL/Tools/Transfer/transfer_bnf.ML 2 Author: Ondrej Kuncar, TU Muenchen 3 4Setup for Transfer for types that are BNF. 5*) 6 7signature TRANSFER_BNF = 8sig 9 exception NO_PRED_DATA of unit 10 11 val base_name_of_bnf: BNF_Def.bnf -> binding 12 val type_name_of_bnf: BNF_Def.bnf -> string 13 val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data 14 val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a 15end 16 17structure Transfer_BNF : TRANSFER_BNF = 18struct 19 20open BNF_Util 21open BNF_Def 22open BNF_FP_Util 23open BNF_FP_Def_Sugar 24 25exception NO_PRED_DATA of unit 26 27(* util functions *) 28 29fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf)) 30 31fun mk_Domainp P = 32 let 33 val PT = fastype_of P 34 val argT = hd (binder_types PT) 35 in 36 Const (\<^const_name>\<open>Domainp\<close>, PT --> argT --> HOLogic.boolT) $ P 37 end 38 39fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst 40 41fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I 42 43fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar) 44 45fun fp_sugar_only_type_ctr f fp_sugars = 46 (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of 47 [] => I 48 | fp_sugars' => f fp_sugars') 49 50(* relation constraints - bi_total & co. *) 51 52fun mk_relation_constraint name arg = 53 (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg 54 55fun side_constraint_tac bnf constr_defs ctxt = 56 let 57 val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf, 58 rel_OO_of_bnf bnf] 59 in 60 SELECT_GOAL (Local_Defs.unfold0_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf) 61 THEN_ALL_NEW assume_tac ctxt 62 end 63 64fun bi_constraint_tac constr_iff sided_constr_intros ctxt = 65 SELECT_GOAL (Local_Defs.unfold0_tac ctxt [constr_iff]) THEN' 66 CONJ_WRAP' (fn thm => rtac ctxt thm THEN_ALL_NEW 67 (REPEAT_DETERM o etac ctxt conjE THEN' assume_tac ctxt)) sided_constr_intros 68 69fun generate_relation_constraint_goal ctxt bnf constraint_def = 70 let 71 val constr_name = 72 constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq 73 |> head_of |> fst o dest_Const 74 val live = live_of_bnf bnf 75 val (((As, Bs), Ds), ctxt') = ctxt 76 |> mk_TFrees live 77 ||>> mk_TFrees live 78 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) 79 80 val relator = mk_rel_of_bnf Ds As Bs bnf 81 val relsT = map2 mk_pred2T As Bs 82 val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' 83 val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args))) 84 val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args 85 val goal = Logic.list_implies (assms, concl) 86 in 87 (goal, ctxt'') 88 end 89 90fun prove_relation_side_constraint ctxt bnf constraint_def = 91 let 92 val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def 93 in 94 Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => 95 side_constraint_tac bnf [constraint_def] goal_ctxt 1) 96 |> Thm.close_derivation \<^here> 97 |> singleton (Variable.export ctxt' ctxt) 98 |> Drule.zero_var_indexes 99 end 100 101fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints = 102 let 103 val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def 104 in 105 Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => 106 bi_constraint_tac constraint_def side_constraints goal_ctxt 1) 107 |> Thm.close_derivation \<^here> 108 |> singleton (Variable.export ctxt' ctxt) 109 |> Drule.zero_var_indexes 110 end 111 112val defs = 113 [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), 114 ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})] 115 116fun prove_relation_constraints bnf ctxt = 117 let 118 val transfer_attr = @{attributes [transfer_rule]} 119 val Tname = base_name_of_bnf bnf 120 121 val defs = map (apsnd (prove_relation_side_constraint ctxt bnf)) defs 122 val bi_total = prove_relation_bi_constraint ctxt bnf @{thm bi_total_alt_def} 123 [snd (nth defs 0), snd (nth defs 1)] 124 val bi_unique = prove_relation_bi_constraint ctxt bnf @{thm bi_unique_alt_def} 125 [snd (nth defs 2), snd (nth defs 3)] 126 val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs 127 in 128 maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs 129 end 130 131(* relator_eq *) 132 133fun relator_eq bnf = 134 [(Binding.empty_atts, [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])] 135 136(* transfer rules *) 137 138fun bnf_transfer_rules bnf = 139 let 140 val transfer_rules = map_transfer_of_bnf bnf :: pred_transfer_of_bnf bnf 141 :: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf 142 val transfer_attr = @{attributes [transfer_rule]} 143 in 144 map (fn thm => (Binding.empty_atts, [([thm],transfer_attr)])) transfer_rules 145 end 146 147(* Domainp theorem for predicator *) 148 149fun Domainp_tac bnf pred_def ctxt = 150 let 151 val n = live_of_bnf bnf 152 val set_map's = set_map_of_bnf bnf 153 in 154 EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Domainp.simps}, 155 in_rel_of_bnf bnf, pred_def]), rtac ctxt iffI, 156 REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt, 157 CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt ballI, dtac ctxt (set_map RS equalityD1 RS set_mp), 158 etac ctxt imageE, dtac ctxt set_rev_mp, assume_tac ctxt, 159 REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm case_prodE}], 160 hyp_subst_tac ctxt, rtac ctxt @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, 161 etac ctxt @{thm DomainPI}]) set_map's, 162 REPEAT_DETERM o etac ctxt conjE, 163 REPEAT_DETERM o resolve_tac ctxt [exI, (refl RS conjI), rotate_prems 1 conjI], 164 rtac ctxt refl, rtac ctxt (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym, 165 map_id_of_bnf bnf]), 166 REPEAT_DETERM_N n o (EVERY' [rtac ctxt @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]}, 167 rtac ctxt @{thm fst_conv}]), rtac ctxt CollectI, 168 CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt (set_map RS @{thm ord_eq_le_trans}), 169 REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}], 170 dtac ctxt (rotate_prems 1 bspec), assume_tac ctxt, 171 etac ctxt @{thm DomainpE}, etac ctxt @{thm someI}]) set_map's 172 ] 173 end 174 175fun prove_Domainp_rel ctxt bnf pred_def = 176 let 177 val live = live_of_bnf bnf 178 val (((As, Bs), Ds), ctxt') = ctxt 179 |> mk_TFrees live 180 ||>> mk_TFrees live 181 ||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) 182 183 val relator = mk_rel_of_bnf Ds As Bs bnf 184 val relsT = map2 mk_pred2T As Bs 185 val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' 186 val lhs = mk_Domainp (list_comb (relator, args)) 187 val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args) 188 val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop 189 in 190 Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} => 191 Domainp_tac bnf pred_def goal_ctxt 1) 192 |> Thm.close_derivation \<^here> 193 |> singleton (Variable.export ctxt'' ctxt) 194 |> Drule.zero_var_indexes 195 end 196 197fun predicator bnf lthy = 198 let 199 val pred_def = pred_set_of_bnf bnf 200 val Domainp_rel = prove_Domainp_rel lthy bnf pred_def 201 val rel_eq_onp = rel_eq_onp_of_bnf bnf 202 val Domainp_rel_thm_name = Binding.qualify_name true (base_name_of_bnf bnf) "Domainp_rel" 203 val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp [] 204 val type_name = type_name_of_bnf bnf 205 val relator_domain_attr = @{attributes [relator_domain]} 206 val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)])] 207 in 208 lthy 209 |> Local_Theory.notes notes 210 |> snd 211 |> Local_Theory.declaration {syntax = false, pervasive = true} 212 (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) 213 end 214 215(* BNF interpretation *) 216 217fun transfer_bnf_interpretation bnf lthy = 218 let 219 val dead = dead_of_bnf bnf 220 val constr_notes = if dead > 0 then [] else prove_relation_constraints bnf lthy 221 val relator_eq_notes = if dead > 0 then [] else relator_eq bnf 222 val transfer_rule_notes = if dead > 0 then [] else bnf_transfer_rules bnf 223 in 224 lthy 225 |> Local_Theory.notes (constr_notes @ relator_eq_notes @ transfer_rule_notes) 226 |> snd 227 |> predicator bnf 228 end 229 230val _ = 231 Theory.setup 232 (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation)) 233 234(* simplification rules for the predicator *) 235 236fun lookup_defined_pred_data ctxt name = 237 case Transfer.lookup_pred_data ctxt name of 238 SOME data => data 239 | NONE => raise NO_PRED_DATA () 240 241 242(* fp_sugar interpretation *) 243 244fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = 245 let 246 val fp_ctr_sugar = #fp_ctr_sugar fp_sugar 247 val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar 248 @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar 249 @ these (Option.map #co_rec_transfers (#fp_co_induct_sugar fp_sugar)) 250 val transfer_attr = @{attributes [transfer_rule]} 251 in 252 map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules 253 end 254 255fun register_pred_injects fp_sugar lthy = 256 let 257 val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar) 258 val type_name = type_name_of_bnf (#fp_bnf fp_sugar) 259 val pred_data = lookup_defined_pred_data lthy type_name 260 |> Transfer.update_pred_simps pred_injects 261 in 262 lthy 263 |> Local_Theory.declaration {syntax = false, pervasive = true} 264 (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) 265 end 266 267fun transfer_fp_sugars_interpretation fp_sugar lthy = 268 let 269 val lthy = register_pred_injects fp_sugar lthy 270 val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar 271 in 272 lthy 273 |> Local_Theory.notes transfer_rules_notes 274 |> snd 275 end 276 277val _ = 278 Theory.setup (fp_sugars_interpretation transfer_plugin 279 (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation))) 280 281end 282