diff -r 2bce9a690b1e -r 530112e8c6ba src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Nov 18 16:19:57 2014 +0100 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Nov 18 16:19:57 2014 +0100 @@ -8,9 +8,12 @@ signature TRANSFER = sig type pred_data + val mk_pred_data: thm -> thm -> thm list -> pred_data val rel_eq_onp: pred_data -> thm val rel_eq_onp_with_tops: pred_data -> thm val pred_def: pred_data -> thm + val pred_simps: pred_data -> thm list + val update_pred_simps: thm list -> pred_data -> pred_data val bottom_rewr_conv: thm list -> conv val top_rewr_conv: thm list -> conv @@ -59,13 +62,23 @@ val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of); -type pred_data = {pred_def:thm, rel_eq_onp: thm} +datatype pred_data = PRED_DATA of {pred_def:thm, rel_eq_onp: thm, pred_simps: thm list} + +fun mk_pred_data pred_def rel_eq_onp pred_simps = PRED_DATA {pred_def = pred_def, + rel_eq_onp = rel_eq_onp, pred_simps = pred_simps} + +fun map_pred_data' f1 f2 f3 (PRED_DATA {pred_def, rel_eq_onp, pred_simps}) = + PRED_DATA {pred_def = f1 pred_def, rel_eq_onp = f2 rel_eq_onp, pred_simps = f3 pred_simps} -val rel_eq_onp: pred_data -> thm = #rel_eq_onp -val rel_eq_onp_with_tops: pred_data -> thm = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv +fun rep_pred_data (PRED_DATA p) = p +val rel_eq_onp = #rel_eq_onp o rep_pred_data +val rel_eq_onp_with_tops = (Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))) - o #rel_eq_onp -val pred_def: pred_data -> thm = #pred_def + o #rel_eq_onp o rep_pred_data +val pred_def = #pred_def o rep_pred_data +val pred_simps = #pred_simps o rep_pred_data +fun update_pred_simps new_pred_data = map_pred_data' I I (K new_pred_data) + structure Data = Generic_Data ( @@ -796,9 +809,12 @@ val untransferred_attribute_parser = Attrib.thms >> untransferred_attribute -fun morph_pred_data phi {pred_def, rel_eq_onp} = - {pred_def = Morphism.thm phi pred_def, - rel_eq_onp = Morphism.thm phi rel_eq_onp} +fun morph_pred_data phi = + let + val morph_thm = Morphism.thm phi + in + map_pred_data' morph_thm morph_thm (map morph_thm) + end fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))