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