author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 35821  ee34f03a7d26 
child 42361  23f352990944 
permissions  rwrr 
37744  1 
(* Title: HOL/Tools/transfer.ML 
2 
Author: Amine Chaieb, University of Cambridge, 2009 

3 
Jeremy Avigad, Carnegie Mellon University 

4 
Florian Haftmann, TU Muenchen 

35648  5 

6 
Simple transfer principle on theorems. 

31706  7 
*) 
8 

32557
3cfe4c13aa6e
plain structure name; signature constraint; shorter lines
haftmann
parents:
32476
diff
changeset

9 
signature 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 
val setup: theory > theory 
18 
end; 

19 

32557
3cfe4c13aa6e
plain structure name; signature constraint; shorter lines
haftmann
parents:
32476
diff
changeset

20 
structure Transfer : TRANSFER = 
31706  21 
struct 
32557
3cfe4c13aa6e
plain structure name; signature constraint; shorter lines
haftmann
parents:
32476
diff
changeset

22 

35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

23 
(* data administration *) 
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

24 

35647  25 
val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of; 
26 

35821  27 
val transfer_morphism_key = Drule.strip_imp_concl (Thm.cprop_of @{thm transfer_morphismI}); 
28 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

29 
fun check_morphism_key ctxt key = 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

30 
let 
35821  31 
val _ = Thm.match (transfer_morphism_key, Thm.cprop_of key) 
32 
handle Pattern.MATCH => error ("Transfer: expected theorem of the form " 

33 
^ quote (Syntax.string_of_term ctxt (Thm.term_of transfer_morphism_key))); 

35647  34 
in direction_of key end; 
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

35 

35674  36 
type entry = { inj : thm list, embed : thm list, return : thm list, cong : thm list, 
35675  37 
hints : string list }; 
33321  38 

35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

39 
val empty_entry = { inj = [], embed = [], return = [], cong = [], hints = [] }; 
35675  40 
fun merge_entry ({ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } : entry, 
41 
{ inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } : entry) = 

35674  42 
{ inj = merge Thm.eq_thm (inj1, inj2), embed = merge Thm.eq_thm (embed1, embed2), 
43 
return = merge Thm.eq_thm (return1, return2), cong = merge Thm.eq_thm (cong1, cong2), 

35675  44 
hints = merge (op =) (hints1, hints2) }; 
33321  45 

33519  46 
structure Data = Generic_Data 
31706  47 
( 
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

48 
type T = (thm * entry) list; 
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

49 
val empty = []; 
35647  50 
val extend = I; 
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

51 
val merge = AList.join Thm.eq_thm (K merge_entry); 
31706  52 
); 
53 

35647  54 

55 
(* data lookup *) 

56 

35708  57 
fun transfer_rules_of ({ inj, embed, return, cong, ... } : entry) = 
35675  58 
(inj, embed, return, cong); 
59 

35647  60 
fun get_by_direction context (a, D) = 
61 
let 

62 
val ctxt = Context.proof_of context; 

63 
val certify = Thm.cterm_of (Context.theory_of context); 

64 
val a0 = certify a; 

65 
val D0 = certify D; 

66 
fun eq_direction ((a, D), thm') = 

67 
let 

68 
val (a', D') = direction_of thm'; 

35674  69 
in a aconvc a' andalso D aconvc D' end; 
70 
in case AList.lookup eq_direction (Data.get context) (a0, D0) of 

35675  71 
SOME e => ((a0, D0), transfer_rules_of e) 
35647  72 
 NONE => error ("Transfer: no such instance: (" 
73 
^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")") 

74 
end; 

31706  75 

35647  76 
fun get_by_hints context hints = 
77 
let 

78 
val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints 

35675  79 
then SOME (direction_of k, transfer_rules_of e) else NONE) (Data.get context); 
35647  80 
val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else (); 
81 
in insts end; 

82 

83 
fun splits P [] = [] 

84 
 splits P (xs as (x :: _)) = 

85 
let 

86 
val (pss, qss) = List.partition (P x) xs; 

87 
in if null pss then [qss] else if null qss then [pss] else pss :: splits P qss end; 

31706  88 

35647  89 
fun get_by_prop context t = 
90 
let 

91 
val tys = map snd (Term.add_vars t []); 

92 
val _ = if null tys then error "Transfer: unable to guess instance" else (); 

93 
val tyss = splits (curry Type.could_unify) tys; 

94 
val get_ty = typ_of o ctyp_of_term o fst o direction_of; 

35675  95 
val insts = map_filter (fn tys => get_first (fn (k, e) => 
35647  96 
if Type.could_unify (hd tys, range_type (get_ty k)) 
35675  97 
then SOME (direction_of k, transfer_rules_of e) 
35647  98 
else NONE) (Data.get context)) tyss; 
99 
val _ = if null insts then 

100 
error "Transfer: no instances, provide direction or hints explicitly" else (); 

101 
in insts end; 

31706  102 

103 

35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

104 
(* applying transfer data *) 
31706  105 

35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

106 
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

107 
let 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

108 
(* identify morphism function *) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

109 
val ([a, D], ctxt2) = ctxt1 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

110 
> 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

111 
>> map Drule.dest_term o snd; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

112 
val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

113 
val T = Thm.typ_of (Thm.ctyp_of_term a); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

114 
val (aT, bT) = (Term.range_type T, Term.domain_type T); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

115 

97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

116 
(* determine variables to transfer *) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

117 
val ctxt3 = ctxt2 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

118 
> Variable.declare_thm thm 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

119 
> Variable.declare_term (term_of a) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

120 
> Variable.declare_term (term_of D); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

121 
val certify = Thm.cterm_of (ProofContext.theory_of ctxt3); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

122 
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

123 
not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

124 
val c_vars = map (certify o Var) vars; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

125 
val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

126 
val c_vars' = map (certify o (fn v => Free (v, bT))) vs'; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

127 
val c_exprs' = map (Thm.capply a) c_vars'; 
31706  128 

35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

129 
(* transfer *) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

130 
val (hyps, ctxt5) = ctxt4 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

131 
> Assumption.add_assumes (map transform c_vars'); 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

132 
val simpset = Simplifier.context ctxt5 HOL_ss 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

133 
addsimps (inj @ embed @ return) addcongs cong; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

134 
val thm' = thm 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

135 
> Drule.cterm_instantiate (c_vars ~~ c_exprs') 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

136 
> fold_rev Thm.implies_intr (map cprop_of hyps) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

137 
> Simplifier.asm_full_simplify simpset 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

138 
in singleton (Variable.export ctxt5 ctxt1) thm' end; 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

139 

97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

140 
fun transfer_thm_multiple insts leave ctxt thm = 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

141 
map (fn inst => transfer_thm inst leave ctxt thm) insts; 
31706  142 

35648  143 
datatype selection = Direction of term * term  Hints of string list  Prop; 
35647  144 

35648  145 
fun insts_for context thm (Direction direction) = [get_by_direction context direction] 
146 
 insts_for context thm (Hints hints) = get_by_hints context hints 

147 
 insts_for context thm Prop = get_by_prop context (Thm.prop_of thm); 

31706  148 

35648  149 
fun transfer context selection leave thm = 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

150 
transfer_thm_multiple (insts_for context thm selection) leave (Context.proof_of context) thm; 
31706  151 

152 

35647  153 
(* maintaining transfer data *) 
31706  154 

35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

155 
fun extend_entry ctxt (a, D) guess 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

156 
{ inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

157 
{ 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

158 
let 
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

159 
fun add_del eq del add = union eq add #> subtract eq del; 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

160 
val guessed = if guess 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

161 
then map (fn thm => transfer_thm 
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

162 
((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

163 
else []; 
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

164 
in 
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

165 
{ 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

166 
return = union Thm.eq_thm guessed (union Thm.eq_thm return1 return2), 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

167 
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

168 
end; 
31706  169 

35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

170 
fun diminish_entry 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

171 
{ inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 } 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

172 
{ inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

173 
{ 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

174 
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

175 
hints = subtract (op =) hints0 hints2 }; 
35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

176 

35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

177 
fun add key guess entry context = 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

178 
let 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

179 
val ctxt = Context.proof_of context; 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

180 
val a_D = check_morphism_key ctxt key; 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

181 
in 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

182 
context 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

183 
> Data.map (AList.map_default Thm.eq_thm 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

184 
(key, empty_entry) (extend_entry ctxt a_D guess entry)) 
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

185 
end; 
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 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

188 

9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

189 
fun drop key = Data.map (AList.delete Thm.eq_thm key); 
35647  190 

31706  191 

35638
50655e2ebc85
dropped dead code; adhere more closely to standard coding conventions
haftmann
parents:
33519
diff
changeset

192 
(* syntax *) 
31706  193 

194 
local 

195 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

196 
fun these scan = Scan.optional scan []; 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

197 
fun these_pair scan = Scan.optional scan ([], []); 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

198 

74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

199 
fun keyword k = Scan.lift (Args.$$$ k) >> K (); 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

200 
fun keyword_colon k = Scan.lift (Args.$$$ k  Args.colon) >> K (); 
31706  201 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

202 
val addN = "add"; 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

203 
val delN = "del"; 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

204 
val keyN = "key"; 
35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

205 
val modeN = "mode"; 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

206 
val automaticN = "automatic"; 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

207 
val manualN = "manual"; 
35674  208 
val injN = "inj"; 
209 
val embedN = "embed"; 

210 
val returnN = "return"; 

211 
val congN = "cong"; 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

212 
val labelsN = "labels"; 
31706  213 

35674  214 
val leavingN = "leaving"; 
215 
val directionN = "direction"; 

216 

35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

217 
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

218 
 keyword_colon modeN  keyword_colon injN  keyword_colon embedN  keyword_colon returnN 
35674  219 
 keyword_colon congN  keyword_colon labelsN 
220 
 keyword_colon leavingN  keyword_colon directionN; 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

221 

74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

222 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

223 
val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name)) 
31706  224 

35645
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

225 
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

226 
 (Scan.lift (Args.$$$ automaticN) >> K true)); 
74e4542d0a4a
transfer: avoid camel case, more standard coding conventions, misc tuning
haftmann
parents:
35638
diff
changeset

227 
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

228 
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

229 
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

230 
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

231 
val labels = (keyword_colon labelsN  names)  these (keyword_colon delN  names); 
31706  232 

35675  233 
val entry_pair = these_pair inj  these_pair embed 
35648  234 
 these_pair return  these_pair cong  these_pair labels 
35675  235 
>> (fn (((((inja, injd), (embeda, embedd)), (returna, returnd)), (conga, congd)), 
35674  236 
(hintsa, hintsd)) => 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

237 
({ 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

238 
{ 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

239 

35648  240 
val selection = (keyword_colon directionN  (Args.term  Args.term) >> Direction) 
241 
 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

242 

31706  243 
in 
244 

35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

245 
val transfer_attribute = keyword delN >> K (Thm.declaration_attribute drop) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

246 
 keyword addN  Scan.optional mode true  entry_pair 
35676
9fa8548d043d
data administration using canonical functorial operations
haftmann
parents:
35675
diff
changeset

247 
>> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute 
35684
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

248 
(fn thm => add thm guess entry_add #> del thm entry_del)) 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

249 
 keyword_colon keyN  Attrib.thm 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

250 
>> (fn key => Thm.declaration_attribute 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

251 
(fn thm => add key false 
97b94dc975c7
clarified transfer code proper; more natural declaration of return rules
haftmann
parents:
35676
diff
changeset

252 
{ inj = [], embed = [], return = [thm], cong = [], hints = [] })); 
31706  253 

35648  254 
val transferred_attribute = selection  these (keyword_colon leavingN  names) 
35674  255 
>> (fn (selection, leave) => Thm.rule_attribute (fn context => 
256 
Conjunction.intr_balanced o transfer context selection leave)); 

31706  257 

258 
end; 

259 

260 

261 
(* theory setup *) 

262 

263 
val setup = 

35648  264 
Attrib.setup @{binding transfer} transfer_attribute 
31706  265 
"Installs transfer data" #> 
35648  266 
Attrib.setup @{binding transferred} transferred_attribute 
31706  267 
"Transfers theorems"; 
268 

269 
end; 