equal
deleted
inserted
replaced
133 If we try out the function with the rules for freshness |
133 If we try out the function with the rules for freshness |
134 *} |
134 *} |
135 |
135 |
136 local_setup %gray {* fn lthy => |
136 local_setup %gray {* fn lthy => |
137 let |
137 let |
138 val def = defn_aux lthy fresh_orules |
138 val arg = (fresh_pred, fresh_arg_tys) |
139 [fresh_pred] (fresh_pred, fresh_arg_tys) |
139 val def = defn_aux lthy fresh_orules [fresh_pred] arg |
140 in |
140 in |
141 tracing (string_of_term lthy def); lthy |
141 tracing (string_of_term lthy def); lthy |
142 end *} |
142 end *} |
143 |
143 |
144 |
144 |
237 |
237 |
238 The tactic will use the following helper function for instantiating universal |
238 The tactic will use the following helper function for instantiating universal |
239 quantifiers. |
239 quantifiers. |
240 *} |
240 *} |
241 |
241 |
242 ML{*fun inst_spec ctrm = |
242 ML{*fun inst_spec ctrm = |
243 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] |
243 let |
244 @{thm spec}*} |
244 val cty = ctyp_of_term ctrm |
|
245 in |
|
246 Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} |
|
247 end*} |
245 |
248 |
246 text {* |
249 text {* |
247 This helper function uses the function @{ML_ind instantiate' in Drule} |
250 This helper function uses the function @{ML_ind instantiate' in Drule} |
248 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given |
251 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given |
249 @{ML_type cterm}. We call this helper function in the following |
252 @{ML_type cterm}. We call this helper function in the following |
611 \begin{minipage}{\textwidth} |
614 \begin{minipage}{\textwidth} |
612 \begin{isabelle} |
615 \begin{isabelle} |
613 *} |
616 *} |
614 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
617 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
615 let |
618 let |
616 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
619 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
617 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
620 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
618 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
621 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
619 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
622 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
620 in |
623 in |
621 s |> cat_lines |
624 s |> cat_lines |
622 |> tracing |
625 |> tracing |
623 end*} |
626 end*} |
624 text_raw{* |
627 text_raw{* |