author | wenzelm |
Wed, 16 Dec 2015 16:31:36 +0100 | |
changeset 61853 | fb7756087101 |
parent 61476 | 1884c40f1539 |
child 66795 | 420d0080545f |
permissions | -rw-r--r-- |
47455 | 1 |
(* Title: HOL/Tools/legacy_transfer.ML |
37744 | 2 |
Author: Amine Chaieb, University of Cambridge, 2009 |
47455 | 3 |
Author: Jeremy Avigad, Carnegie Mellon University |
4 |
Author: Florian Haftmann, TU Muenchen |
|
35648 | 5 |
|
6 |
Simple transfer principle on theorems. |
|
31706 | 7 |
*) |
8 |
||
47324
ed2bad9b7c6a
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
huffman
parents:
46497
diff
changeset
|
9 |
signature LEGACY_TRANSFER = |
31706 | 10 |
sig |
35648 | 11 |
datatype selection = Direction of term * term | Hints of string list | Prop |
35674 | 12 |
val transfer: Context.generic -> selection -> string list -> thm -> thm list |
31706 | 13 |
type entry |
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
14 |
val add: thm -> bool -> entry -> Context.generic -> Context.generic |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
15 |
val del: thm -> entry -> Context.generic -> Context.generic |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
16 |
val drop: thm -> Context.generic -> Context.generic |
31706 | 17 |
end; |
18 |
||
47324
ed2bad9b7c6a
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
huffman
parents:
46497
diff
changeset
|
19 |
structure Legacy_Transfer : LEGACY_TRANSFER = |
31706 | 20 |
struct |
32557
3cfe4c13aa6e
plain structure name; signature constraint; shorter lines
haftmann
parents:
32476
diff
changeset
|
21 |
|
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
22 |
(* data administration *) |
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
23 |
|
59582 | 24 |
val direction_of = Thm.dest_binop o Thm.dest_arg o Thm.cprop_of; |
35647 | 25 |
|
35821 | 26 |
val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI}); |
27 |
||
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
28 |
fun check_morphism_key ctxt key = |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
29 |
let |
35821 | 30 |
val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key) |
31 |
handle Pattern.MATCH => error ("Transfer: expected theorem of the form " |
|
32 |
^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key))); |
|
35647 | 33 |
in direction_of key end; |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
34 |
|
35674 | 35 |
type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list, |
35675 | 36 |
hints : string list }; |
33321 | 37 |
|
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
38 |
val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] }; |
35675 | 39 |
fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry, |
40 |
{ inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) = |
|
35674 | 41 |
{ inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2), |
42 |
return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2), |
|
35675 | 43 |
hints = merge (op =) (hints1, hints2) }; |
33321 | 44 |
|
33519 | 45 |
structure Data = Generic_Data |
31706 | 46 |
( |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
47 |
type T = (thm * entry) list; |
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
48 |
val empty = []; |
35647 | 49 |
val extend = I; |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
50 |
val merge = AList.join Thm.eq_thm (K merge_entry); |
31706 | 51 |
); |
52 |
||
35647 | 53 |
|
54 |
(* data lookup *) |
|
55 |
||
35708 | 56 |
fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) = |
35675 | 57 |
(inj, embed, return, cong); |
58 |
||
35647 | 59 |
fun get_by_direction context (a, D) = |
60 |
let |
|
61 |
val ctxt = Context.proof_of context; |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
62 |
val a0 = Thm.cterm_of ctxt a; |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
63 |
val D0 = Thm.cterm_of ctxt D; |
35647 | 64 |
fun eq_direction ((a, D), thm') = |
65 |
let |
|
66 |
val (a', D') = direction_of thm'; |
|
35674 | 67 |
in a aconvc a' andalso D aconvc D' end; |
68 |
in case AList.lookup eq_direction (Data.get context) (a0, D0) of |
|
35675 | 69 |
SOME e => ((a0, D0), transfer_rules_of e) |
35647 | 70 |
| NONE => error ("Transfer: no such instance: (" |
71 |
^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")") |
|
72 |
end; |
|
31706 | 73 |
|
35647 | 74 |
fun get_by_hints context hints = |
75 |
let |
|
76 |
val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints |
|
35675 | 77 |
then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context); |
45430 | 78 |
val _ = if null insts then error ("Transfer: no such labels: " ^ commas_quote hints) else (); |
35647 | 79 |
in insts end; |
80 |
||
81 |
fun splits P [] = [] |
|
82 |
| splits P (xs as (x :: _)) = |
|
83 |
let |
|
84 |
val (pss, qss) = List.partition (P x) xs; |
|
85 |
in if null pss then [qss] else if null qss then [pss] else pss :: splits P qss end; |
|
31706 | 86 |
|
35647 | 87 |
fun get_by_prop context t = |
88 |
let |
|
89 |
val tys = map snd (Term.add_vars t []); |
|
90 |
val _ = if null tys then error "Transfer: unable to guess instance" else (); |
|
91 |
val tyss = splits (curry Type.could_unify) tys; |
|
59586 | 92 |
val get_ty = Thm.typ_of_cterm o fst o direction_of; |
35675 | 93 |
val insts = map_filter (fn tys => get_first (fn (k, e) => |
35647 | 94 |
if Type.could_unify (hd tys, range_type (get_ty k)) |
35675 | 95 |
then SOME (direction_of k, transfer_rules_of e) |
35647 | 96 |
else NONE) (Data.get context)) tyss; |
97 |
val _ = if null insts then |
|
98 |
error "Transfer: no instances, provide direction or hints explicitly" else (); |
|
99 |
in insts end; |
|
31706 | 100 |
|
101 |
||
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
102 |
(* applying transfer data *) |
31706 | 103 |
|
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
104 |
fun transfer_thm ((raw_a, raw_D), (inj, embed, return, cong)) leave ctxt1 thm = |
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
105 |
let |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
106 |
(* identify morphism function *) |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
107 |
val ([a, D], ctxt2) = ctxt1 |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
108 |
|> Variable.import true (map Drule.mk_term [raw_a, raw_D]) |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
109 |
|>> map Drule.dest_term o snd; |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45620
diff
changeset
|
110 |
val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D; |
59586 | 111 |
val T = Thm.typ_of_cterm a; |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
112 |
val (aT, bT) = (Term.range_type T, Term.domain_type T); |
58824 | 113 |
|
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
114 |
(* determine variables to transfer *) |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
115 |
val ctxt3 = ctxt2 |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
116 |
|> Variable.declare_thm thm |
59582 | 117 |
|> Variable.declare_term (Thm.term_of a) |
118 |
|> Variable.declare_term (Thm.term_of D); |
|
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
119 |
val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
120 |
not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []); |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
121 |
val c_vars = map (Thm.cterm_of ctxt3 o Var) vars; |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
122 |
val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3; |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
123 |
val c_vars' = map (Thm.cterm_of ctxt3 o (fn v => Free (v, bT))) vs'; |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45620
diff
changeset
|
124 |
val c_exprs' = map (Thm.apply a) c_vars'; |
31706 | 125 |
|
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
126 |
(* transfer *) |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
127 |
val (hyps, ctxt5) = ctxt4 |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
128 |
|> Assumption.add_assumes (map transform c_vars'); |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45430
diff
changeset
|
129 |
val simpset = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47455
diff
changeset
|
130 |
put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return) |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45430
diff
changeset
|
131 |
|> fold Simplifier.add_cong cong; |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
132 |
val thm' = thm |
60784 | 133 |
|> infer_instantiate ctxt5 (map (#1 o dest_Var o Thm.term_of) c_vars ~~ c_exprs') |
59582 | 134 |
|> fold_rev Thm.implies_intr (map Thm.cprop_of hyps) |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
135 |
|> Simplifier.asm_full_simplify simpset |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
136 |
in singleton (Variable.export ctxt5 ctxt1) thm' end; |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
137 |
|
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
138 |
fun transfer_thm_multiple insts leave ctxt thm = |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
139 |
map (fn inst => transfer_thm inst leave ctxt thm) insts; |
31706 | 140 |
|
35648 | 141 |
datatype selection = Direction of term * term | Hints of string list | Prop; |
35647 | 142 |
|
35648 | 143 |
fun insts_for context thm (Direction direction) = [get_by_direction context direction] |
144 |
| insts_for context thm (Hints hints) = get_by_hints context hints |
|
145 |
| insts_for context thm Prop = get_by_prop context (Thm.prop_of thm); |
|
31706 | 146 |
|
35648 | 147 |
fun transfer context selection leave thm = |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
148 |
transfer_thm_multiple (insts_for context thm selection) leave (Context.proof_of context) thm; |
31706 | 149 |
|
150 |
||
35647 | 151 |
(* maintaining transfer data *) |
31706 | 152 |
|
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
153 |
fun extend_entry ctxt (a, D) guess |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
154 |
{ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
155 |
{ inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
156 |
let |
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
157 |
fun add_del eq del add = union eq add #> subtract eq del; |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
158 |
val guessed = if guess |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
159 |
then map (fn thm => transfer_thm |
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
160 |
((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1 |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
161 |
else []; |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
162 |
in |
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
163 |
{ inj = union Thm.eq_thm inj1 inj2, embed = union Thm.eq_thm embed1 embed2, |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
164 |
return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2), |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
165 |
cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 } |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
166 |
end; |
31706 | 167 |
|
58824 | 168 |
fun diminish_entry |
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
169 |
{ inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 } |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
170 |
{ inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
171 |
{ inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2, |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
172 |
return = subtract Thm.eq_thm return0 return2, cong = subtract Thm.eq_thm cong0 cong2, |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
173 |
hints = subtract (op =) hints0 hints2 }; |
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
174 |
|
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
175 |
fun add key guess entry context = |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
176 |
let |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
177 |
val ctxt = Context.proof_of context; |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
178 |
val a_D = check_morphism_key ctxt key; |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
179 |
in |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
180 |
context |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
181 |
|> Data.map (AList.map_default Thm.eq_thm |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
182 |
(key, empty_entry) (extend_entry ctxt a_D guess entry)) |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
183 |
end; |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
184 |
|
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
185 |
fun del key entry = Data.map (AList.map_entry Thm.eq_thm key (diminish_entry entry)); |
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
186 |
|
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset
|
187 |
fun drop key = Data.map (AList.delete Thm.eq_thm key); |
35647 | 188 |
|
31706 | 189 |
|
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset
|
190 |
(* syntax *) |
31706 | 191 |
|
192 |
local |
|
193 |
||
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
194 |
fun these scan = Scan.optional scan []; |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
195 |
fun these_pair scan = Scan.optional scan ([], []); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
196 |
|
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
197 |
fun keyword k = Scan.lift (Args.$$$ k) >> K (); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
198 |
fun keyword_colon k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
31706 | 199 |
|
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
200 |
val addN = "add"; |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
201 |
val delN = "del"; |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
202 |
val keyN = "key"; |
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
203 |
val modeN = "mode"; |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
204 |
val automaticN = "automatic"; |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
205 |
val manualN = "manual"; |
35674 | 206 |
val injN = "inj"; |
207 |
val embedN = "embed"; |
|
208 |
val returnN = "return"; |
|
209 |
val congN = "cong"; |
|
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
210 |
val labelsN = "labels"; |
31706 | 211 |
|
35674 | 212 |
val leavingN = "leaving"; |
213 |
val directionN = "direction"; |
|
214 |
||
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
215 |
val any_keyword = keyword_colon addN || keyword_colon delN || keyword_colon keyN |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
216 |
|| keyword_colon modeN || keyword_colon injN || keyword_colon embedN || keyword_colon returnN |
35674 | 217 |
|| keyword_colon congN || keyword_colon labelsN |
218 |
|| keyword_colon leavingN || keyword_colon directionN; |
|
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
219 |
|
61476 | 220 |
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
221 |
val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name)) |
31706 | 222 |
|
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
223 |
val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
224 |
|| (Scan.lift (Args.$$$ automaticN) >> K true)); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
225 |
val inj = (keyword_colon injN |-- thms) -- these (keyword_colon delN |-- thms); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
226 |
val embed = (keyword_colon embedN |-- thms) -- these (keyword_colon delN |-- thms); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
227 |
val return = (keyword_colon returnN |-- thms) -- these (keyword_colon delN |-- thms); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
228 |
val cong = (keyword_colon congN |-- thms) -- these (keyword_colon delN |-- thms); |
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
229 |
val labels = (keyword_colon labelsN |-- names) -- these (keyword_colon delN |-- names); |
31706 | 230 |
|
35675 | 231 |
val entry_pair = these_pair inj -- these_pair embed |
35648 | 232 |
-- these_pair return -- these_pair cong -- these_pair labels |
35675 | 233 |
>> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)), |
35674 | 234 |
(hintsa, hintsd)) => |
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
235 |
({ inj = inja, embed = embeda, return = returna, cong = conga, hints = hintsa }, |
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset
|
236 |
{ inj = injd, embed = embedd, return = returnd, cong = congd, hints = hintsd })); |
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
237 |
|
35648 | 238 |
val selection = (keyword_colon directionN |-- (Args.term -- Args.term) >> Direction) |
239 |
|| these names >> (fn hints => if null hints then Prop else Hints hints); |
|
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset
|
240 |
|
31706 | 241 |
in |
242 |
||
58824 | 243 |
val _ = |
244 |
Theory.setup |
|
245 |
(Attrib.setup @{binding transfer} |
|
246 |
(keyword delN >> K (Thm.declaration_attribute drop) |
|
247 |
|| keyword addN |-- Scan.optional mode true -- entry_pair |
|
248 |
>> (fn (guess, (entry_add, entry_del)) => |
|
249 |
Thm.declaration_attribute (fn thm => add thm guess entry_add #> del thm entry_del)) |
|
250 |
|| keyword_colon keyN |-- Attrib.thm |
|
251 |
>> (fn key => Thm.declaration_attribute (fn thm => |
|
252 |
add key false { inj = [], embed = [], return = [thm], cong = [], hints = [] }))) |
|
253 |
"install transfer data" #> |
|
254 |
Attrib.setup @{binding transferred} |
|
255 |
(selection -- these (keyword_colon leavingN |-- names) |
|
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61476
diff
changeset
|
256 |
>> (fn (selection, leave) => Thm.rule_attribute [] (fn context => |
58824 | 257 |
Conjunction.intr_balanced o transfer context selection leave))) |
258 |
"transfer theorems"); |
|
31706 | 259 |
|
260 |
end; |
|
261 |
||
262 |
end; |