7 signature ASSUMPTION = |
7 signature ASSUMPTION = |
8 sig |
8 sig |
9 type export = bool -> cterm list -> (thm -> thm) * (term -> term) |
9 type export = bool -> cterm list -> (thm -> thm) * (term -> term) |
10 val assume_export: export |
10 val assume_export: export |
11 val presume_export: export |
11 val presume_export: export |
12 val assume: cterm -> thm |
12 val assume: Proof.context -> cterm -> thm |
13 val all_assms_of: Proof.context -> cterm list |
13 val all_assms_of: Proof.context -> cterm list |
14 val all_prems_of: Proof.context -> thm list |
14 val all_prems_of: Proof.context -> thm list |
15 val check_hyps: Proof.context -> thm -> thm |
15 val check_hyps: Proof.context -> thm -> thm |
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 |
95 drop (length (all_prems_of outer)) (all_prems_of inner); |
95 drop (length (all_prems_of outer)) (all_prems_of inner); |
96 |
96 |
97 |
97 |
98 (* add assumptions *) |
98 (* add assumptions *) |
99 |
99 |
100 fun add_assms export new_asms = |
100 fun add_assms export new_asms ctxt = |
101 let val new_prems = map assume new_asms in |
101 let val new_prems = map (assume ctxt) new_asms in |
102 map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #> |
102 ctxt |
103 pair new_prems |
103 |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) |
|
104 |> pair new_prems |
104 end; |
105 end; |
105 |
106 |
106 val add_assumes = add_assms assume_export; |
107 val add_assumes = add_assms assume_export; |
107 |
108 |
108 |
109 |
109 (* export *) |
110 (* export *) |
110 |
111 |
111 fun export is_goal inner outer = |
112 fun export is_goal inner outer = |
112 Raw_Simplifier.norm_hhf_protect #> |
113 Raw_Simplifier.norm_hhf_protect inner #> |
113 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> |
114 fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> |
114 Raw_Simplifier.norm_hhf_protect; |
115 Raw_Simplifier.norm_hhf_protect outer; |
115 |
116 |
116 fun export_term inner outer = |
117 fun export_term inner outer = |
117 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
118 fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); |
118 |
119 |
119 fun export_morphism inner outer = |
120 fun export_morphism inner outer = |