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