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