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