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