equal
deleted
inserted
replaced
15 val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context |
15 val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context |
16 val fixed_abbrev: (binding * mixfix) * term -> Proof.context -> |
16 val fixed_abbrev: (binding * mixfix) * term -> Proof.context -> |
17 (term * term) * Proof.context |
17 (term * term) * Proof.context |
18 val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm |
18 val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm |
19 val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm |
19 val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm |
20 val contract: thm list -> cterm -> thm -> thm |
20 val contract: Proof.context -> thm list -> cterm -> thm -> thm |
21 val print_rules: Proof.context -> unit |
21 val print_rules: Proof.context -> unit |
22 val defn_add: attribute |
22 val defn_add: attribute |
23 val defn_del: attribute |
23 val defn_del: attribute |
24 val meta_rewrite_conv: Proof.context -> conv |
24 val meta_rewrite_conv: Proof.context -> conv |
25 val meta_rewrite_rule: Proof.context -> thm -> thm |
25 val meta_rewrite_rule: Proof.context -> thm -> thm |
160 TERM b as b xs == b as |
160 TERM b as b xs == b as |
161 *) |
161 *) |
162 fun export_cterm inner outer ct = |
162 fun export_cterm inner outer ct = |
163 export inner outer (Drule.mk_term ct) ||> Drule.dest_term; |
163 export inner outer (Drule.mk_term ct) ||> Drule.dest_term; |
164 |
164 |
165 fun contract defs ct th = |
165 fun contract ctxt defs ct th = |
166 th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2); |
166 th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2); |
167 |
167 |
168 |
168 |
169 |
169 |
170 (** defived definitions **) |
170 (** defived definitions **) |
171 |
171 |
198 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv; |
198 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv; |
199 |
199 |
200 |
200 |
201 (* rewriting with object-level rules *) |
201 (* rewriting with object-level rules *) |
202 |
202 |
203 fun meta f ctxt = f o map (meta_rewrite_rule ctxt); |
203 fun meta f ctxt = f ctxt o map (meta_rewrite_rule ctxt); |
204 |
204 |
205 val unfold = meta Raw_Simplifier.rewrite_rule; |
205 val unfold = meta Raw_Simplifier.rewrite_rule; |
206 val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule; |
206 val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule; |
207 val unfold_tac = meta Raw_Simplifier.rewrite_goals_tac; |
207 val unfold_tac = meta Raw_Simplifier.rewrite_goals_tac; |
208 val fold = meta Raw_Simplifier.fold_rule; |
208 val fold = meta Raw_Simplifier.fold_rule; |
218 |> meta_rewrite_conv ctxt |
218 |> meta_rewrite_conv ctxt |
219 |> (snd o Logic.dest_equals o Thm.prop_of) |
219 |> (snd o Logic.dest_equals o Thm.prop_of) |
220 |> conditional ? Logic.strip_imp_concl |
220 |> conditional ? Logic.strip_imp_concl |
221 |> (abs_def o #2 o cert_def ctxt); |
221 |> (abs_def o #2 o cert_def ctxt); |
222 fun prove ctxt' def = |
222 fun prove ctxt' def = |
223 Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop (K (ALLGOALS |
223 Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop |
224 (CONVERSION (meta_rewrite_conv ctxt') THEN' |
224 (fn {context = ctxt'', ...} => |
225 rewrite_goal_tac [def] THEN' |
225 ALLGOALS |
226 resolve_tac [Drule.reflexive_thm]))) |
226 (CONVERSION (meta_rewrite_conv ctxt'') THEN' |
|
227 rewrite_goal_tac ctxt'' [def] THEN' |
|
228 resolve_tac [Drule.reflexive_thm])) |
227 handle ERROR msg => cat_error msg "Failed to prove definitional specification"; |
229 handle ERROR msg => cat_error msg "Failed to prove definitional specification"; |
228 in (((c, T), rhs), prove) end; |
230 in (((c, T), rhs), prove) end; |
229 |
231 |
230 end; |
232 end; |