author | krauss |
Wed, 04 Oct 2006 11:18:39 +0200 | |
changeset 20851 | bf80cb83f8be |
parent 20523 | 36a59e5d0039 |
child 20876 | bc2669d5744d |
permissions | -rw-r--r-- |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/lib.ML |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
4 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
5 |
A package for general recursive function definitions. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
Some fairly general functions that should probably go somewhere else... |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
7 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
10 |
fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
11 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
12 |
fun mk_forall (var as Free (v,T)) t = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
13 |
all T $ Abs (v,T, abstract_over (var,t)) |
19922 | 14 |
| mk_forall v _ = let val _ = print v in sys_error "mk_forall" end |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
15 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
17 |
(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
18 |
fun tupled_lambda vars t = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
case vars of |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
20 |
(Free v) => lambda (Free v) t |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
21 |
| (Var v) => lambda (Var v) t |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
22 |
| (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs => |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
23 |
(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t)) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
24 |
| _ => raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
25 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
26 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
27 |
fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
28 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
29 |
val (n, body) = Term.dest_abs a |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
30 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
31 |
(Free (n, T), body) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
32 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
33 |
| dest_all _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
34 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
35 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
36 |
(* Removes all quantifiers from a term, replacing bound variables by frees. *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
37 |
fun dest_all_all (t as (Const ("all",_) $ _)) = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
39 |
val (v,b) = dest_all t |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
40 |
val (vs, b') = dest_all_all b |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
41 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
42 |
(v :: vs, b') |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
43 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
44 |
| dest_all_all t = ([],t) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
45 |
|
19922 | 46 |
|
47 |
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = |
|
48 |
let |
|
20154
c709a29f1363
renamed Variable.rename_wrt to Variable.variant_frees;
wenzelm
parents:
19922
diff
changeset
|
49 |
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] |
19922 | 50 |
val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx |
51 |
||
52 |
val (n'', body) = Term.dest_abs (n', T, b) |
|
53 |
val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) |
|
54 |
||
55 |
val (ctx'', vs, bd) = dest_all_all_ctx ctx' body |
|
56 |
in |
|
57 |
(ctx'', (n', T) :: vs, bd) |
|
58 |
end |
|
59 |
| dest_all_all_ctx ctx t = |
|
60 |
(ctx, [], t) |
|
61 |
||
62 |
||
63 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |
(* unfold *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
65 |
fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
66 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
67 |
val dest_implies_list = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
68 |
split_last o (unfold Logic.is_implies (fst o Logic.dest_implies) (snd o Logic.dest_implies) single) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
69 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
70 |
fun implies_elim_swp a b = implies_elim b a |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
71 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
72 |
fun map3 _ [] [] [] = [] |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
73 |
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
19841 | 74 |
| map3 _ _ _ _ = raise Library.UnequalLengths; |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
75 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
76 |
fun map4 _ [] [] [] [] = [] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
77 |
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
78 |
| map4 _ _ _ _ _ = raise Library.UnequalLengths; |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
79 |
|
19922 | 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 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
84 |
fun map7 _ [] [] [] [] [] [] [] = [] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
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 |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
86 |
| map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths; |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
87 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
88 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
89 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
90 |
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
19922 | 91 |
fun unordered_pairs [] = [] |
92 |
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
93 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
94 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
95 |
fun the_single [x] = x |
19841 | 96 |
| the_single _ = sys_error "the_single" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
97 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
98 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
99 |
(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
100 |
fun replace_frees assoc = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
101 |
map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
102 |
NONE => c |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
103 |
| SOME t => t) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
104 |
| t => t) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
105 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
106 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
107 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
108 |
fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
109 |
| rename_bound n _ = raise Match |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
110 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
111 |
fun mk_forall_rename (n, v) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
112 |
rename_bound n o mk_forall v |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
113 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
114 |
fun forall_intr_rename (n, cv) thm = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
115 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
116 |
val allthm = forall_intr cv thm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
117 |
val reflx = prop_of allthm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
118 |
|> rename_bound n |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
119 |
|> cterm_of (theory_of_thm thm) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
120 |
|> reflexive |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
121 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
122 |
equal_elim reflx allthm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
123 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
124 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
125 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
126 |
(* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
127 |
fun frees_in_term ctxt t = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
128 |
rev (fold_aterms (fn Free (v as (x, _)) => |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20154
diff
changeset
|
129 |
if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t []) |
20851 | 130 |
|
131 |
||
132 |
fun plural sg pl [] = sys_error "plural" |
|
133 |
| plural sg pl [x] = sg |
|
134 |
| plural sg pl (x::y::ys) = pl |