13 structure Transfer : TRANSFER = |
13 structure Transfer : TRANSFER = |
14 struct |
14 struct |
15 |
15 |
16 (* data administration *) |
16 (* data administration *) |
17 |
17 |
|
18 val direction_of = Thm.dest_binop o Thm.dest_arg o cprop_of; |
|
19 |
18 fun check_morphism_key ctxt key = |
20 fun check_morphism_key ctxt key = |
19 let |
21 let |
20 val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key) |
22 val _ = (Thm.match o pairself Thm.cprop_of) (@{thm transfer_morphismI}, key) |
21 handle Pattern.MATCH => error |
23 handle Pattern.MATCH => error |
22 ("Expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI})); |
24 ("Transfer: expected theorem of the form " ^ quote (Display.string_of_thm ctxt @{thm transfer_morphismI})); |
23 in (Thm.dest_binop o Thm.dest_arg o Thm.cprop_of) key end; |
25 in direction_of key end; |
24 |
26 |
25 type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list, |
27 type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list, |
26 guess : bool, hints : string list }; |
28 guess : bool, hints : string list }; |
27 |
29 |
28 fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry, |
30 fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry, |
33 |
35 |
34 structure Data = Generic_Data |
36 structure Data = Generic_Data |
35 ( |
37 ( |
36 type T = (thm * entry) list; |
38 type T = (thm * entry) list; |
37 val empty = []; |
39 val empty = []; |
38 val extend = I; |
40 val extend = I; |
39 val merge = AList.join Thm.eq_thm (K merge_entry); |
41 val merge = AList.join Thm.eq_thm (K merge_entry); |
40 ); |
42 ); |
41 |
43 |
|
44 |
|
45 (* data lookup *) |
|
46 |
|
47 fun get_by_direction context (a, D) = |
|
48 let |
|
49 val ctxt = Context.proof_of context; |
|
50 val certify = Thm.cterm_of (Context.theory_of context); |
|
51 val a0 = certify a; |
|
52 val D0 = certify D; |
|
53 fun eq_direction ((a, D), thm') = |
|
54 let |
|
55 val (a', D') = direction_of thm'; |
|
56 in a0 aconvc a' andalso D0 aconvc D' end; |
|
57 in case AList.lookup eq_direction (Data.get context) (a, D) of |
|
58 SOME e => ((a0, D0), e) |
|
59 | NONE => error ("Transfer: no such instance: (" |
|
60 ^ Syntax.string_of_term ctxt a ^ ", " ^ Syntax.string_of_term ctxt D ^ ")") |
|
61 end; |
|
62 |
|
63 fun get_by_hints context hints = |
|
64 let |
|
65 val insts = map_filter (fn (k, e) => if exists (member (op =) (#hints e)) hints |
|
66 then SOME (direction_of k, e) else NONE) (Data.get context); |
|
67 val _ = if null insts then error ("Transfer: no such labels: " ^ commas (map quote hints)) else (); |
|
68 in insts end; |
|
69 |
|
70 fun splits P [] = [] |
|
71 | splits P (xs as (x :: _)) = |
|
72 let |
|
73 val (pss, qss) = List.partition (P x) xs; |
|
74 in if null pss then [qss] else if null qss then [pss] else pss :: splits P qss end; |
|
75 |
|
76 fun get_by_prop context t = |
|
77 let |
|
78 val tys = map snd (Term.add_vars t []); |
|
79 val _ = if null tys then error "Transfer: unable to guess instance" else (); |
|
80 val tyss = splits (curry Type.could_unify) tys; |
|
81 val get_ty = typ_of o ctyp_of_term o fst o direction_of; |
|
82 val insts = map_filter (fn tys => get_first (fn (k, ss) => |
|
83 if Type.could_unify (hd tys, range_type (get_ty k)) |
|
84 then SOME (direction_of k, ss) |
|
85 else NONE) (Data.get context)) tyss; |
|
86 val _ = if null insts then |
|
87 error "Transfer: no instances, provide direction or hints explicitly" else (); |
|
88 in insts end; |
|
89 |
|
90 |
|
91 (* applying transfer data *) |
|
92 |
42 val get = Data.get o Context.Proof; |
93 val get = Data.get o Context.Proof; |
43 |
94 |
44 fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, [])); |
95 fun transfer_thm inj_only a0 D0 {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} |
45 |
96 leave ctxt0 th = |
46 val del_attribute = Thm.declaration_attribute del; |
|
47 |
|
48 |
|
49 (* applying transfer data *) |
|
50 |
|
51 fun build_simpset inj_only {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = |
|
52 HOL_ss addsimps inj addsimps (if inj_only then [] else emb @ ret) addcongs cg; |
|
53 |
|
54 fun basic_transfer_rule inj_only a0 D0 e leave ctxt0 th = |
|
55 let |
97 let |
56 val ([a, D], ctxt) = apfst (map Drule.dest_term o snd) |
98 val ([a, D], ctxt) = apfst (map Drule.dest_term o snd) |
57 (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0); |
99 (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0); |
58 val (aT, bT) = |
100 val (aT, bT) = |
59 let val T = typ_of (ctyp_of_term a) |
101 let val T = typ_of (ctyp_of_term a) |
69 val cis = map (Thm.capply a) cfis |
111 val cis = map (Thm.capply a) cfis |
70 val (hs, ctxt''') = Assumption.add_assumes (map (fn ct => |
112 val (hs, ctxt''') = Assumption.add_assumes (map (fn ct => |
71 Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''; |
113 Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''; |
72 val th1 = Drule.cterm_instantiate (cns ~~ cis) th; |
114 val th1 = Drule.cterm_instantiate (cns ~~ cis) th; |
73 val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1); |
115 val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1); |
74 val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' |
116 val simpset = (Simplifier.context ctxt''' HOL_ss) |
75 (build_simpset inj_only e)) (fold_rev implies_intr (map cprop_of hs) th2); |
117 addsimps inj addsimps (if inj_only then [] else emb @ ret) addcongs cg; |
|
118 val th3 = Simplifier.asm_full_simplify simpset |
|
119 (fold_rev implies_intr (map cprop_of hs) th2); |
76 in hd (Variable.export ctxt''' ctxt0 [th3]) end; |
120 in hd (Variable.export ctxt''' ctxt0 [th3]) end; |
77 |
121 |
78 fun transfer_rule (a, D) leave (gctxt, th) = |
122 fun transfer_thm_multiple inj_only insts leave ctxt thm = |
79 let |
123 Conjunction.intr_balanced (map |
80 fun transfer_ruleh a D leave ctxt th = |
124 (fn ((a, D), e) => transfer_thm false a D e leave ctxt thm) insts); |
81 let |
125 |
82 val al = get ctxt; |
126 fun transfer_by_direction (a, D) leave (context, thm) = |
83 val certify = Thm.cterm_of (ProofContext.theory_of ctxt); |
127 let |
84 val a0 = certify a; |
128 val ((a0, D0), e) = get_by_direction context (a, D); |
85 val D0 = certify D; |
129 in (context, transfer_thm false a0 D0 e leave (Context.proof_of context) thm) end; |
86 fun h (th', e) = |
130 |
87 let |
131 fun transfer_by_hints hints leave (context, thm) = |
88 val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' |
132 (context, transfer_thm_multiple false (get_by_hints context hints) |
89 in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE end; |
133 leave (Context.proof_of context) thm); |
90 in case get_first h al of |
134 |
91 SOME e => basic_transfer_rule false a0 D0 e leave ctxt th |
135 fun transfer_by_prop leave (context, thm) = |
92 | NONE => error "Transfer: corresponding instance not found in context data" |
136 (context, transfer_thm_multiple false (get_by_prop context (Thm.prop_of thm)) |
93 end; |
137 leave (Context.proof_of context) thm); |
94 in |
138 |
95 (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th) |
139 fun transferred_attribute [] NONE leave = transfer_by_prop leave |
96 end; |
140 | transferred_attribute hints NONE leave = transfer_by_hints hints leave |
97 |
141 | transferred_attribute _ (SOME (a, D)) leave = transfer_by_direction (a, D) leave; |
98 fun splits P [] = [] |
142 |
99 | splits P (xxs as (x :: xs)) = |
143 |
100 let |
144 (* maintaining transfer data *) |
101 val pss = filter (P x) xxs; |
|
102 val qss = filter_out (P x) xxs; |
|
103 in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss end; |
|
104 |
|
105 fun all_transfers leave (gctxt, th) = |
|
106 let |
|
107 val ctxt = Context.proof_of gctxt; |
|
108 val tys = map snd (Term.add_vars (prop_of th) []); |
|
109 val _ = if null tys then error "transfer: Unable to guess instance" else (); |
|
110 val tyss = splits (curry Type.could_unify) tys; |
|
111 val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of; |
|
112 val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of; |
|
113 val insts = |
|
114 map_filter (fn tys => |
|
115 get_first (fn (k,ss) => |
|
116 if Type.could_unify (hd tys, range_type (get_ty k)) |
|
117 then SOME (get_aD k, ss) |
|
118 else NONE) (get ctxt)) tyss; |
|
119 val _ = |
|
120 if null insts then |
|
121 error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" |
|
122 else (); |
|
123 val ths = map (fn ((a, D), e) => basic_transfer_rule false a D e leave ctxt th) insts; |
|
124 val cth = Conjunction.intr_balanced ths; |
|
125 in (gctxt, cth) end; |
|
126 |
|
127 fun transfer_rule_by_hint ls leave (gctxt, th) = |
|
128 let |
|
129 val ctxt = Context.proof_of gctxt; |
|
130 val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of; |
|
131 val insts = map_filter (fn (k,e) => if exists (member (op =) (#hints e)) ls |
|
132 then SOME (get_aD k, e) else NONE) (get ctxt); |
|
133 val _ = if null insts then error "Transfer: No labels provided are stored in the context" else (); |
|
134 val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts; |
|
135 val cth = Conjunction.intr_balanced ths; |
|
136 in (gctxt, cth) end; |
|
137 |
|
138 fun transferred_attribute ls NONE leave = |
|
139 if null ls then all_transfers leave else transfer_rule_by_hint ls leave |
|
140 | transferred_attribute _ (SOME (a, D)) leave = transfer_rule (a, D) leave; |
|
141 |
|
142 |
|
143 (* adding transfer data *) |
|
144 |
145 |
145 fun merge_update eq m (k, v) [] = [(k, v)] |
146 fun merge_update eq m (k, v) [] = [(k, v)] |
146 | merge_update eq m (k, v) ((k', v') :: al) = |
147 | merge_update eq m (k, v) ((k', v') :: al) = |
147 if eq (k, k') then (k', m (v, v')) :: al else (k', v') :: merge_update eq m (k, v) al; |
148 if eq (k, k') then (k', m (v, v')) :: al else (k', v') :: merge_update eq m (k, v) al; |
148 |
149 |
171 val inj' = if null inja then #inj |
172 val inj' = if null inja then #inj |
172 (case AList.lookup Thm.eq_thm al key of SOME e => e |
173 (case AList.lookup Thm.eq_thm al key of SOME e => e |
173 | NONE => error "Transfer: cannot generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") |
174 | NONE => error "Transfer: cannot generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") |
174 else inja |
175 else inja |
175 val ret' = merge Thm.eq_thm (reta, map |
176 val ret' = merge Thm.eq_thm (reta, map |
176 (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, |
177 (fn th => transfer_thm true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, |
177 hints = hintsa} [] ctxt0 th RS sym) emba); |
178 hints = hintsa} [] ctxt0 th RS sym) emba); |
178 in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end |
179 in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end |
179 else e0; |
180 else e0; |
180 in merge_update Thm.eq_thm (merge_entries ed) (key, entry) al end); |
181 in merge_update Thm.eq_thm (merge_entries ed) (key, entry) al end); |
181 |
182 |
182 fun add_attribute args = Thm.declaration_attribute (add args); |
183 fun add_attribute args = Thm.declaration_attribute (add args); |
|
184 |
|
185 fun del key = Data.map (remove (eq_fst Thm.eq_thm) (key, [])); |
|
186 |
|
187 val del_attribute = Thm.declaration_attribute del; |
183 |
188 |
184 |
189 |
185 (* syntax *) |
190 (* syntax *) |
186 |
191 |
187 local |
192 local |