src/HOL/Tools/transfer.ML
author huffman
Sat, 02 Jun 2012 08:27:29 +0200
changeset 48066 c6783c9b87bf
parent 48065 8aa05d38299a
child 49625 06cf80661e7a
permissions -rw-r--r--
transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     1
(*  Title:      HOL/Tools/transfer.ML
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman, TU Muenchen
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     3
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     4
Generic theorem transfer method.
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     5
*)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     6
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     7
signature TRANSFER =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     8
sig
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     9
  val prep_conv: conv
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
    10
  val get_relator_eq: Proof.context -> thm list
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    11
  val transfer_add: attribute
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    12
  val transfer_del: attribute
47803
2e3821e13d67 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
huffman
parents: 47789
diff changeset
    13
  val transfer_rule_of_term: Proof.context -> term -> thm
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
    14
  val transfer_tac: bool -> Proof.context -> int -> tactic
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
    15
  val transfer_prover_tac: Proof.context -> int -> tactic
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    16
  val setup: theory -> theory
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    17
end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    18
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    19
structure Transfer : TRANSFER =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    20
struct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    21
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    22
(** Theory Data **)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    23
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    24
structure Data = Generic_Data
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    25
(
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    26
  type T =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    27
    { transfer_raw : thm Item_Net.T,
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    28
      known_frees : (string * typ) list,
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    29
      compound_rhs : unit Net.net,
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    30
      relator_eq : thm Item_Net.T }
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    31
  val empty =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    32
    { transfer_raw = Thm.full_rules,
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    33
      known_frees = [],
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    34
      compound_rhs = Net.empty,
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    35
      relator_eq = Thm.full_rules }
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    36
  val extend = I
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    37
  fun merge
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    38
    ( { transfer_raw = t1, known_frees = k1,
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    39
        compound_rhs = c1, relator_eq = r1},
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    40
      { transfer_raw = t2, known_frees = k2,
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    41
        compound_rhs = c2, relator_eq = r2}) =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    42
    { transfer_raw = Item_Net.merge (t1, t2),
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    43
      known_frees = Library.merge (op =) (k1, k2),
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    44
      compound_rhs = Net.merge (K true) (c1, c2),
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    45
      relator_eq = Item_Net.merge (r1, r2) }
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    46
)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    47
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    48
fun get_relator_eq ctxt = ctxt
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    49
  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    50
  |> map (Thm.symmetric o mk_meta_eq)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    51
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    52
fun get_transfer_raw ctxt = ctxt
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    53
  |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    54
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    55
fun get_known_frees ctxt = ctxt
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    56
  |> (#known_frees o Data.get o Context.Proof)
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    57
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    58
fun get_compound_rhs ctxt = ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    59
  |> (#compound_rhs o Data.get o Context.Proof)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    60
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    61
fun map_data f1 f2 f3 f4
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    62
  { transfer_raw, known_frees, compound_rhs, relator_eq } =
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    63
  { transfer_raw = f1 transfer_raw,
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    64
    known_frees = f2 known_frees,
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    65
    compound_rhs = f3 compound_rhs,
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    66
    relator_eq = f4 relator_eq }
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    67
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    68
fun map_transfer_raw f = map_data f I I I
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    69
fun map_known_frees f = map_data I f I I
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    70
fun map_compound_rhs f = map_data I I f I
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    71
fun map_relator_eq f = map_data I I I f
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
    72
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    73
fun add_transfer_thm thm = Data.map
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    74
  (map_transfer_raw (Item_Net.update thm) o
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    75
   map_compound_rhs
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    76
     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    77
        _ $ _ $ (rhs as (_ $ _)) => Net.insert_term (K true) (rhs, ())
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    78
      | _ => I) o
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    79
   map_known_frees (Term.add_frees (Thm.concl_of thm)))
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    80
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    81
fun del_transfer_thm thm = Data.map (map_transfer_raw (Item_Net.remove thm))
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    82
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    83
val relator_eq_setup =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    84
  let
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    85
    val name = @{binding relator_eq}
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    86
    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    87
    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    88
    val add = Thm.declaration_attribute add_thm
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    89
    val del = Thm.declaration_attribute del_thm
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    90
    val text = "declaration of relator equality rule (used by transfer method)"
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    91
    val content = Item_Net.content o #relator_eq o Data.get
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    92
  in
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    93
    Attrib.setup name (Attrib.add_del add del) text
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    94
    #> Global_Theory.add_thms_dynamic (name, content)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    95
  end
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
    96
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    97
(** Conversions **)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    98
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    99
val Rel_rule = Thm.symmetric @{thm Rel_def}
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   100
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   101
fun dest_funcT cT =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   102
  (case Thm.dest_ctyp cT of [T, U] => (T, U)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   103
    | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   104
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   105
fun Rel_conv ct =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   106
  let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   107
      val (cU, _) = dest_funcT cT'
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   108
  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   109
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   110
fun Trueprop_conv cv ct =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   111
  (case Thm.term_of ct of
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   112
    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   113
  | _ => raise CTERM ("Trueprop_conv", [ct]))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   114
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   115
(* Conversion to preprocess a transfer rule *)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   116
fun prep_conv ct = (
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   117
      Conv.implies_conv Conv.all_conv prep_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   118
      else_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   119
      Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   120
      else_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   121
      Conv.all_conv) ct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   122
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   123
(** Transfer proof method **)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   124
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   125
fun RelT (Const (@{const_name Rel}, _) $ _ $ _ $ y) = fastype_of y
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   126
  | RelT t = raise TERM ("RelT", [t])
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   127
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   128
(* Tactic to correspond a value to itself *)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   129
fun eq_tac ctxt = SUBGOAL (fn (t, i) =>
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   130
  let
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   131
    val T = RelT (HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   132
    val cT = ctyp_of (Proof_Context.theory_of ctxt) T
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
   133
    val rews = get_relator_eq ctxt
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   134
    val thm1 = Drule.instantiate' [SOME cT] [] @{thm Rel_eq_refl}
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   135
    val thm2 = Raw_Simplifier.rewrite_rule rews thm1
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   136
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   137
    rtac thm2 i
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   138
  end handle Match => no_tac | TERM _ => no_tac)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   139
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   140
val post_simps =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   141
  @{thms transfer_forall_eq [symmetric]
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   142
    transfer_implies_eq [symmetric] transfer_bforall_unfold}
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   143
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   144
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   145
  let
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
   146
    val keepers = keepers @ get_known_frees ctxt
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   147
    val vs = rev (Term.add_frees t [])
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   148
    val vs' = filter_out (member (op =) keepers) vs
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   149
  in
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   150
    Induct.arbitrary_tac ctxt 0 vs' i
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   151
  end)
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   152
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   153
fun mk_relT (T, U) = T --> U --> HOLogic.boolT
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   154
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   155
fun mk_Rel t =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   156
  let val T = fastype_of t
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   157
  in Const (@{const_name Transfer.Rel}, T --> T) $ t end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   158
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   159
fun transfer_rule_of_terms ctxt tab t u =
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   160
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   161
    val thy = Proof_Context.theory_of ctxt
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   162
    (* precondition: T must consist of only TFrees and function space *)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   163
    fun rel (T as TFree (a, _)) U =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   164
          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   165
      | rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   166
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   167
          val r1 = rel T1 U1
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   168
          val r2 = rel T2 U2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   169
          val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   170
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   171
          Const (@{const_name fun_rel}, rT) $ r1 $ r2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   172
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   173
      | rel T U = raise TYPE ("rel", [T, U], [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   174
    fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   175
      | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   176
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   177
          val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   178
          val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   179
          val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   180
          val thm0 = Thm.assume cprop
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   181
          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   182
          val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   183
          val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   184
          val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   185
          val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   186
          val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   187
          val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   188
          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   189
          val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   190
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   191
          (thm2 COMP rule, hyps)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   192
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   193
      | zip ctxt thms (f $ t) (g $ u) =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   194
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   195
          val (thm1, hyps1) = zip ctxt thms f g
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   196
          val (thm2, hyps2) = zip ctxt thms t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   197
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   198
          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   199
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   200
      | zip _ _ (t as Free (_, T)) u =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   201
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   202
          val U = fastype_of u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   203
          val prop = mk_Rel (rel T U) $ t $ u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   204
          val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   205
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   206
          (Thm.assume cprop, [cprop])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   207
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   208
      | zip _ _ t u = raise TERM ("zip_relterm", [t, u])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   209
    val r = mk_Rel (rel (fastype_of t) (fastype_of u))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   210
    val goal = HOLogic.mk_Trueprop (r $ t $ u)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   211
    val rename = Thm.trivial (cterm_of thy goal)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   212
    val (thm, hyps) = zip ctxt [] t u
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   213
  in
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   214
    Drule.implies_intr_list hyps (thm RS rename)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   215
  end
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   216
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   217
fun transfer_rule_of_term ctxt t =
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   218
  let
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   219
    val compound_rhs = get_compound_rhs ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   220
    val is_rhs = not o null o Net.unify_term compound_rhs
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   221
    fun dummy ctxt =
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   222
      let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   223
        val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   224
      in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   225
        (Free (c, dummyT), ctxt)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   226
      end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   227
    (* create a lambda term of the same shape as the given term *)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   228
    fun skeleton (Bound i) ctxt = (Bound i, ctxt)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   229
      | skeleton (Abs (x, _, t)) ctxt =
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   230
        let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   231
          val (t', ctxt) = skeleton t ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   232
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   233
          (Abs (x, dummyT, t'), ctxt)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   234
        end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   235
      | skeleton (tu as (t $ u)) ctxt =
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   236
        if is_rhs tu then dummy ctxt else
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   237
        let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   238
          val (t', ctxt) = skeleton t ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   239
          val (u', ctxt) = skeleton u ctxt
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   240
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   241
          (t' $ u', ctxt)
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   242
        end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   243
      | skeleton _ ctxt = dummy ctxt
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   244
    val s = skeleton t ctxt |> fst |> Syntax.check_term ctxt |>
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   245
      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   246
    val frees = map fst (Term.add_frees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   247
    val tfrees = map fst (Term.add_tfrees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   248
    fun prep a = "R" ^ Library.unprefix "'" a
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   249
    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   250
    val thm = transfer_rule_of_terms ctxt' (tfrees ~~ rnames) s t
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   251
  in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   252
    Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   253
  end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   254
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   255
fun transfer_tac equiv ctxt i =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   256
  let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   257
    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   258
    val start_rule = 
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   259
      if equiv then @{thm transfer_start} else @{thm transfer_start'}
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   260
    val rules = get_transfer_raw ctxt
47803
2e3821e13d67 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
huffman
parents: 47789
diff changeset
   261
    (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
2e3821e13d67 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
huffman
parents: 47789
diff changeset
   262
    val end_tac = if equiv then K all_tac else K no_tac
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   263
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   264
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   265
      [rewrite_goal_tac pre_simps i THEN
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   266
       SUBGOAL (fn (t, i) =>
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   267
         rtac start_rule i THEN
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   268
         (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   269
           THEN_ALL_NEW
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   270
             (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
47803
2e3821e13d67 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
huffman
parents: 47789
diff changeset
   271
               ORELSE' eq_tac ctxt ORELSE' end_tac)) (i + 1)) i,
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   272
       (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   273
       rewrite_goal_tac post_simps i,
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   274
       rtac @{thm _} i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   275
  end
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   276
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   277
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   278
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   279
    val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   280
    val rule1 = transfer_rule_of_term ctxt rhs
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   281
    val rules = get_transfer_raw ctxt
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   282
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   283
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   284
      [CONVERSION prep_conv i,
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   285
       rtac @{thm transfer_prover_start} i,
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   286
       (rtac rule1 THEN_ALL_NEW
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   287
         REPEAT_ALL_NEW
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   288
           (resolve_tac rules ORELSE' eq_tac ctxt)) (i+1),
47618
1568dadd598a make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents: 47580
diff changeset
   289
       rtac @{thm refl} i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   290
  end)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   291
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   292
(** Methods and attributes **)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   293
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   294
val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   295
  error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   296
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   297
val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   298
  |-- Scan.repeat free) []
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   299
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   300
fun transfer_method equiv : (Proof.context -> Method.method) context_parser =
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   301
  fixing >> (fn vs => fn ctxt =>
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   302
    SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   303
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   304
val transfer_prover_method : (Proof.context -> Method.method) context_parser =
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   305
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   306
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   307
(* Attribute for transfer rules *)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   308
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   309
val prep_rule = Conv.fconv_rule prep_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   310
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   311
val transfer_add =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   312
  Thm.declaration_attribute (add_transfer_thm o prep_rule)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   313
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   314
val transfer_del =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   315
  Thm.declaration_attribute (del_transfer_thm o prep_rule)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   316
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   317
val transfer_attribute =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   318
  Attrib.add_del transfer_add transfer_del
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   319
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   320
(* Theory setup *)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   321
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   322
val setup =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   323
  relator_eq_setup
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   324
  #> Attrib.setup @{binding transfer_rule} transfer_attribute
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   325
     "transfer rule for transfer method"
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   326
  #> Global_Theory.add_thms_dynamic
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   327
     (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   328
  #> Method.setup @{binding transfer} (transfer_method true)
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   329
     "generic theorem transfer method"
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   330
  #> Method.setup @{binding transfer'} (transfer_method false)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   331
     "generic theorem transfer method"
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   332
  #> Method.setup @{binding transfer_prover} transfer_prover_method
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   333
     "for proving transfer rules"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   334
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   335
end