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