1 (* Title: HOL/Tools/Function/fundef_lib.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A package for general recursive function definitions. |
|
5 Some fairly general functions that should probably go somewhere else... |
|
6 *) |
|
7 |
|
8 structure FundefLib = struct |
|
9 |
|
10 fun map_option f NONE = NONE |
|
11 | map_option f (SOME x) = SOME (f x); |
|
12 |
|
13 fun fold_option f NONE y = y |
|
14 | fold_option f (SOME x) y = f x y; |
|
15 |
|
16 fun fold_map_option f NONE y = (NONE, y) |
|
17 | fold_map_option f (SOME x) y = apfst SOME (f x y); |
|
18 |
|
19 (* Ex: "The variable" ^ plural " is" "s are" vs *) |
|
20 fun plural sg pl [x] = sg |
|
21 | plural sg pl _ = pl |
|
22 |
|
23 (* lambda-abstracts over an arbitrarily nested tuple |
|
24 ==> hologic.ML? *) |
|
25 fun tupled_lambda vars t = |
|
26 case vars of |
|
27 (Free v) => lambda (Free v) t |
|
28 | (Var v) => lambda (Var v) t |
|
29 | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs => |
|
30 (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t)) |
|
31 | _ => raise Match |
|
32 |
|
33 |
|
34 fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) = |
|
35 let |
|
36 val (n, body) = Term.dest_abs a |
|
37 in |
|
38 (Free (n, T), body) |
|
39 end |
|
40 | dest_all _ = raise Match |
|
41 |
|
42 |
|
43 (* Removes all quantifiers from a term, replacing bound variables by frees. *) |
|
44 fun dest_all_all (t as (Const ("all",_) $ _)) = |
|
45 let |
|
46 val (v,b) = dest_all t |
|
47 val (vs, b') = dest_all_all b |
|
48 in |
|
49 (v :: vs, b') |
|
50 end |
|
51 | dest_all_all t = ([],t) |
|
52 |
|
53 |
|
54 (* FIXME: similar to Variable.focus *) |
|
55 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = |
|
56 let |
|
57 val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] |
|
58 val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx |
|
59 |
|
60 val (n'', body) = Term.dest_abs (n', T, b) |
|
61 val _ = (n' = n'') orelse error "dest_all_ctx" |
|
62 (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) |
|
63 |
|
64 val (ctx'', vs, bd) = dest_all_all_ctx ctx' body |
|
65 in |
|
66 (ctx'', (n', T) :: vs, bd) |
|
67 end |
|
68 | dest_all_all_ctx ctx t = |
|
69 (ctx, [], t) |
|
70 |
|
71 |
|
72 fun map3 _ [] [] [] = [] |
|
73 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
|
74 | map3 _ _ _ _ = raise Library.UnequalLengths; |
|
75 |
|
76 fun map4 _ [] [] [] [] = [] |
|
77 | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
|
78 | map4 _ _ _ _ _ = raise Library.UnequalLengths; |
|
79 |
|
80 fun map6 _ [] [] [] [] [] [] = [] |
|
81 | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws |
|
82 | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths; |
|
83 |
|
84 fun map7 _ [] [] [] [] [] [] [] = [] |
|
85 | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs |
|
86 | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths; |
|
87 |
|
88 |
|
89 |
|
90 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
|
91 (* ==> library *) |
|
92 fun unordered_pairs [] = [] |
|
93 | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
|
94 |
|
95 |
|
96 (* Replaces Frees by name. Works with loose Bounds. *) |
|
97 fun replace_frees assoc = |
|
98 map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) |
|
99 | t => t) |
|
100 |
|
101 |
|
102 fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) |
|
103 | rename_bound n _ = raise Match |
|
104 |
|
105 fun mk_forall_rename (n, v) = |
|
106 rename_bound n o Logic.all v |
|
107 |
|
108 fun forall_intr_rename (n, cv) thm = |
|
109 let |
|
110 val allthm = forall_intr cv thm |
|
111 val (_ $ abs) = prop_of allthm |
|
112 in |
|
113 Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm |
|
114 end |
|
115 |
|
116 |
|
117 (* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
|
118 fun frees_in_term ctxt t = |
|
119 Term.add_frees t [] |
|
120 |> filter_out (Variable.is_fixed ctxt o fst) |
|
121 |> rev |
|
122 |
|
123 |
|
124 datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
|
125 |
|
126 fun try_proof cgoal tac = |
|
127 case SINGLE tac (Goal.init cgoal) of |
|
128 NONE => Fail |
|
129 | SOME st => |
|
130 if Thm.no_prems st |
|
131 then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) |
|
132 else Stuck st |
|
133 |
|
134 |
|
135 fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = |
|
136 if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] |
|
137 | dest_binop_list _ t = [ t ] |
|
138 |
|
139 |
|
140 (* separate two parts in a +-expression: |
|
141 "a + b + c + d + e" --> "(a + b + d) + (c + e)" |
|
142 |
|
143 Here, + can be any binary operation that is AC. |
|
144 |
|
145 cn - The name of the binop-constructor (e.g. @{const_name Un}) |
|
146 ac - the AC rewrite rules for cn |
|
147 is - the list of indices of the expressions that should become the first part |
|
148 (e.g. [0,1,3] in the above example) |
|
149 *) |
|
150 |
|
151 fun regroup_conv neu cn ac is ct = |
|
152 let |
|
153 val mk = HOLogic.mk_binop cn |
|
154 val t = term_of ct |
|
155 val xs = dest_binop_list cn t |
|
156 val js = subtract (op =) is (0 upto (length xs) - 1) |
|
157 val ty = fastype_of t |
|
158 val thy = theory_of_cterm ct |
|
159 in |
|
160 Goal.prove_internal [] |
|
161 (cterm_of thy |
|
162 (Logic.mk_equals (t, |
|
163 if is = [] |
|
164 then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) |
|
165 else if js = [] |
|
166 then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) |
|
167 else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) |
|
168 (K (rewrite_goals_tac ac |
|
169 THEN rtac Drule.reflexive_thm 1)) |
|
170 end |
|
171 |
|
172 (* instance for unions *) |
|
173 fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup} |
|
174 (map (fn t => t RS eq_reflection) (@{thms Un_ac} @ |
|
175 @{thms Un_empty_right} @ |
|
176 @{thms Un_empty_left})) t |
|
177 |
|
178 |
|
179 end |
|