15 val all_prems_of: Proof.context -> thm list |
15 val all_prems_of: Proof.context -> thm list |
16 val local_assms_of: Proof.context -> Proof.context -> cterm list |
16 val local_assms_of: Proof.context -> Proof.context -> cterm list |
17 val local_prems_of: Proof.context -> Proof.context -> thm list |
17 val local_prems_of: Proof.context -> Proof.context -> thm list |
18 val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context |
18 val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context |
19 val add_assumes: cterm list -> Proof.context -> thm list * Proof.context |
19 val add_assumes: cterm list -> Proof.context -> thm list * Proof.context |
|
20 val export_term: Proof.context -> Proof.context -> term -> term |
20 val export: bool -> Proof.context -> Proof.context -> thm -> thm |
21 val export: bool -> Proof.context -> Proof.context -> thm -> thm |
21 val export_term: Proof.context -> Proof.context -> term -> term |
|
22 val export_morphism: Proof.context -> Proof.context -> morphism |
22 val export_morphism: Proof.context -> Proof.context -> morphism |
23 end; |
23 end; |
24 |
24 |
25 structure Assumption: ASSUMPTION = |
25 structure Assumption: ASSUMPTION = |
26 struct |
26 struct |
126 val add_assumes = add_assms assume_export; |
126 val add_assumes = add_assms assume_export; |
127 |
127 |
128 |
128 |
129 (* export *) |
129 (* export *) |
130 |
130 |
131 fun export is_goal inner outer = |
|
132 Raw_Simplifier.norm_hhf_protect_without_context #> |
|
133 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> |
|
134 Raw_Simplifier.norm_hhf_protect_without_context; |
|
135 |
|
136 fun export_term inner outer = |
131 fun export_term inner outer = |
137 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
132 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
138 |
133 |
|
134 fun export_thm is_goal inner outer = |
|
135 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer); |
|
136 |
|
137 fun export is_goal inner outer = |
|
138 Raw_Simplifier.norm_hhf_protect inner #> |
|
139 export_thm is_goal inner outer #> |
|
140 Raw_Simplifier.norm_hhf_protect outer; |
|
141 |
139 fun export_morphism inner outer = |
142 fun export_morphism inner outer = |
140 let |
143 let |
141 val thm = export false inner outer; |
144 val export0 = export_thm false inner outer; |
|
145 fun thm thy = |
|
146 let val norm = norm_hhf_protect (Proof_Context.init_global thy) |
|
147 in norm #> export0 #> norm end; |
142 val term = export_term inner outer; |
148 val term = export_term inner outer; |
143 val typ = Logic.type_map term; |
149 val typ = Logic.type_map term; |
144 in |
150 in |
145 Morphism.morphism "Assumption.export" |
151 Morphism.morphism "Assumption.export" |
146 {binding = [], typ = [K typ], term = [K term], fact = [K (map thm)]} |
152 {binding = [], typ = [K typ], term = [K term], fact = [map o thm o Morphism.the_theory]} |
|
153 |> Morphism.set_context (Proof_Context.theory_of inner) |
147 end; |
154 end; |
148 |
155 |
149 end; |
156 end; |