src/HOL/Hyperreal/transfer.ML
author huffman
Mon Sep 12 23:06:24 2005 +0200 (2005-09-12 ago)
changeset 17329 72637e062a0d
child 17332 4910cf8c0cd2
permissions -rw-r--r--
new implementation of transfer principle
huffman@17329
     1
signature TRANSFER_TAC =
huffman@17329
     2
sig
huffman@17329
     3
  val transfer_tac: thm list -> int -> tactic
huffman@17329
     4
  val setup: (theory -> theory) list
huffman@17329
     5
end;
huffman@17329
     6
huffman@17329
     7
structure Transfer: TRANSFER_TAC =
huffman@17329
     8
struct
huffman@17329
     9
huffman@17329
    10
(* TODO: make this list extensible *)
huffman@17329
    11
val star_consts =
huffman@17329
    12
  [ "StarType.star_of", "StarType.Ifun"
huffman@17329
    13
  , "StarType.unstar", "StarType.Iset" ]
huffman@17329
    14
huffman@17329
    15
structure TransferData = TheoryDataFun
huffman@17329
    16
(struct
huffman@17329
    17
  val name = "HOL/transfer";
huffman@17329
    18
  type T = {
huffman@17329
    19
    intros: thm list,
huffman@17329
    20
    unfolds: thm list,
huffman@17329
    21
    refolds: thm list,
huffman@17329
    22
    consts: string list
huffman@17329
    23
  };
huffman@17329
    24
  val empty = {intros = [], unfolds = [], refolds = [], consts = star_consts};
huffman@17329
    25
  val copy = I;
huffman@17329
    26
  val extend = I;
huffman@17329
    27
  fun merge _
huffman@17329
    28
    ({intros = intros1, unfolds = unfolds1,
huffman@17329
    29
      refolds = refolds1, consts = consts1},
huffman@17329
    30
     {intros = intros2, unfolds = unfolds2,
huffman@17329
    31
      refolds = refolds2, consts = consts2}) =
huffman@17329
    32
   {intros = Drule.merge_rules (intros1, intros2),
huffman@17329
    33
    unfolds = Drule.merge_rules (unfolds1, unfolds2),
huffman@17329
    34
    refolds = Drule.merge_rules (refolds1, refolds2),
huffman@17329
    35
    consts = merge_lists consts1 consts2};
huffman@17329
    36
  fun print _ _ = ();
huffman@17329
    37
end);
huffman@17329
    38
huffman@17329
    39
val transfer_start = thm "transfer_start"
huffman@17329
    40
huffman@17329
    41
fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
huffman@17329
    42
  | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
huffman@17329
    43
  | unstar_typ T = T
huffman@17329
    44
huffman@17329
    45
fun unstar_term consts term =
huffman@17329
    46
  let
huffman@17329
    47
    fun delete a = exists (fn x => x = a) consts
huffman@17329
    48
    fun unstar (Const(a,T) $ t) = if (delete a) then (unstar t)
huffman@17329
    49
          else (Const(a,unstar_typ T) $ unstar t)
huffman@17329
    50
      | unstar (f $ t) = unstar f $ unstar t
huffman@17329
    51
      | unstar (Const(a,T)) = Const(a,unstar_typ T)
huffman@17329
    52
      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) 
huffman@17329
    53
      | unstar t = t
huffman@17329
    54
  in
huffman@17329
    55
    unstar term
huffman@17329
    56
  end
huffman@17329
    57
huffman@17329
    58
val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
huffman@17329
    59
huffman@17329
    60
fun transfer_thm_of thy ths t =
huffman@17329
    61
  let
huffman@17329
    62
    val {intros,unfolds,refolds,consts} = TransferData.get thy
huffman@17329
    63
    val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t))
huffman@17329
    64
    val u = unstar_term consts t'
huffman@17329
    65
    val ct = cterm_of thy (Logic.mk_equals (t,u))
huffman@17329
    66
    val tacs =
huffman@17329
    67
      [ rewrite_goals_tac atomizers
huffman@17329
    68
      , match_tac [transitive_thm] 1
huffman@17329
    69
      , resolve_tac [transfer_start] 1
huffman@17329
    70
      , REPEAT_ALL_NEW (resolve_tac intros) 1
huffman@17329
    71
      , match_tac [reflexive_thm] 1 ]
huffman@17329
    72
  in
huffman@17329
    73
    prove_goalw_cterm (ths @ refolds @ unfolds) ct (fn _ => tacs)
huffman@17329
    74
  end
huffman@17329
    75
huffman@17329
    76
fun transfer_tac ths =
huffman@17329
    77
    SUBGOAL (fn (t,i) =>
huffman@17329
    78
        (fn th =>
huffman@17329
    79
            let val thy = theory_of_thm th
huffman@17329
    80
                val tr = transfer_thm_of thy ths t
huffman@17329
    81
            in rewrite_goals_tac [tr] th
huffman@17329
    82
            end
huffman@17329
    83
        )
huffman@17329
    84
    )
huffman@17329
    85
huffman@17329
    86
local
huffman@17329
    87
fun map_intros f = TransferData.map
huffman@17329
    88
  (fn {intros,unfolds,refolds,consts} =>
huffman@17329
    89
    {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
huffman@17329
    90
huffman@17329
    91
fun map_unfolds f = TransferData.map
huffman@17329
    92
  (fn {intros,unfolds,refolds,consts} =>
huffman@17329
    93
    {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
huffman@17329
    94
huffman@17329
    95
fun map_refolds f = TransferData.map
huffman@17329
    96
  (fn {intros,unfolds,refolds,consts} =>
huffman@17329
    97
    {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
huffman@17329
    98
huffman@17329
    99
fun map_consts f = TransferData.map
huffman@17329
   100
  (fn {intros,unfolds,refolds,consts} =>
huffman@17329
   101
    {intros=intros, unfolds=unfolds, refolds=refolds, consts=f consts})
huffman@17329
   102
in
huffman@17329
   103
fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm);
huffman@17329
   104
fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm);
huffman@17329
   105
huffman@17329
   106
fun unfold_add_global (thy, thm) = (map_unfolds (Drule.add_rule thm) thy, thm);
huffman@17329
   107
fun unfold_del_global (thy, thm) = (map_unfolds (Drule.del_rule thm) thy, thm);
huffman@17329
   108
huffman@17329
   109
fun refold_add_global (thy, thm) = (map_refolds (Drule.add_rule thm) thy, thm);
huffman@17329
   110
fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm);
huffman@17329
   111
end
huffman@17329
   112
huffman@17329
   113
local
huffman@17329
   114
  val undef_local =
huffman@17329
   115
    Attrib.add_del_args
huffman@17329
   116
      Attrib.undef_local_attribute
huffman@17329
   117
      Attrib.undef_local_attribute;
huffman@17329
   118
in
huffman@17329
   119
  val intro_attr =
huffman@17329
   120
   (Attrib.add_del_args intro_add_global intro_del_global, undef_local);
huffman@17329
   121
  val unfold_attr =
huffman@17329
   122
   (Attrib.add_del_args unfold_add_global unfold_del_global, undef_local);
huffman@17329
   123
  val refold_attr =
huffman@17329
   124
   (Attrib.add_del_args refold_add_global refold_del_global, undef_local);
huffman@17329
   125
end
huffman@17329
   126
huffman@17329
   127
val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
huffman@17329
   128
huffman@17329
   129
val setup =
huffman@17329
   130
  [ TransferData.init
huffman@17329
   131
  , Attrib.add_attributes
huffman@17329
   132
    [ ("transfer_intro", intro_attr, "transfer introduction rule")
huffman@17329
   133
    , ("transfer_unfold", unfold_attr, "transfer unfolding rule")
huffman@17329
   134
    , ("transfer_refold", refold_attr, "transfer refolding rule")
huffman@17329
   135
    ]
huffman@17329
   136
  , Method.add_method
huffman@17329
   137
    ("transfer", Method.thms_args transfer_method, "transfer principle")
huffman@17329
   138
  ];
huffman@17329
   139
huffman@17329
   140
end;