src/HOL/Hyperreal/transfer.ML
author wenzelm
Sat, 21 Jan 2006 23:02:20 +0100
changeset 18729 216e31270509
parent 18708 4b3dadb4fe33
child 19734 e9a06ce3a97a
permissions -rw-r--r--
simplified type attribute; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17333
605c97701833 add header
huffman
parents: 17332
diff changeset
     1
(*  Title       : HOL/Hyperreal/transfer.ML
605c97701833 add header
huffman
parents: 17332
diff changeset
     2
    ID          : $Id$
605c97701833 add header
huffman
parents: 17332
diff changeset
     3
    Author      : Brian Huffman
605c97701833 add header
huffman
parents: 17332
diff changeset
     4
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
     5
Transfer principle tactic for nonstandard analysis.
17333
605c97701833 add header
huffman
parents: 17332
diff changeset
     6
*)
605c97701833 add header
huffman
parents: 17332
diff changeset
     7
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
     8
signature TRANSFER =
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
     9
sig
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    10
  val transfer_tac: Proof.context -> thm list -> int -> tactic
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17333
diff changeset
    11
  val add_const: string -> theory -> theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
    12
  val setup: theory -> theory
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    13
end;
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    14
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    15
structure Transfer: TRANSFER =
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    16
struct
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    17
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    18
structure TransferData = GenericDataFun
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    19
(struct
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    20
  val name = "HOL/transfer";
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    21
  type T = {
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    22
    intros: thm list,
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    23
    unfolds: thm list,
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    24
    refolds: thm list,
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    25
    consts: string list
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    26
  };
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17333
diff changeset
    27
  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    28
  val extend = I;
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    29
  fun merge _
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    30
    ({intros = intros1, unfolds = unfolds1,
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    31
      refolds = refolds1, consts = consts1},
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    32
     {intros = intros2, unfolds = unfolds2,
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    33
      refolds = refolds2, consts = consts2}) =
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    34
   {intros = Drule.merge_rules (intros1, intros2),
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    35
    unfolds = Drule.merge_rules (unfolds1, unfolds2),
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    36
    refolds = Drule.merge_rules (refolds1, refolds2),
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    37
    consts = merge_lists consts1 consts2};
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    38
  fun print _ _ = ();
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    39
end);
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    40
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    41
val transfer_start = thm "transfer_start"
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    42
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17333
diff changeset
    43
fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    44
  | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    45
  | unstar_typ T = T
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    46
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    47
fun unstar_term consts term =
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    48
  let
17432
835647238122 use mem operator
huffman
parents: 17429
diff changeset
    49
    fun unstar (Const(a,T) $ t) = if (a mem consts) then (unstar t)
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    50
          else (Const(a,unstar_typ T) $ unstar t)
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    51
      | unstar (f $ t) = unstar f $ unstar t
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    52
      | unstar (Const(a,T)) = Const(a,unstar_typ T)
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    53
      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t) 
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    54
      | unstar t = t
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    55
  in
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    56
    unstar term
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    57
  end
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    58
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    59
val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    60
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    61
fun transfer_thm_of ctxt ths t =
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    62
  let
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    63
    val thy = ProofContext.theory_of ctxt;
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    64
    val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    65
    val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t))
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    66
    val u = unstar_term consts t'
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    67
    val tac =
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    68
      rewrite_goals_tac (ths @ refolds @ unfolds) THEN
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    69
      rewrite_goals_tac atomizers THEN
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    70
      match_tac [transitive_thm] 1 THEN
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    71
      resolve_tac [transfer_start] 1 THEN
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    72
      REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    73
      match_tac [reflexive_thm] 1
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    74
  in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (K tac) end
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    75
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    76
fun transfer_tac ctxt ths =
17329
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 =>
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    79
            let val tr = transfer_thm_of ctxt ths t
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    80
            in rewrite_goals_tac [tr] th end))
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    81
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    82
local
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    83
fun map_intros f = TransferData.map
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    84
  (fn {intros,unfolds,refolds,consts} =>
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    85
    {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    86
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    87
fun map_unfolds 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=intros, unfolds=f 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_refolds 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=unfolds, refolds=f refolds, consts=consts})
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    94
in
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    95
val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule);
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    96
val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule);
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
    97
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    98
val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule);
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    99
val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule);
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   100
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   101
val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule);
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   102
val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule);
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   103
end
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   104
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   105
fun add_const c = Context.theory_map (TransferData.map
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17333
diff changeset
   106
  (fn {intros,unfolds,refolds,consts} =>
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   107
    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
17429
e8d6ed3aacfe merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents: 17333
diff changeset
   108
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   109
val transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt =>
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   110
  Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths));
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   111
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   112
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
   113
  TransferData.init #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
   114
  Attrib.add_attributes
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   115
    [("transfer_intro", Attrib.add_del_args intro_add intro_del,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
   116
      "declaration of transfer introduction rule"),
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   117
     ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
   118
      "declaration of transfer unfolding rule"),
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   119
     ("transfer_refold", Attrib.add_del_args refold_add refold_del,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17985
diff changeset
   120
      "declaration of transfer refolding rule")] #>
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   121
  Method.add_method ("transfer", transfer_method, "transfer principle");
17329
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   122
72637e062a0d new implementation of transfer principle
huffman
parents:
diff changeset
   123
end;