53 ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
54 ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
54 Bound 0)) |
55 Bound 0)) |
55 | ap_split T T3 u = u; |
56 | ap_split T T3 u = u; |
56 |
57 |
57 (*Curries any Var of function type in the rule*) |
58 (*Curries any Var of function type in the rule*) |
58 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = |
59 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl = |
59 let val T' = HOLogic.prodT_factors T1 ---> T2; |
60 let val T' = HOLogic.prodT_factors T1 ---> T2; |
60 val newt = ap_split T1 T2 (Var (v, T')); |
61 val newt = ap_split T1 T2 (Var (v, T')); |
61 val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)); |
62 val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
62 in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end |
63 in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end |
63 | split_rule_var' (t, rl) = rl; |
64 | split_rule_var' t rl = rl; |
64 |
65 |
65 |
66 |
66 (* complete splitting of partially splitted rules *) |
67 (* complete splitting of partially splitted rules *) |
67 |
68 |
68 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
69 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
69 (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U) |
70 (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U) |
70 (incr_boundvars 1 u) $ Bound 0)) |
71 (incr_boundvars 1 u) $ Bound 0)) |
71 | ap_split' _ _ u = u; |
72 | ap_split' _ _ u = u; |
72 |
73 |
73 fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) = |
74 fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) = |
74 let |
75 let |
75 val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)) |
76 val cterm = Thm.cterm_of (Thm.theory_of_thm rl) |
76 val (Us', U') = strip_type T; |
77 val (Us', U') = strip_type T; |
77 val Us = Library.take (length ts, Us'); |
78 val Us = Library.take (length ts, Us'); |
78 val U = Library.drop (length ts, Us') ---> U'; |
79 val U = Library.drop (length ts, Us') ---> U'; |
79 val T' = List.concat (map HOLogic.prodT_factors Us) ---> U; |
80 val T' = List.concat (map HOLogic.prodT_factors Us) ---> U; |
80 fun mk_tuple ((xs, insts), v as Var ((a, _), T)) = |
81 fun mk_tuple (v as Var ((a, _), T)) (xs, insts) = |
81 let |
82 let |
82 val Ts = HOLogic.prodT_factors T; |
83 val Ts = HOLogic.prodT_factors T; |
83 val ys = Term.variantlist (replicate (length Ts) a, xs); |
84 val ys = Term.variantlist (replicate (length Ts) a, xs); |
84 in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T |
85 in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T |
85 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) |
86 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) |
86 end |
87 end |
87 | mk_tuple (x, _) = x; |
88 | mk_tuple _ x = x; |
88 val newt = ap_split' Us U (Var (v, T')); |
89 val newt = ap_split' Us U (Var (v, T')); |
89 val cterm = Thm.cterm_of (#sign (Thm.rep_thm rl)); |
90 val cterm = Thm.cterm_of (Thm.theory_of_thm rl); |
90 val (vs', insts) = Library.foldl mk_tuple ((vs, []), ts); |
91 val (vs', insts) = fold mk_tuple ts (vs, []); |
91 in |
92 in |
92 (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
93 (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
93 end |
94 end |
94 | complete_split_rule_var (_, x) = x; |
95 | complete_split_rule_var _ x = x; |
95 |
96 |
96 fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t) |
97 fun collect_vars (Abs (_, _, t)) = collect_vars t |
97 | collect_vars (vs, t) = (case strip_comb t of |
98 | collect_vars t = |
98 (v as Var _, ts) => (v, ts)::vs |
99 (case strip_comb t of |
99 | (t, ts) => Library.foldl collect_vars (vs, ts)); |
100 (v as Var _, ts) => cons (v, ts) |
|
101 | (t, ts) => fold collect_vars ts); |
100 |
102 |
101 |
103 |
102 val split_rule_var = Drule.standard o remove_internal_split o split_rule_var'; |
104 val split_rule_var = (Drule.standard o remove_internal_split) oo split_rule_var'; |
103 |
105 |
104 (*curries ALL function variables occurring in a rule's conclusion*) |
106 (*curries ALL function variables occurring in a rule's conclusion*) |
105 fun split_rule rl = |
107 fun split_rule rl = |
106 foldr split_rule_var' rl (Term.term_vars (concl_of rl)) |
108 fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl |
107 |> remove_internal_split |
109 |> remove_internal_split |
108 |> Drule.standard; |
110 |> Drule.standard; |
109 |
111 |
|
112 (*curries ALL function variables*) |
110 fun complete_split_rule rl = |
113 fun complete_split_rule rl = |
111 fst (foldr complete_split_rule_var |
114 let |
112 (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl)))) |
115 val prop = Thm.prop_of rl; |
113 (collect_vars ([], concl_of rl))) |
116 val xs = Term.fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I) prop []; |
114 |> remove_internal_split |
117 val vars = collect_vars prop []; |
115 |> Drule.standard |
118 in |
116 |> RuleCases.save rl; |
119 fst (fold_rev complete_split_rule_var vars (rl, xs)) |
|
120 |> remove_internal_split |
|
121 |> Drule.standard |
|
122 |> RuleCases.save rl |
|
123 end; |
117 |
124 |
118 |
125 |
119 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
126 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; |
120 |
127 |
121 fun split_rule_goal xss rl = |
128 fun split_rule_goal xss rl = |
122 let |
129 let |
123 fun one_split i s = Tactic.rule_by_tactic (pair_tac s i); |
130 fun one_split i s = Tactic.rule_by_tactic (pair_tac s i); |
124 fun one_goal (i, xs) = fold (one_split (i+1)) xs; |
131 fun one_goal (i, xs) = fold (one_split (i + 1)) xs; |
125 in |
132 in |
126 rl |
133 rl |
127 |> Library.fold_index one_goal xss |
134 |> fold_index one_goal xss |
128 |> Simplifier.full_simplify split_rule_ss |
135 |> Simplifier.full_simplify split_rule_ss |
129 |> Drule.standard |
136 |> Drule.standard |
130 |> RuleCases.save rl |
137 |> RuleCases.save rl |
131 end; |
138 end; |
132 |
139 |
133 (* attribute syntax *) |
140 (* attribute syntax *) |
134 |
141 |