16 val extra_hyps: Proof.context -> thm -> term list |
16 val extra_hyps: Proof.context -> thm -> term list |
17 val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context |
17 val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context |
18 val add_assumes: cterm list -> Proof.context -> thm list * Proof.context |
18 val add_assumes: cterm list -> Proof.context -> thm list * Proof.context |
19 val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context |
19 val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context |
20 val export: bool -> Proof.context -> Proof.context -> thm -> thm |
20 val export: bool -> Proof.context -> Proof.context -> thm -> thm |
|
21 val export_term: Proof.context -> Proof.context -> term -> term |
21 val export_morphism: Proof.context -> Proof.context -> morphism |
22 val export_morphism: Proof.context -> Proof.context -> morphism |
22 end; |
23 end; |
23 |
24 |
24 structure Assumption: ASSUMPTION = |
25 structure Assumption: ASSUMPTION = |
25 struct |
26 struct |
26 |
27 |
27 (** basic rules **) |
28 (** basic rules **) |
28 |
29 |
29 type export = bool -> cterm list -> thm -> thm |
30 type export = bool -> cterm list -> (thm -> thm) * (term -> term); |
30 |
31 |
31 (* |
32 (* |
32 [A] |
33 [A] |
33 : |
34 : |
34 B |
35 B |
35 -------- |
36 -------- |
36 #A ==> B |
37 #A ==> B |
37 *) |
38 *) |
38 fun assume_export true = Drule.implies_intr_protected |
39 fun assume_export is_goal asms = |
39 | assume_export false = Drule.implies_intr_list; |
40 (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t); |
40 |
41 |
41 (* |
42 (* |
42 [A] |
43 [A] |
43 : |
44 : |
44 B |
45 B |
96 in (asms', prems) end); |
97 in (asms', prems) end); |
97 |
98 |
98 |
99 |
99 (* export *) |
100 (* export *) |
100 |
101 |
|
102 fun diff_assms inner outer = |
|
103 Library.drop (length (assumptions_of outer), assumptions_of inner); |
|
104 |
101 fun export is_goal inner outer = |
105 fun export is_goal inner outer = |
102 let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in |
106 let val asms = diff_assms inner outer in |
103 MetaSimplifier.norm_hhf_protect |
107 MetaSimplifier.norm_hhf_protect |
104 #> fold_rev (fn (e, As) => e is_goal As) asms |
108 #> fold_rev (fn (e, As) => #1 (e is_goal As)) asms |
105 #> MetaSimplifier.norm_hhf_protect |
109 #> MetaSimplifier.norm_hhf_protect |
106 end; |
110 end; |
|
111 |
|
112 fun export_term inner outer = |
|
113 fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer); |
107 |
114 |
108 fun export_morphism inner outer = |
115 fun export_morphism inner outer = |
109 let |
116 let |
110 val thm = export false inner outer; |
117 val thm = export false inner outer; |
111 fun term t = Drule.term_rule (ProofContext.theory_of inner (*delayed until now*)) thm t; |
118 val term = export_term inner outer; |
112 val typ = Logic.type_map term; |
119 val typ = Logic.type_map term; |
113 in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end; |
120 in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end; |
114 |
121 |
115 end; |
122 end; |