1(* Title: HOL/Nonstandard_Analysis/transfer_principle.ML 2 Author: Brian Huffman 3 4Transfer principle tactic for nonstandard analysis. 5*) 6 7signature TRANSFER_PRINCIPLE = 8sig 9 val transfer_tac: Proof.context -> thm list -> int -> tactic 10 val add_const: string -> theory -> theory 11end; 12 13structure Transfer_Principle: TRANSFER_PRINCIPLE = 14struct 15 16structure Data = Generic_Data 17( 18 type T = { 19 intros: thm list, 20 unfolds: thm list, 21 refolds: thm list, 22 consts: string list 23 }; 24 val empty = {intros = [], unfolds = [], refolds = [], consts = []}; 25 val extend = I; 26 fun merge 27 ({intros = intros1, unfolds = unfolds1, 28 refolds = refolds1, consts = consts1}, 29 {intros = intros2, unfolds = unfolds2, 30 refolds = refolds2, consts = consts2}) : T = 31 {intros = Thm.merge_thms (intros1, intros2), 32 unfolds = Thm.merge_thms (unfolds1, unfolds2), 33 refolds = Thm.merge_thms (refolds1, refolds2), 34 consts = Library.merge (op =) (consts1, consts2)}; 35); 36 37fun unstar_typ (Type (\<^type_name>\<open>star\<close>, [t])) = unstar_typ t 38 | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) 39 | unstar_typ T = T 40 41fun unstar_term consts term = 42 let 43 fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t) 44 else (Const(a,unstar_typ T) $ unstar t) 45 | unstar (f $ t) = unstar f $ unstar t 46 | unstar (Const(a,T)) = Const(a,unstar_typ T) 47 | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) 48 | unstar t = t 49 in 50 unstar term 51 end 52 53local exception MATCH 54in 55fun transfer_star_tac ctxt = 56 let 57 fun thm_of (Const (\<^const_name>\<open>Ifun\<close>, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u] 58 | thm_of (Const (\<^const_name>\<open>star_of\<close>, _) $ _) = @{thm star_of_def} 59 | thm_of (Const (\<^const_name>\<open>star_n\<close>, _) $ _) = @{thm Pure.reflexive} 60 | thm_of _ = raise MATCH; 61 62 fun thm_of_goal (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ (Const (\<^const_name>\<open>star_n\<close>, _) $ _)) = 63 thm_of t 64 | thm_of_goal _ = raise MATCH; 65 in 66 SUBGOAL (fn (t, i) => 67 resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i 68 handle MATCH => no_tac) 69 end; 70end; 71 72fun transfer_thm_of ctxt ths t = 73 let 74 val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt); 75 val meta = Local_Defs.meta_rewrite_rule ctxt; 76 val ths' = map meta ths; 77 val unfolds' = map meta unfolds and refolds' = map meta refolds; 78 val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t)) 79 val u = unstar_term consts t' 80 val tac = 81 rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN 82 ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN 83 match_tac ctxt [transitive_thm] 1 THEN 84 resolve_tac ctxt [@{thm transfer_start}] 1 THEN 85 REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN 86 match_tac ctxt [reflexive_thm] 1 87 in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end; 88 89fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th => 90 let 91 val tr = transfer_thm_of ctxt ths t 92 val (_$ l $ r) = Thm.concl_of tr; 93 val trs = if l aconv r then [] else [tr]; 94 in rewrite_goals_tac ctxt trs th end)); 95 96local 97 98fun map_intros f = Data.map 99 (fn {intros,unfolds,refolds,consts} => 100 {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts}) 101 102fun map_unfolds f = Data.map 103 (fn {intros,unfolds,refolds,consts} => 104 {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts}) 105 106fun map_refolds f = Data.map 107 (fn {intros,unfolds,refolds,consts} => 108 {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) 109in 110 111val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm o Thm.trim_context); 112val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm); 113 114val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm o Thm.trim_context); 115val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm); 116 117val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm o Thm.trim_context); 118val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm); 119 120end 121 122fun add_const c = Context.theory_map (Data.map 123 (fn {intros,unfolds,refolds,consts} => 124 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) 125 126val _ = 127 Theory.setup 128 (Attrib.setup \<^binding>\<open>transfer_intro\<close> (Attrib.add_del intro_add intro_del) 129 "declaration of transfer introduction rule" #> 130 Attrib.setup \<^binding>\<open>transfer_unfold\<close> (Attrib.add_del unfold_add unfold_del) 131 "declaration of transfer unfolding rule" #> 132 Attrib.setup \<^binding>\<open>transfer_refold\<close> (Attrib.add_del refold_add refold_del) 133 "declaration of transfer refolding rule") 134 135end; 136