author | haftmann |
Fri, 10 Dec 2010 16:10:50 +0100 | |
changeset 41107 | 8795cd75965e |
parent 40722 | 441260986b63 |
child 41113 | b223fa19af3c |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Function/function_lib.ML |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
4 |
A package for general recursive function definitions. |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
5 |
Some fairly general functions that should probably go somewhere else... |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
|
36945 | 8 |
structure Function_Lib = (* FIXME proper signature *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
9 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
10 |
|
40076 | 11 |
(* "The variable" ^ plural " is" "s are" vs *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
12 |
fun plural sg pl [x] = sg |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
13 |
| plural sg pl _ = pl |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
14 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
15 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
16 |
(* Removes all quantifiers from a term, replacing bound variables by frees. *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
17 |
fun dest_all_all (t as (Const ("all",_) $ _)) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
18 |
let |
40076 | 19 |
val (v,b) = Logic.dest_all t |> apfst Free |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
20 |
val (vs, b') = dest_all_all b |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
21 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
22 |
(v :: vs, b') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
23 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
24 |
| dest_all_all t = ([],t) |
33611 | 25 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
26 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
27 |
(* FIXME: similar to Variable.focus *) |
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33611
diff
changeset
|
28 |
fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
29 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
30 |
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
31 |
val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
32 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
33 |
val (n'', body) = Term.dest_abs (n', T, b) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
34 |
val _ = (n' = n'') orelse error "dest_all_ctx" |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
35 |
(* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
36 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
37 |
val (ctx'', vs, bd) = dest_all_all_ctx ctx' body |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
38 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
39 |
(ctx'', (n', T) :: vs, bd) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
40 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
41 |
| dest_all_all_ctx ctx t = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
42 |
(ctx, [], t) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
fun map4 _ [] [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
| map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us |
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40076
diff
changeset
|
47 |
| map4 _ _ _ _ _ = raise ListPair.UnequalLengths; |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
fun map7 _ [] [] [] [] [] [] [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
50 |
| 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 |
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40076
diff
changeset
|
51 |
| map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
53 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
56 |
fun unordered_pairs [] = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
| unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
59 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
60 |
(* Replaces Frees by name. Works with loose Bounds. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
61 |
fun replace_frees assoc = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
62 |
map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
| t => t) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
64 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
fun rename_bound n (Q $ Abs (_, T, b)) = (Q $ Abs (n, T, b)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
| rename_bound n _ = raise Match |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
68 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
69 |
fun mk_forall_rename (n, v) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
70 |
rename_bound n o Logic.all v |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
71 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
fun forall_intr_rename (n, cv) thm = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
73 |
let |
36945 | 74 |
val allthm = Thm.forall_intr cv thm |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
75 |
val (_ $ abs) = prop_of allthm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
76 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
77 |
Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
78 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
(* Returns the frees in a term in canonical order, excluding the fixes from the context *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
82 |
fun frees_in_term ctxt t = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
83 |
Term.add_frees t [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
84 |
|> filter_out (Variable.is_fixed ctxt o fst) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
85 |
|> rev |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
86 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
87 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
88 |
datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
89 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
90 |
fun try_proof cgoal tac = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
91 |
case SINGLE tac (Goal.init cgoal) of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
92 |
NONE => Fail |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
93 |
| SOME st => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
94 |
if Thm.no_prems st |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
95 |
then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
96 |
else Stuck st |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
97 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
98 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
99 |
fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
100 |
if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ] |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
101 |
| dest_binop_list _ t = [ t ] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
102 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
103 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
104 |
(* separate two parts in a +-expression: |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
105 |
"a + b + c + d + e" --> "(a + b + d) + (c + e)" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
106 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
Here, + can be any binary operation that is AC. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
108 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
109 |
cn - The name of the binop-constructor (e.g. @{const_name Un}) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
ac - the AC rewrite rules for cn |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
111 |
is - the list of indices of the expressions that should become the first part |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
112 |
(e.g. [0,1,3] in the above example) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
113 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
fun regroup_conv neu cn ac is ct = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
116 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
117 |
val mk = HOLogic.mk_binop cn |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
118 |
val t = term_of ct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
119 |
val xs = dest_binop_list cn t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
val js = subtract (op =) is (0 upto (length xs) - 1) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
val ty = fastype_of t |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
val thy = theory_of_cterm ct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
123 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
124 |
Goal.prove_internal [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
(cterm_of thy |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
(Logic.mk_equals (t, |
33611 | 127 |
if null is |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
then mk (Const (neu, ty), foldr1 mk (map (nth xs) js)) |
33611 | 129 |
else if null js |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js))))) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
132 |
(K (rewrite_goals_tac ac |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
133 |
THEN rtac Drule.reflexive_thm 1)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
134 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
136 |
(* instance for unions *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
137 |
val regroup_union_conv = |
35402 | 138 |
regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup} |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
139 |
(map (fn t => t RS eq_reflection) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
140 |
(@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left})) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
end |