src/HOL/Tools/transfer.ML
author kuncar
Thu, 22 Aug 2013 17:19:44 +0200
changeset 53144 74b879546c33
parent 53131 701360318565
child 53145 2fb458aceb78
permissions -rw-r--r--
publish a private function
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
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
     3
    Author:     Ondrej Kuncar, TU Muenchen
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     4
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     5
Generic theorem transfer method.
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     6
*)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     7
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     8
signature TRANSFER =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
     9
sig
52883
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
    10
  val bottom_rewr_conv: thm list -> conv
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
    11
  val top_rewr_conv: thm list -> conv
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
    12
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    13
  val prep_conv: conv
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    14
  val get_transfer_raw: Proof.context -> thm list
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
    15
  val get_relator_eq: Proof.context -> thm list
49625
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    16
  val get_sym_relator_eq: Proof.context -> thm list
51954
2e3f9e72b8c4 publish a private function
kuncar
parents: 51437
diff changeset
    17
  val get_relator_eq_raw: Proof.context -> thm list
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    18
  val get_relator_domain: Proof.context -> thm list
53144
74b879546c33 publish a private function
kuncar
parents: 53131
diff changeset
    19
  val get_compound_lhs: Proof.context -> term Net.net
74b879546c33 publish a private function
kuncar
parents: 53131
diff changeset
    20
  val get_compound_rhs: Proof.context -> term Net.net
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    21
  val transfer_add: attribute
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    22
  val transfer_del: attribute
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    23
  val transferred_attribute: thm list -> attribute
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
    24
  val untransferred_attribute: thm list -> attribute
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    25
  val transfer_domain_add: attribute
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    26
  val transfer_domain_del: attribute
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    27
  val transfer_rule_of_term: Proof.context -> bool -> term -> thm
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    28
  val transfer_rule_of_lhs: Proof.context -> term -> thm
47658
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
    29
  val transfer_tac: bool -> Proof.context -> int -> tactic
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
    30
  val transfer_prover_tac: Proof.context -> int -> tactic
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    31
  val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    32
  val setup: theory -> theory
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    33
end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    34
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    35
structure Transfer : TRANSFER =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    36
struct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    37
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    38
(** Theory Data **)
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    39
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    40
structure Data = Generic_Data
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    41
(
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    42
  type T =
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    43
    { 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
    44
      known_frees : (string * typ) list,
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
    45
      compound_lhs : term Net.net,
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
    46
      compound_rhs : term Net.net,
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    47
      relator_eq : thm Item_Net.T,
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    48
      relator_eq_raw : thm Item_Net.T,
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    49
      relator_domain : thm Item_Net.T }
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    50
  val empty =
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    51
    { transfer_raw = Thm.intro_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
    52
      known_frees = [],
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    53
      compound_lhs = Net.empty,
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    54
      compound_rhs = Net.empty,
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    55
      relator_eq = Thm.full_rules,
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    56
      relator_eq_raw = Thm.full_rules,
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    57
      relator_domain = Thm.full_rules }
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    58
  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
    59
  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
    60
    ( { transfer_raw = t1, known_frees = k1,
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    61
        compound_lhs = l1,
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    62
        compound_rhs = c1, relator_eq = r1,
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    63
        relator_eq_raw = rw1, relator_domain = rd1 },
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    64
      { transfer_raw = t2, known_frees = k2,
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    65
        compound_lhs = l2,
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    66
        compound_rhs = c2, relator_eq = r2,
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    67
        relator_eq_raw = rw2, relator_domain = rd2 } ) =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    68
    { 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
    69
      known_frees = Library.merge (op =) (k1, k2),
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    70
      compound_lhs = Net.merge (K true) (l1, l2),
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
    71
      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
    72
      relator_eq = Item_Net.merge (r1, r2),
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    73
      relator_eq_raw = Item_Net.merge (rw1, rw2),
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    74
      relator_domain = Item_Net.merge (rd1, rd2) }
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    75
)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
    76
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    77
fun get_transfer_raw ctxt = ctxt
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    78
  |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    79
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    80
fun get_known_frees ctxt = ctxt
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    81
  |> (#known_frees o Data.get o Context.Proof)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    82
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    83
fun get_compound_lhs ctxt = ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    84
  |> (#compound_lhs o Data.get o Context.Proof)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
    85
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    86
fun get_compound_rhs ctxt = ctxt
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    87
  |> (#compound_rhs o Data.get o Context.Proof)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
    88
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    89
fun get_relator_eq ctxt = ctxt
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    90
  |> (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
    91
  |> map safe_mk_meta_eq
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    92
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    93
fun get_sym_relator_eq ctxt = ctxt
06cf80661e7a new get function for non-symmetric relator_eq & tuned
kuncar
parents: 48066
diff changeset
    94
  |> (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
    95
  |> map (Thm.symmetric o safe_mk_meta_eq)
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
    96
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    97
fun get_relator_eq_raw ctxt = ctxt
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
    98
  |> (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
    99
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   100
fun get_relator_domain ctxt = ctxt
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   101
  |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
   102
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   103
fun map_data f1 f2 f3 f4 f5 f6 f7
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   104
  { transfer_raw, known_frees, compound_lhs, compound_rhs,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   105
    relator_eq, relator_eq_raw, relator_domain } =
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
   106
  { 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
   107
    known_frees = f2 known_frees,
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   108
    compound_lhs = f3 compound_lhs,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   109
    compound_rhs = f4 compound_rhs,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   110
    relator_eq = f5 relator_eq,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   111
    relator_eq_raw = f6 relator_eq_raw,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   112
    relator_domain = f7 relator_domain }
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   113
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   114
fun map_transfer_raw   f = map_data f I I I I I I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   115
fun map_known_frees    f = map_data I f I I I I I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   116
fun map_compound_lhs   f = map_data I I f I I I I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   117
fun map_compound_rhs   f = map_data I I I f I I I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   118
fun map_relator_eq     f = map_data I I I I f I I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   119
fun map_relator_eq_raw f = map_data I I I I I f I
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   120
fun map_relator_domain f = map_data I I I I I I f
47503
cb44d09d9d22 add theory data for relator identity rules;
huffman
parents: 47356
diff changeset
   121
48065
8aa05d38299a transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
huffman
parents: 48064
diff changeset
   122
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
   123
  (map_transfer_raw (Item_Net.update thm) o
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   124
   map_compound_lhs
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   125
     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   126
        Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   127
          Net.insert_term_safe (K true) (lhs, lhs)
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   128
      | _ => I) 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
   129
   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
   130
     (case HOLogic.dest_Trueprop (Thm.concl_of thm) of
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   131
        Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   132
          Net.insert_term_safe (K true) (rhs, rhs)
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   133
      | _ => 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
   134
   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
   135
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   136
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
   137
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   138
(** Conversions **)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   139
52883
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   140
fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   141
fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   142
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   143
fun transfer_rel_conv conv = 
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   144
  Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   145
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   146
val Rel_rule = Thm.symmetric @{thm Rel_def}
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   147
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   148
fun dest_funcT cT =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   149
  (case Thm.dest_ctyp cT of [T, U] => (T, U)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   150
    | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   151
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   152
fun Rel_conv ct =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   153
  let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   154
      val (cU, _) = dest_funcT cT'
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   155
  in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   156
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   157
(* Conversion to preprocess a transfer rule *)
51955
04d9381bebff try to detect assumptions of transfer rules that are in a shape of a transfer rule
kuncar
parents: 51954
diff changeset
   158
fun safe_Rel_conv ct =
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   159
  Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct
51955
04d9381bebff try to detect assumptions of transfer rules that are in a shape of a transfer rule
kuncar
parents: 51954
diff changeset
   160
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   161
fun prep_conv ct = (
51955
04d9381bebff try to detect assumptions of transfer rules that are in a shape of a transfer rule
kuncar
parents: 51954
diff changeset
   162
      Conv.implies_conv safe_Rel_conv prep_conv
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   163
      else_conv
51955
04d9381bebff try to detect assumptions of transfer rules that are in a shape of a transfer rule
kuncar
parents: 51954
diff changeset
   164
      safe_Rel_conv
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   165
      else_conv
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   166
      Conv.all_conv) ct
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   167
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   168
(** 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
   169
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   170
fun mk_is_equality t =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   171
  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   172
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   173
val is_equality_lemma =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   174
  @{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
   175
    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
   176
      erule meta_mp, rule refl, simp)}
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   177
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   178
fun gen_abstract_equalities (dest : term -> term * (term -> term)) thm =
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   179
  let
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   180
    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
   181
    val prop = Thm.prop_of thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   182
    val (t, mk_prop') = dest prop
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   183
    (* Only consider "op =" at non-base types *)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   184
    fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   185
        (case T of Type (_, []) => false | _ => true)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   186
      | is_eq _ = false
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   187
    val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   188
    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
   189
    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
   190
    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
   191
    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
   192
    val frees = map Free (names ~~ eqTs)
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   193
    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
   194
    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
   195
    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
   196
    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
   197
    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
   198
    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   199
  in
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   200
    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
   201
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   202
    handle TERM _ => thm
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   203
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   204
fun abstract_equalities_transfer ctxt thm =
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   205
  let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   206
    fun dest prop =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   207
      let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   208
        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
   209
        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
   210
        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
   211
      in
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   212
        (rel, fn rel' =>
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   213
          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
   214
      end
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   215
    val contracted_eq_thm = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   216
      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   217
      handle CTERM _ => thm
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   218
  in
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   219
    gen_abstract_equalities dest contracted_eq_thm
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   220
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   221
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   222
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
   223
  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
   224
    (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
   225
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   226
fun abstract_equalities_domain ctxt thm =
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   227
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   228
    fun dest prop =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   229
      let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   230
        val prems = Logic.strip_imp_prems prop
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   231
        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   232
        val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   233
      in
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   234
        (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   235
      end
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   236
    fun transfer_rel_conv conv = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   237
      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   238
    val contracted_eq_thm = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   239
      Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   240
  in
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   241
    gen_abstract_equalities dest contracted_eq_thm
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   242
  end 
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   243
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   244
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   245
(** Replacing explicit Domainp predicates with Domainp assumptions **)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   246
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   247
fun mk_Domainp_assm (T, R) =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   248
  HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   249
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   250
val Domainp_lemma =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   251
  @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   252
    by (rule, drule meta_spec,
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   253
      erule meta_mp, rule refl, simp)}
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   254
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   255
fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   256
  | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   257
  | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   258
  | fold_Domainp _ _ = I
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   259
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   260
fun subst_terms tab t = 
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   261
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   262
    val t' = Termtab.lookup tab t
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   263
  in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   264
    case t' of
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   265
      SOME t' => t'
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   266
      | NONE => 
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   267
        (case t of
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   268
          u $ v => (subst_terms tab u) $ (subst_terms tab v)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   269
          | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   270
          | t => t)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   271
  end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   272
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   273
fun gen_abstract_domains (dest : term -> term * (term -> term)) thm =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   274
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   275
    val thy = Thm.theory_of_thm thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   276
    val prop = Thm.prop_of thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   277
    val (t, mk_prop') = dest prop
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   278
    val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   279
    val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   280
    val used = Term.add_free_names t []
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   281
    val rels = map (snd o dest_comb) Domainp_tms
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   282
    val rel_names = map (fst o fst o dest_Var) rels
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   283
    val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   284
    val frees = map Free (names ~~ Domainp_Ts)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   285
    val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   286
    val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   287
    val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   288
    val prop2 = Logic.list_rename_params (rev names) prop1
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   289
    val cprop = Thm.cterm_of thy prop2
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   290
    val equal_thm = Raw_Simplifier.rewrite false [Domainp_lemma] cprop
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   291
    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   292
  in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   293
    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   294
  end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   295
    handle TERM _ => thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   296
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   297
fun abstract_domains_transfer thm =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   298
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   299
    fun dest prop =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   300
      let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   301
        val prems = Logic.strip_imp_prems prop
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   302
        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   303
        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   304
      in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   305
        (x, fn x' =>
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   306
          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   307
      end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   308
  in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   309
    gen_abstract_domains dest thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   310
  end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   311
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   312
fun detect_transfer_rules thm =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   313
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   314
    fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   315
      (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   316
      | _ $ _ $ _ => true
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   317
      | _ => false
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   318
    fun safe_transfer_rule_conv ctm =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   319
      if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   320
  in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   321
    Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   322
  end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   323
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   324
(** Adding transfer domain rules **)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   325
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   326
fun add_transfer_domain_thm thm ctxt = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   327
  (add_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   328
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   329
fun del_transfer_domain_thm thm ctxt = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   330
  (del_transfer_thm o abstract_equalities_domain (Context.proof_of ctxt) o detect_transfer_rules) thm ctxt
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   331
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   332
(** Transfer proof method **)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   333
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   334
val post_simps =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   335
  @{thms transfer_forall_eq [symmetric]
47355
3d9d98e0f1a4 add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
huffman
parents: 47327
diff changeset
   336
    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
   337
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   338
fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   339
  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
   340
    val keepers = keepers @ get_known_frees ctxt
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   341
    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
   342
    val vs' = filter_out (member (op =) keepers) vs
47356
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   343
  in
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   344
    Induct.arbitrary_tac ctxt 0 vs' i
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   345
  end)
19fb95255ec9 transfer method generalizes over free variables in goal
huffman
parents: 47355
diff changeset
   346
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   347
fun mk_relT (T, U) = T --> U --> HOLogic.boolT
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   348
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   349
fun mk_Rel t =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   350
  let val T = fastype_of t
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   351
  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
   352
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   353
fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   354
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   355
    val thy = Proof_Context.theory_of ctxt
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   356
    (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   357
    fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   358
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   359
          val r1 = rel T1 U1
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   360
          val r2 = rel T2 U2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   361
          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
   362
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   363
          Const (@{const_name fun_rel}, rT) $ r1 $ r2
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   364
        end
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   365
      | rel T U =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   366
        let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   367
          val (a, _) = dest_TFree (prj (T, U))
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   368
        in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   369
          Free (the (AList.lookup (op =) tab a), mk_relT (T, U))
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   370
        end
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   371
    fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   372
      | 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
   373
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   374
          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
   375
          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
   376
          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
   377
          val thm0 = Thm.assume cprop
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   378
          val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   379
          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
   380
          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
   381
          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
   382
          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
   383
          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
   384
          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
   385
          val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   386
          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
   387
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   388
          (thm2 COMP rule, hyps)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   389
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   390
      | zip ctxt thms (f $ t) (g $ u) =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   391
        let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   392
          val (thm1, hyps1) = zip ctxt thms f g
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   393
          val (thm2, hyps2) = zip ctxt thms t u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   394
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   395
          (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   396
        end
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   397
      | zip _ _ t u =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   398
        let
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   399
          val T = fastype_of t
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   400
          val U = fastype_of u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   401
          val prop = mk_Rel (rel T U) $ t $ u
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   402
          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
   403
        in
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   404
          (Thm.assume cprop, [cprop])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   405
        end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   406
    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
   407
    val goal = HOLogic.mk_Trueprop (r $ t $ u)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   408
    val rename = Thm.trivial (cterm_of thy goal)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   409
    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
   410
  in
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   411
    Drule.implies_intr_list hyps (thm RS rename)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   412
  end
47580
d99c883cdf2c use simpler method for preserving bound variable names in transfer tactic
huffman
parents: 47568
diff changeset
   413
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   414
(* create a lambda term of the same shape as the given term *)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   415
fun skeleton (is_atom : term -> bool) ctxt t =
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   416
  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
   417
    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
   418
      let
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   419
        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
   420
      in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   421
        (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
   422
      end
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   423
    fun go (Bound i) ctxt = (Bound i, ctxt)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   424
      | go (Abs (x, _, t)) ctxt =
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   425
        let
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   426
          val (t', ctxt) = go t ctxt
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   427
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   428
          (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
   429
        end
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   430
      | go (tu as (t $ u)) ctxt =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   431
        if is_atom 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
   432
        let
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   433
          val (t', ctxt) = go t ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   434
          val (u', ctxt) = go u ctxt
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   435
        in
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48065
diff changeset
   436
          (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
   437
        end
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   438
      | go _ ctxt = dummy ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   439
  in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   440
    go t ctxt |> fst |> Syntax.check_term ctxt |>
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   441
      map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   442
  end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   443
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   444
(** Monotonicity analysis **)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   445
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   446
(* TODO: Put extensible table in theory data *)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   447
val monotab =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   448
  Symtab.make
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   449
    [(@{const_name transfer_implies}, [~1, 1]),
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   450
     (@{const_name transfer_forall}, [1])(*,
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   451
     (@{const_name implies}, [~1, 1]),
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   452
     (@{const_name All}, [1])*)]
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   453
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   454
(*
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   455
Function bool_insts determines the set of boolean-relation variables
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   456
that can be instantiated to implies, rev_implies, or iff.
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   457
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   458
Invariants: bool_insts p (t, u) requires that
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   459
  u :: _ => _ => ... => bool, and
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   460
  t is a skeleton of u
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   461
*)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   462
fun bool_insts p (t, u) =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   463
  let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   464
    fun strip2 (t1 $ t2, u1 $ u2, tus) =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   465
        strip2 (t1, u1, (t2, u2) :: tus)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   466
      | strip2 x = x
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   467
    fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   468
    fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   469
      | go Ts p (t, u) tab =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   470
        let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   471
          val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   472
          val (_, tf, tus) = strip2 (t, u, [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   473
          val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   474
          val tab1 =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   475
            case ps_opt of
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   476
              SOME ps =>
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   477
              let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   478
                val ps' = map (fn x => p * x) (take (length tus) ps)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   479
              in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   480
                fold I (map2 (go Ts) ps' tus) tab
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   481
              end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   482
            | NONE => tab
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   483
          val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   484
        in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   485
          Symtab.join (K or3) (tab1, tab2)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   486
        end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   487
    val tab = go [] p (t, u) Symtab.empty
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   488
    fun f (a, (true, false, false)) = SOME (a, @{const implies})
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   489
      | f (a, (false, true, false)) = SOME (a, @{const rev_implies})
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   490
      | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   491
      | f _                         = NONE
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   492
  in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   493
    map_filter f (Symtab.dest tab)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   494
  end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   495
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   496
fun matches_list ctxt term = 
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   497
   exists (equal true) o map (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   498
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   499
fun transfer_rule_of_term ctxt equiv t : thm =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   500
  let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   501
    val compound_rhs = get_compound_rhs ctxt
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   502
    fun is_rhs t = (matches_list ctxt t o Net.unify_term compound_rhs) t
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   503
    val s = skeleton is_rhs ctxt t
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   504
    val frees = map fst (Term.add_frees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   505
    val tfrees = map fst (Term.add_tfrees s [])
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   506
    fun prep a = "R" ^ Library.unprefix "'" a
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   507
    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   508
    val tab = tfrees ~~ rnames
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   509
    fun prep a = the (AList.lookup (op =) tab a)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   510
    val thm = transfer_rule_of_terms fst ctxt' tab s t
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   511
    val binsts = bool_insts (if equiv then 0 else 1) (s, t)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   512
    val cbool = @{ctyp bool}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   513
    val relT = @{typ "bool => bool => bool"}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   514
    val idx = Thm.maxidx_of thm + 1
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   515
    val thy = Proof_Context.theory_of ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   516
    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   517
    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   518
  in
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   519
    thm
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   520
      |> Thm.generalize (tfrees, rnames @ frees) idx
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   521
      |> Thm.instantiate (map tinst binsts, map inst binsts)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   522
  end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   523
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   524
fun transfer_rule_of_lhs ctxt t : thm =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   525
  let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   526
    val compound_lhs = get_compound_lhs ctxt
53131
701360318565 double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
kuncar
parents: 53042
diff changeset
   527
    fun is_lhs t = (matches_list ctxt t o Net.unify_term compound_lhs) t
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   528
    val s = skeleton is_lhs ctxt t
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   529
    val frees = map fst (Term.add_frees s [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   530
    val tfrees = map fst (Term.add_tfrees s [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   531
    fun prep a = "R" ^ Library.unprefix "'" a
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   532
    val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   533
    val tab = tfrees ~~ rnames
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   534
    fun prep a = the (AList.lookup (op =) tab a)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   535
    val thm = transfer_rule_of_terms snd ctxt' tab t s
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   536
    val binsts = bool_insts 1 (s, t)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   537
    val cbool = @{ctyp bool}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   538
    val relT = @{typ "bool => bool => bool"}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   539
    val idx = Thm.maxidx_of thm + 1
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   540
    val thy = Proof_Context.theory_of ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   541
    fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   542
    fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   543
  in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   544
    thm
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   545
      |> Thm.generalize (tfrees, rnames @ frees) idx
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   546
      |> Thm.instantiate (map tinst binsts, map inst binsts)
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   547
  end
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   548
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   549
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
   550
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   551
fun transfer_tac equiv ctxt i =
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   552
  let
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   553
    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   554
    val start_rule =
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   555
      if equiv then @{thm transfer_start} else @{thm transfer_start'}
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   556
    val rules = get_transfer_raw ctxt
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   557
    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
   558
    (* 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
   559
    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
   560
    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
   561
    fun main_tac (t, i) =
3259ea7a52af transfer package: error message if preprocessing goal to object-logic formula fails
huffman
parents: 49976
diff changeset
   562
      rtac start_rule i THEN
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   563
      (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))
49977
3259ea7a52af transfer package: error message if preprocessing goal to object-logic formula fails
huffman
parents: 49976
diff changeset
   564
        THEN_ALL_NEW
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   565
          (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
   566
            ORELSE' end_tac)) (i + 1)
3259ea7a52af transfer package: error message if preprocessing goal to object-logic formula fails
huffman
parents: 49976
diff changeset
   567
        handle TERM (_, ts) => raise TERM (err_msg, ts)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   568
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   569
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   570
      [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
   571
       SUBGOAL main_tac i,
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   572
       (* 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
   573
       rewrite_goal_tac post_simps i,
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   574
       Goal.norm_hhf_tac i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   575
  end
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   576
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   577
fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   578
  let
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   579
    val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   580
    val rule1 = transfer_rule_of_term ctxt false rhs
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   581
    val rules = get_transfer_raw ctxt
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   582
    val eq_rules = get_relator_eq_raw ctxt
52883
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   583
    val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm fun_rel_eq[symmetric,THEN eq_reflection]}])
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   584
  in
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   585
    EVERY
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   586
      [CONVERSION prep_conv i,
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   587
       rtac @{thm transfer_prover_start} i,
52883
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   588
       ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))
0a7c97c76f46 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents: 52358
diff changeset
   589
        THEN_ALL_NEW
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   590
         (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
   591
       rtac @{thm refl} i]
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   592
  end)
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   593
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   594
(** Transfer attribute **)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   595
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   596
fun transferred ctxt extra_rules thm =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   597
  let
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   598
    val start_rule = @{thm transfer_start}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   599
    val start_rule' = @{thm transfer_start'}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   600
    val rules = extra_rules @ get_transfer_raw ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   601
    val eq_rules = get_relator_eq_raw ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   602
    val err_msg = "Transfer failed to convert goal to an object-logic formula"
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   603
    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   604
    val thm1 = Drule.forall_intr_vars thm
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   605
    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   606
                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   607
    val thm2 = thm1
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   608
      |> Thm.certify_instantiate (instT, [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   609
      |> Raw_Simplifier.rewrite_rule pre_simps
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   610
    val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   611
    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   612
    val rule = transfer_rule_of_lhs ctxt' t
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   613
    val tac =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   614
      resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   615
      (rtac rule
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   616
        THEN_ALL_NEW
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   617
          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   618
            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   619
        handle TERM (_, ts) => raise TERM (err_msg, ts)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   620
    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   621
    val tnames = map (fst o dest_TFree o snd) instT
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   622
  in
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   623
    thm3
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   624
      |> Raw_Simplifier.rewrite_rule post_simps
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   625
      |> Raw_Simplifier.norm_hhf
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   626
      |> Drule.generalize (tnames, [])
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   627
      |> Drule.zero_var_indexes
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   628
  end
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   629
(*
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   630
    handle THM _ => thm
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   631
*)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   632
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   633
fun untransferred ctxt extra_rules thm =
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   634
  let
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   635
    val start_rule = @{thm untransfer_start}
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   636
    val rules = extra_rules @ get_transfer_raw ctxt
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   637
    val eq_rules = get_relator_eq_raw ctxt
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   638
    val err_msg = "Transfer failed to convert goal to an object-logic formula"
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   639
    val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   640
    val thm1 = Drule.forall_intr_vars thm
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   641
    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   642
                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   643
    val thm2 = thm1
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   644
      |> Thm.certify_instantiate (instT, [])
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   645
      |> Raw_Simplifier.rewrite_rule pre_simps
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   646
    val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   647
    val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   648
    val rule = transfer_rule_of_term ctxt' true t
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   649
    val tac =
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   650
      rtac (thm2 RS start_rule) 1 THEN
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   651
      (rtac rule
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   652
        THEN_ALL_NEW
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   653
          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   654
            THEN_ALL_NEW (DETERM o eq_tac eq_rules)))) 1
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   655
        handle TERM (_, ts) => raise TERM (err_msg, ts)
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   656
    val thm3 = Goal.prove_internal [] @{cpat "Trueprop ?P"} (K tac)
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   657
    val tnames = map (fst o dest_TFree o snd) instT
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   658
  in
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   659
    thm3
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   660
      |> Raw_Simplifier.rewrite_rule post_simps
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   661
      |> Raw_Simplifier.norm_hhf
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   662
      |> Drule.generalize (tnames, [])
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   663
      |> Drule.zero_var_indexes
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   664
  end
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   665
47789
71a526ee569a implement transfer tactic with more scalable forward proof methods
huffman
parents: 47658
diff changeset
   666
(** Methods and attributes **)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   667
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   668
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
   669
  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
   670
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   671
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
   672
  |-- Scan.repeat free) []
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   673
53042
aa0322a65bea standardized aliases;
wenzelm
parents: 52884
diff changeset
   674
fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =
47568
98c8b7542b72 add option to transfer method for specifying variables not to generalize over
huffman
parents: 47523
diff changeset
   675
  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
   676
    SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   677
53042
aa0322a65bea standardized aliases;
wenzelm
parents: 52884
diff changeset
   678
val transfer_prover_method : (Proof.context -> Proof.method) context_parser =
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   679
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   680
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   681
(* Attribute for transfer rules *)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   682
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   683
fun prep_rule ctxt thm = 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   684
  (abstract_domains_transfer o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv) thm
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   685
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   686
val transfer_add =
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   687
  Thm.declaration_attribute (fn thm => fn ctxt => 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   688
    (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   689
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   690
val transfer_del =
52884
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   691
  Thm.declaration_attribute (fn thm => fn ctxt => 
34c47bc771f2 contract equalities in transfer and transfer domain rules when they are registered
kuncar
parents: 52883
diff changeset
   692
    (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   693
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   694
val transfer_attribute =
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   695
  Attrib.add_del transfer_add transfer_del
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   696
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   697
(* Attributes for transfer domain rules *)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   698
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   699
val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   700
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   701
val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   702
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   703
val transfer_domain_attribute =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   704
  Attrib.add_del transfer_domain_add transfer_domain_del
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   705
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   706
(* Attributes for transferred rules *)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   707
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   708
fun transferred_attribute thms = Thm.rule_attribute
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   709
  (fn context => transferred (Context.proof_of context) thms)
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   710
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   711
fun untransferred_attribute thms = Thm.rule_attribute
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   712
  (fn context => untransferred (Context.proof_of context) thms)
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   713
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   714
val transferred_attribute_parser =
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   715
  Attrib.thms >> transferred_attribute
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   716
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   717
val untransferred_attribute_parser =
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   718
  Attrib.thms >> untransferred_attribute
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   719
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   720
(* Theory setup *)
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   721
49975
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   722
val relator_eq_setup =
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   723
  let
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   724
    val name = @{binding relator_eq}
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   725
    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
   726
      #> 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
   727
    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
   728
      #> 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
   729
    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
   730
    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
   731
    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
   732
    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
   733
  in
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   734
    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
   735
    #> 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
   736
  end
faf4afed009f transfer package: more flexible handling of equality relations using is_equality predicate
huffman
parents: 49625
diff changeset
   737
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   738
val relator_domain_setup =
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   739
  let
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   740
    val name = @{binding relator_domain}
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   741
    fun add_thm thm = Data.map (map_relator_domain (Item_Net.update thm))
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   742
      #> add_transfer_domain_thm thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   743
    fun del_thm thm = Data.map (map_relator_domain (Item_Net.remove thm))
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   744
      #> del_transfer_domain_thm thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   745
    val add = Thm.declaration_attribute add_thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   746
    val del = Thm.declaration_attribute del_thm
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   747
    val text = "declaration of relator domain rule (used by transfer method)"
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   748
    val content = Item_Net.content o #relator_domain o Data.get
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   749
  in
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   750
    Attrib.setup name (Attrib.add_del add del) text
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   751
    #> Global_Theory.add_thms_dynamic (name, content)
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   752
  end
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   753
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   754
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   755
val setup =
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   756
  relator_eq_setup
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   757
  #> relator_domain_setup
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   758
  #> Attrib.setup @{binding transfer_rule} transfer_attribute
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   759
     "transfer rule for transfer method"
48064
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   760
  #> Global_Theory.add_thms_dynamic
7bd9e18ce058 unify theory-data structures for transfer package
huffman
parents: 47803
diff changeset
   761
     (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
51956
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   762
  #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute
a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents: 51955
diff changeset
   763
     "transfer domain rule for transfer method"
52354
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   764
  #> Attrib.setup @{binding transferred} transferred_attribute_parser
acb4f932dd24 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
huffman
parents: 51996
diff changeset
   765
     "raw theorem transferred to abstract theorem using transfer rules"
52358
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   766
  #> Attrib.setup @{binding untransferred} untransferred_attribute_parser
f4c4bcb0d564 implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
huffman
parents: 52354
diff changeset
   767
     "abstract theorem transferred to raw theorem using transfer rules"
51437
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   768
  #> Global_Theory.add_thms_dynamic
8739f8abbecb fixing transfer tactic - unfold fully identity relation by using relator_eq
kuncar
parents: 51374
diff changeset
   769
     (@{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
   770
  #> 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
   771
     "generic theorem transfer method"
7631f6f7873d enable variant of transfer method that proves an implication instead of an equivalence
huffman
parents: 47635
diff changeset
   772
  #> Method.setup @{binding transfer'} (transfer_method false)
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   773
     "generic theorem transfer method"
47635
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   774
  #> Method.setup @{binding transfer_prover} transfer_prover_method
ebb79474262c rename 'correspondence' method to 'transfer_prover'
huffman
parents: 47618
diff changeset
   775
     "for proving transfer rules"
47325
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   776
ec6187036495 new transfer proof method
huffman
parents:
diff changeset
   777
end