4 Some tools for managing tupled arguments and abstractions in rules. |
4 Some tools for managing tupled arguments and abstractions in rules. |
5 *) |
5 *) |
6 |
6 |
7 signature SPLIT_RULE = |
7 signature SPLIT_RULE = |
8 sig |
8 sig |
9 val split_rule_var: term -> thm -> thm |
9 val split_rule_var: Proof.context -> term -> thm -> thm |
10 val split_rule: thm -> thm |
10 val split_rule: Proof.context -> thm -> thm |
11 val complete_split_rule: thm -> thm |
11 val complete_split_rule: Proof.context -> thm -> thm |
12 val setup: theory -> theory |
12 val setup: theory -> theory |
13 end; |
13 end; |
14 |
14 |
15 structure Split_Rule: SPLIT_RULE = |
15 structure Split_Rule: SPLIT_RULE = |
16 struct |
16 struct |
19 |
19 |
20 fun internal_split_const (Ta, Tb, Tc) = |
20 fun internal_split_const (Ta, Tb, Tc) = |
21 Const (@{const_name Product_Type.internal_split}, |
21 Const (@{const_name Product_Type.internal_split}, |
22 [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); |
22 [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); |
23 |
23 |
24 val eval_internal_split = |
24 fun eval_internal_split ctxt = |
25 hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}]; |
25 hol_simplify ctxt @{thms internal_split_def} o |
|
26 hol_simplify ctxt @{thms internal_split_conv}; |
26 |
27 |
27 val remove_internal_split = eval_internal_split o split_all; |
28 fun remove_internal_split ctxt = eval_internal_split ctxt o split_all ctxt; |
28 |
29 |
29 |
30 |
30 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
31 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
31 with result type T. The call creates a new term expecting one argument |
32 with result type T. The call creates a new term expecting one argument |
32 of type S.*) |
33 of type S.*) |
82 (case strip_comb t of |
83 (case strip_comb t of |
83 (v as Var _, ts) => cons (v, ts) |
84 (v as Var _, ts) => cons (v, ts) |
84 | (t, ts) => fold collect_vars ts); |
85 | (t, ts) => fold collect_vars ts); |
85 |
86 |
86 |
87 |
87 val split_rule_var = (Drule.export_without_context o remove_internal_split) oo split_rule_var'; |
88 fun split_rule_var ctxt = |
|
89 (Drule.export_without_context o remove_internal_split ctxt) oo split_rule_var'; |
88 |
90 |
89 (*curries ALL function variables occurring in a rule's conclusion*) |
91 (*curries ALL function variables occurring in a rule's conclusion*) |
90 fun split_rule rl = |
92 fun split_rule ctxt rl = |
91 fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl |
93 fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl |
92 |> remove_internal_split |
94 |> remove_internal_split ctxt |
93 |> Drule.export_without_context; |
95 |> Drule.export_without_context; |
94 |
96 |
95 (*curries ALL function variables*) |
97 (*curries ALL function variables*) |
96 fun complete_split_rule rl = |
98 fun complete_split_rule ctxt rl = |
97 let |
99 let |
98 val prop = Thm.prop_of rl; |
100 val prop = Thm.prop_of rl; |
99 val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop []; |
101 val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop []; |
100 val vars = collect_vars prop []; |
102 val vars = collect_vars prop []; |
101 in |
103 in |
102 fst (fold_rev complete_split_rule_var vars (rl, xs)) |
104 fst (fold_rev complete_split_rule_var vars (rl, xs)) |
103 |> remove_internal_split |
105 |> remove_internal_split ctxt |
104 |> Drule.export_without_context |
106 |> Drule.export_without_context |
105 |> Rule_Cases.save rl |
107 |> Rule_Cases.save rl |
106 end; |
108 end; |
107 |
109 |
108 |
110 |
109 (* attribute syntax *) |
111 (* attribute syntax *) |
110 |
112 |
111 val setup = |
113 val setup = |
112 Attrib.setup @{binding split_format} |
114 Attrib.setup @{binding split_format} |
113 (Scan.lift |
115 (Scan.lift (Args.parens (Args.$$$ "complete") |
114 (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)))) |
116 >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of)))) |
115 "split pair-typed subterms in premises, or function arguments" #> |
117 "split pair-typed subterms in premises, or function arguments" #> |
116 Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule))) |
118 Attrib.setup @{binding split_rule} |
|
119 (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of))) |
117 "curries ALL function variables occurring in a rule's conclusion"; |
120 "curries ALL function variables occurring in a rule's conclusion"; |
118 |
121 |
119 end; |
122 end; |
120 |
123 |