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