src/HOL/Tools/transfer.ML
author huffman
Wed, 24 Oct 2012 18:43:25 +0200
changeset 49975 faf4afed009f
parent 49625 06cf80661e7a
child 49976 e1c45d8ec175
permissions -rw-r--r--
transfer package: more flexible handling of equality relations using is_equality predicate
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
49625
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    11
  val get_sym_relator_eq: Proof.context -> thm list
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    12
  val transfer_add: attribute
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    13
  val transfer_del: attribute
47803
2e3821e13d67 allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
huffman
parents: 47789
diff changeset
    14
  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
    15
  val transfer_tac: bool -> Proof.context -> int -> tactic
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
    16
  val transfer_prover_tac: Proof.context -> int -> tactic
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    17
  val setup: theory -> theory
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    18
end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    19
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    20
structure Transfer : TRANSFER =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    21
struct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    22
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    23
(** Theory Data **)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    24
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    25
structure Data = Generic_Data
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    26
(
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    27
  type T =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    28
    { 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
    29
      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
    30
      compound_rhs : unit Net.net,
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    31
      relator_eq : thm Item_Net.T }
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    32
  val empty =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    33
    { 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
    34
      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
    35
      compound_rhs = Net.empty,
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    36
      relator_eq = Thm.full_rules }
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    37
  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
    38
  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
    39
    ( { 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
    40
        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
    41
      { 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
    42
        compound_rhs = c2, relator_eq = r2}) =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    43
    { 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
    44
      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
    45
      compound_rhs = Net.merge (K true) (c1, c2),
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    46
      relator_eq = Item_Net.merge (r1, r2) }
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    47
)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    48
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    49
fun get_relator_eq ctxt = ctxt
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    50
  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
49625
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    51
  |> map safe_mk_meta_eq
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    52
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    53
fun get_sym_relator_eq ctxt = ctxt
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    54
  |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    55
  |> map (Thm.symmetric o safe_mk_meta_eq)
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    56
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    57
fun get_transfer_raw ctxt = ctxt
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    58
  |> (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
    59
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    60
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
    61
  |> (#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
    62
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    63
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
    64
  |> (#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
    65
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    66
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
    67
  { 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
    68
  { 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
    69
    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
    70
    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
    71
    relator_eq = f4 relator_eq }
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    72
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    73
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
    74
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
    75
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
    76
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
    77
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
    78
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
    79
  (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
    80
   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
    81
     (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
    82
        _ $ _ $ (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
    83
      | _ => 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
    84
   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
    85
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    86
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
    87
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    88
(** Conversions **)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    89
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    90
val Rel_rule = Thm.symmetric @{thm Rel_def}
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    91
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    92
fun dest_funcT cT =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    93
  (case Thm.dest_ctyp cT of [T, U] => (T, U)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    94
    | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    95
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    96
fun Rel_conv ct =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    97
  let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    98
      val (cU, _) = dest_funcT cT'
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    99
  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   100
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   101
fun Trueprop_conv cv ct =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   102
  (case Thm.term_of ct of
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   103
    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   104
  | _ => raise CTERM ("Trueprop_conv", [ct]))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   105
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   106
(* Conversion to preprocess a transfer rule *)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   107
fun prep_conv ct = (
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   108
      Conv.implies_conv Conv.all_conv prep_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   109
      else_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   110
      Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   111
      else_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   112
      Conv.all_conv) ct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   113
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   114
(** Replacing explicit equalities with is_equality premises **)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   115
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   116
fun mk_is_equality t =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   117
  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   118
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   119
val is_equality_lemma =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   120
  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   121
    by (unfold is_equality_def, rule, drule meta_spec,
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   122
      erule meta_mp, rule refl, simp)}
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   123
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   124
fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   125
  let
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   126
    val thy = Thm.theory_of_thm thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   127
    val prop = Thm.prop_of thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   128
    val (t, mk_prop') = dest prop
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   129
    val add_eqs = Term.fold_aterms
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   130
      (fn t as Const (@{const_name HOL.eq}, _) => insert (op =) t | _ => I)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   131
    val eq_consts = rev (add_eqs t [])
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   132
    val eqTs = map (snd o dest_Const) eq_consts
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   133
    val used = Term.add_free_names prop []
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   134
    val names = map (K "") eqTs |> Name.variant_list used
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   135
    val frees = map Free (names ~~ eqTs)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   136
    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   137
    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   138
    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   139
    val cprop = Thm.cterm_of thy prop2
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   140
    val equal_thm = Raw_Simplifier.rewrite false [is_equality_lemma] cprop
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   141
    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   142
  in
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   143
    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   144
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   145
    handle TERM _ => thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   146
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   147
fun abstract_equalities_transfer thm =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   148
  let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   149
    fun dest prop =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   150
      let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   151
        val prems = Logic.strip_imp_prems prop
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   152
        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   153
        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   154
      in
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   155
        (rel, fn rel' =>
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   156
          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   157
      end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   158
  in
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   159
    gen_abstract_equalities dest thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   160
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   161
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   162
fun abstract_equalities_relator_eq rel_eq_thm =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   163
  gen_abstract_equalities (fn x => (x, I))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   164
    (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   165
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   166
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   167
(** Transfer proof method **)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   168
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   169
val post_simps =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   170
  @{thms transfer_forall_eq [symmetric]
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   171
    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
   172
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   173
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   174
  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
   175
    val keepers = keepers @ get_known_frees ctxt
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   176
    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
   177
    val vs' = filter_out (member (op =) keepers) vs
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   178
  in
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   179
    Induct.arbitrary_tac ctxt 0 vs' i
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   180
  end)
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   181
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   182
fun mk_relT (T, U) = T --> U --> HOLogic.boolT
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   183
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   184
fun mk_Rel t =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   185
  let val T = fastype_of t
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   186
  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
   187
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   188
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
   189
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   190
    val thy = Proof_Context.theory_of ctxt
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   191
    (* 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
   192
    fun rel (T as TFree (a, _)) U =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   193
          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
   194
      | 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
   195
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   196
          val r1 = rel T1 U1
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   197
          val r2 = rel T2 U2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   198
          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
   199
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   200
          Const (@{const_name fun_rel}, rT) $ r1 $ r2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   201
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   202
      | rel T U = raise TYPE ("rel", [T, U], [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   203
    fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   204
      | 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
   205
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   206
          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
   207
          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
   208
          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
   209
          val thm0 = Thm.assume cprop
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   210
          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   211
          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
   212
          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
   213
          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
   214
          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
   215
          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
   216
          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
   217
          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   218
          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
   219
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   220
          (thm2 COMP rule, hyps)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   221
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   222
      | zip ctxt thms (f $ t) (g $ u) =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   223
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   224
          val (thm1, hyps1) = zip ctxt thms f g
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   225
          val (thm2, hyps2) = zip ctxt thms t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   226
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   227
          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   228
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   229
      | zip _ _ (t as Free (_, T)) u =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   230
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   231
          val U = fastype_of u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   232
          val prop = mk_Rel (rel T U) $ t $ u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   233
          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
   234
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   235
          (Thm.assume cprop, [cprop])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   236
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   237
      | zip _ _ t u = raise TERM ("zip_relterm", [t, u])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   238
    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
   239
    val goal = HOLogic.mk_Trueprop (r $ t $ u)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   240
    val rename = Thm.trivial (cterm_of thy goal)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   241
    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
   242
  in
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   243
    Drule.implies_intr_list hyps (thm RS rename)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   244
  end
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   245
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   246
fun transfer_rule_of_term ctxt t =
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   247
  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
   248
    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
   249
    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
   250
    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
   251
      let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   252
        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
   253
      in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   254
        (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
   255
      end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   256
    (* 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
   257
    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
   258
      | 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
   259
        let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   260
          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
   261
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   262
          (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
   263
        end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   264
      | 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
   265
        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
   266
        let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   267
          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
   268
          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
   269
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   270
          (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
   271
        end
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   272
      | skeleton _ ctxt = dummy ctxt
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   273
    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
   274
      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
   275
    val frees = map fst (Term.add_frees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   276
    val tfrees = map fst (Term.add_tfrees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   277
    fun prep a = "R" ^ Library.unprefix "'" a
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   278
    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
   279
    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
   280
  in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   281
    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
   282
  end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   283
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   284
fun transfer_tac equiv ctxt i =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   285
  let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   286
    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
   287
    val start_rule = 
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   288
      if equiv then @{thm transfer_start} else @{thm transfer_start'}
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   289
    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
   290
    (* 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
   291
    val end_tac = if equiv then K all_tac else K no_tac
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   292
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   293
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   294
      [rewrite_goal_tac pre_simps i THEN
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   295
       SUBGOAL (fn (t, i) =>
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   296
         rtac start_rule i THEN
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   297
         (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
   298
           THEN_ALL_NEW
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   299
             (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   300
               ORELSE' end_tac)) (i + 1)) i,
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   301
       (* 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
   302
       rewrite_goal_tac post_simps i,
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   303
       rtac @{thm _} i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   304
  end
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   305
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   306
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   307
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   308
    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
   309
    val rule1 = transfer_rule_of_term ctxt rhs
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   310
    val rules = get_transfer_raw ctxt
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   311
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   312
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   313
      [CONVERSION prep_conv i,
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   314
       rtac @{thm transfer_prover_start} i,
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   315
       (rtac rule1 THEN_ALL_NEW
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   316
         REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
47618
1568dadd598a make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
huffman
parents: 47580
diff changeset
   317
       rtac @{thm refl} i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   318
  end)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   319
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   320
(** Methods and attributes **)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   321
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   322
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
   323
  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
   324
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   325
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
   326
  |-- Scan.repeat free) []
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   327
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   328
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
   329
  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
   330
    SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   331
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   332
val transfer_prover_method : (Proof.context -> Method.method) context_parser =
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   333
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   334
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   335
(* Attribute for transfer rules *)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   336
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   337
val prep_rule = abstract_equalities_transfer o Conv.fconv_rule prep_conv
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   338
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   339
val transfer_add =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   340
  Thm.declaration_attribute (add_transfer_thm o prep_rule)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   341
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   342
val transfer_del =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   343
  Thm.declaration_attribute (del_transfer_thm o prep_rule)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   344
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   345
val transfer_attribute =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   346
  Attrib.add_del transfer_add transfer_del
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   347
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   348
(* Theory setup *)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   349
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   350
val relator_eq_setup =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   351
  let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   352
    val name = @{binding relator_eq}
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   353
    fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   354
      #> add_transfer_thm (abstract_equalities_relator_eq thm)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   355
    fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   356
      #> del_transfer_thm (abstract_equalities_relator_eq thm)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   357
    val add = Thm.declaration_attribute add_thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   358
    val del = Thm.declaration_attribute del_thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   359
    val text = "declaration of relator equality rule (used by transfer method)"
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   360
    val content = Item_Net.content o #relator_eq o Data.get
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   361
  in
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   362
    Attrib.setup name (Attrib.add_del add del) text
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   363
    #> Global_Theory.add_thms_dynamic (name, content)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   364
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   365
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   366
val setup =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   367
  relator_eq_setup
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   368
  #> Attrib.setup @{binding transfer_rule} transfer_attribute
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   369
     "transfer rule for transfer method"
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   370
  #> Global_Theory.add_thms_dynamic
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   371
     (@{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
   372
  #> 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
   373
     "generic theorem transfer method"
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   374
  #> Method.setup @{binding transfer'} (transfer_method false)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   375
     "generic theorem transfer method"
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   376
  #> Method.setup @{binding transfer_prover} transfer_prover_method
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   377
     "for proving transfer rules"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   378
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   379
end