author | bulwahn |
Sat, 24 Oct 2009 16:55:42 +0200 | |
changeset 33140 | 83951822bfd0 |
parent 33119 | bf18c8174571 |
permissions | -rw-r--r-- |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
2 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
Preprocessing sets to predicates |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
|
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33119
diff
changeset
|
6 |
signature PREDICATE_COMPILE_SET = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
sig |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
val preprocess_intro : thm -> theory -> thm * theory |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
val preprocess_clause : term -> theory -> term * theory |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
val unfold_set_notation : thm -> thm; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
|
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33119
diff
changeset
|
15 |
structure Predicate_Compile_Set : PREDICATE_COMPILE_SET = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
(*FIXME: unfolding Ball in pretty adhoc here *) |
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
18 |
val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, |
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
19 |
@{thm Ball_def}, @{thm Bex_def}] |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
fun find_set_theorems ctxt cname = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
val _ = cname |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
fun preprocess_term t ctxt = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
case t of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
Const ("op :", _) $ x $ A => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
case strip_comb A of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
(Const (cname, T), params) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
val _ = find_set_theorems |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
(t, ctxt) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
| _ => (t, ctxt) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
| _ => (t, ctxt) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
43 |
(* |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
fun preprocess_intro th thy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
45 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
val cnames = find_heads_of_prems |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
47 |
val set_cname = filter (has_set_definition |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
48 |
val _ = define_preds |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
49 |
val _ = prep_pred_def |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
50 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
51 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
52 |
end; |