author | wenzelm |
Wed, 28 Oct 2009 00:07:51 +0100 | |
changeset 33265 | 01c9c6dbd890 |
parent 33250 | 5c2af18a3237 |
child 33278 | ba9f52f56356 |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_fun.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
|
33265 | 4 |
Preprocessing functions to predicates. |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
5 |
*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_FUN = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
sig |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
10 |
val rewrite_intro : theory -> thm -> thm list |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
val setup_oracle : theory -> theory |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
val pred_of_function : theory -> string -> string option |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
14 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
15 |
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
struct |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
18 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
(* Oracle for preprocessing *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
fun the_oracle () = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
24 |
case !oracle of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
25 |
NONE => error "Oracle is not setup" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
26 |
| SOME (_, oracle) => oracle |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
27 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
28 |
val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #-> |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
29 |
(fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
30 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
31 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
32 |
fun is_funtype (Type ("fun", [_, _])) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
33 |
| is_funtype _ = false; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
34 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
35 |
fun is_Type (Type _) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
36 |
| is_Type _ = false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
37 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
38 |
(* returns true if t is an application of an datatype constructor *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
39 |
(* which then consequently would be splitted *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
40 |
(* else false *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
41 |
(* |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
42 |
fun is_constructor thy t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
43 |
if (is_Type (fastype_of t)) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
44 |
(case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
45 |
NONE => false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
46 |
| SOME info => (let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
47 |
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
48 |
val (c, _) = strip_comb t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
49 |
in (case c of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
50 |
Const (name, _) => name mem_string constr_consts |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
51 |
| _ => false) end)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
52 |
else false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
53 |
*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
54 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
55 |
(* must be exported in code.ML *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
56 |
fun is_constr thy = is_some o Code.get_datatype_of_constr thy; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
57 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
58 |
(* Table from constant name (string) to term of inductive predicate *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
59 |
structure Pred_Compile_Preproc = TheoryDataFun |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
60 |
( |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
61 |
type T = string Symtab.table; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
62 |
val empty = Symtab.empty; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
63 |
val copy = I; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
64 |
val extend = I; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
65 |
fun merge _ = Symtab.merge (op =); |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
66 |
) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
67 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
68 |
fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
69 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
70 |
fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
71 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
72 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
73 |
fun transform_ho_typ (T as Type ("fun", _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
74 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
75 |
val (Ts, T') = strip_type T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
77 |
| transform_ho_typ t = t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
78 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
79 |
fun transform_ho_arg arg = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
80 |
case (fastype_of arg) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
81 |
(T as Type ("fun", _)) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
(case arg of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
Free (name, _) => Free (name, transform_ho_typ T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
84 |
| _ => error "I am surprised") |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
85 |
| _ => arg |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
86 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
fun pred_type T = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
88 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
89 |
val (Ts, T') = strip_type T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
90 |
val Ts' = map transform_ho_typ Ts |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
91 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
92 |
(Ts' @ [T']) ---> HOLogic.boolT |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
93 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
94 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
95 |
(* FIXME: create new predicate name -- does not avoid nameclashing *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
96 |
fun pred_of f = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
97 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
98 |
val (name, T) = dest_Const f |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
99 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
100 |
if (body_type T = @{typ bool}) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
101 |
(Free (Long_Name.base_name name ^ "P", T)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
102 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
103 |
(Free (Long_Name.base_name name ^ "P", pred_type T)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
104 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
105 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
106 |
fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
107 |
| mk_param thy lookup_pred t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
108 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
109 |
val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
110 |
in if Predicate_Compile_Aux.is_predT (fastype_of t) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
111 |
t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
112 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
113 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
114 |
val (vs, body) = strip_abs t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
115 |
val names = Term.add_free_names body [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
116 |
val vs_names = Name.variant_list names (map fst vs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
117 |
val vs' = map2 (curry Free) vs_names (map snd vs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
118 |
val body' = subst_bounds (rev vs', body) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
119 |
val (f, args) = strip_comb body' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
120 |
val resname = Name.variant (vs_names @ names) "res" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
121 |
val resvar = Free (resname, body_type (fastype_of body')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
122 |
(*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
123 |
val pred_body = list_comb (P, args @ [resvar]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
124 |
*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
125 |
val pred_body = HOLogic.mk_eq (body', resvar) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
126 |
val param = fold_rev lambda (vs' @ [resvar]) pred_body |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
127 |
in param end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
128 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
129 |
(* creates the list of premises for every intro rule *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
130 |
(* theory -> term -> (string list, term list list) *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
131 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
132 |
fun dest_code_eqn eqn = let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
133 |
val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
134 |
val (func, args) = strip_comb lhs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
135 |
in ((func, args), rhs) end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
136 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
137 |
fun string_of_typ T = Syntax.string_of_typ_global @{theory} T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
138 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
139 |
fun string_of_term t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
140 |
case t of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
141 |
Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
142 |
| Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
143 |
| Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
144 |
| Bound i => "Bound " ^ string_of_int i |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
145 |
| Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
146 |
| t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
147 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
148 |
fun ind_package_get_nparams thy name = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
149 |
case try (Inductive.the_inductive (ProofContext.init thy)) name of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
150 |
SOME (_, result) => length (Inductive.params_of (#raw_induct result)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
151 |
| NONE => error ("No such predicate: " ^ quote name) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
152 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
153 |
(* TODO: does not work with higher order functions yet *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
154 |
fun mk_rewr_eq (func, pred) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
155 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
156 |
val (argTs, resT) = (strip_type (fastype_of func)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
157 |
val nctxt = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
158 |
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
159 |
val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
160 |
val ([resname], nctxt'') = Name.variants ["r"] nctxt' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
161 |
val args = map Free (argnames ~~ argTs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
162 |
val res = Free (resname, resT) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
163 |
in Logic.mk_equals |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
164 |
(HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
165 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
166 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
167 |
fun has_split_rule_cname @{const_name "nat_case"} = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
168 |
| has_split_rule_cname @{const_name "list_case"} = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
169 |
| has_split_rule_cname _ = false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
170 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
171 |
fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
172 |
| has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
173 |
| has_split_rule_term thy _ = false |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
174 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
175 |
fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
176 |
| has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
177 |
| has_split_rule_term' thy c = has_split_rule_term thy c |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
178 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
179 |
fun prepare_split_thm ctxt split_thm = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
180 |
(split_thm RS @{thm iffD2}) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
181 |
|> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]}, |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
182 |
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
183 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
184 |
fun find_split_thm thy (Const (name, typ)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
185 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
186 |
fun split_name str = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
187 |
case first_field "." str |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
188 |
of (SOME (field, rest)) => field :: split_name rest |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
189 |
| NONE => [str] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
190 |
val splitted_name = split_name name |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
191 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
192 |
if length splitted_name > 0 andalso |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
193 |
String.isSuffix "_case" (List.last splitted_name) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
194 |
then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
195 |
(List.take (splitted_name, length splitted_name - 1)) @ ["split"] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
196 |
|> space_implode "." |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
197 |
|> PureThy.get_thm thy |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
198 |
|> SOME |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
199 |
handle ERROR msg => NONE |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
200 |
else NONE |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
201 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
202 |
| find_split_thm _ _ = NONE |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
203 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
204 |
fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
205 |
| find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
206 |
| find_split_thm' thy c = find_split_thm thy c |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
207 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
208 |
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
209 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
210 |
fun folds_map f xs y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
211 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
212 |
fun folds_map' acc [] y = [(rev acc, y)] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
213 |
| folds_map' acc (x :: xs) y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
214 |
maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
215 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
216 |
folds_map' [] xs y |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
217 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
218 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
219 |
fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
220 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
221 |
fun mk_prems' (t as Const (name, T)) (names, prems) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
222 |
if is_constr thy name orelse (is_none (try lookup_pred t)) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
223 |
[(t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
224 |
else [(lookup_pred t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
225 |
| mk_prems' (t as Free (f, T)) (names, prems) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
226 |
[(lookup_pred t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
227 |
| mk_prems' (t as Abs _) (names, prems) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
228 |
if Predicate_Compile_Aux.is_predT (fastype_of t) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
229 |
[(t, (names, prems))] else error "mk_prems': Abs " |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
230 |
(* mk_param *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
231 |
| mk_prems' t (names, prems) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
232 |
if Predicate_Compile_Aux.is_constrt thy t then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
233 |
[(t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
234 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
235 |
if has_split_rule_term' thy (fst (strip_comb t)) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
236 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
237 |
val (f, args) = strip_comb t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
238 |
val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
239 |
(* TODO: contextify things - this line is to unvarify the split_thm *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
240 |
(*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
241 |
val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
242 |
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
243 |
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
244 |
val (_, split_args) = strip_comb split_t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
245 |
val match = split_args ~~ args |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
246 |
fun mk_prems_of_assm assm = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
247 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
248 |
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
249 |
val var_names = Name.variant_list names (map fst vTs) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
250 |
val vars = map Free (var_names ~~ (map snd vTs)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
251 |
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
252 |
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
253 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
254 |
mk_prems' inner_t (var_names @ names, prems' @ prems) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
255 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
256 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
257 |
maps mk_prems_of_assm assms |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
258 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
259 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
260 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
261 |
val (f, args) = strip_comb t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
262 |
(* TODO: special procedure for higher-order functions: split arguments in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
263 |
simple types and function types *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
264 |
val resname = Name.variant names "res" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
265 |
val resvar = Free (resname, body_type (fastype_of t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
266 |
val names' = resname :: names |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
267 |
fun mk_prems'' (t as Const (c, _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
268 |
if is_constr thy c orelse (is_none (try lookup_pred t)) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
269 |
folds_map mk_prems' args (names', prems) |> |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
270 |
map |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
271 |
(fn (argvs, (names'', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
272 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
273 |
val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
274 |
in (names'', prem :: prems') end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
275 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
276 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
277 |
val pred = lookup_pred t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
278 |
val nparams = get_nparams pred |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
279 |
val (params, args) = chop nparams args |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
280 |
val params' = map (mk_param thy lookup_pred) params |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
281 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
282 |
folds_map mk_prems' args (names', prems) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
283 |
|> map (fn (argvs, (names'', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
284 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
285 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
286 |
in (names'', prem :: prems') end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
287 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
288 |
| mk_prems'' (t as Free (_, _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
289 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
290 |
(* higher order argument call *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
291 |
val pred = lookup_pred t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
292 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
293 |
folds_map mk_prems' args (resname :: names, prems) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
294 |
|> map (fn (argvs, (names', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
295 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
296 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar])) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
297 |
in (names', prem :: prems') end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
298 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
299 |
| mk_prems'' t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
300 |
error ("Invalid term: " ^ Syntax.string_of_term_global thy t) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
301 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
302 |
map (pair resvar) (mk_prems'' f) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
303 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
304 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
305 |
mk_prems' t (names, prems) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
306 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
307 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
308 |
(* assumption: mutual recursive predicates all have the same parameters. *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
309 |
fun define_predicates specs thy = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
310 |
if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
311 |
([], thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
312 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
313 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
314 |
val consts = map fst specs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
315 |
val eqns = maps snd specs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
316 |
(*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
317 |
(* create prednames *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
318 |
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
319 |
val argss' = map (map transform_ho_arg) argss |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
320 |
val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss')) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
321 |
val preds = map pred_of funs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
322 |
val prednames = map (fst o dest_Free) preds |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
323 |
val funnames = map (fst o dest_Const) funs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
324 |
val fun_pred_names = (funnames ~~ prednames) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
325 |
(* mapping from term (Free or Const) to term *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
326 |
fun lookup_pred (Const (name, T)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
327 |
(case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
328 |
SOME c => Const (c, pred_type T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
329 |
| NONE => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
330 |
(case AList.lookup op = fun_pred_names name of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
331 |
SOME f => Free (f, pred_type T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
332 |
| NONE => Const (name, T))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
333 |
| lookup_pred (Free (name, T)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
334 |
if member op = (map fst pnames) name then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
335 |
Free (name, transform_ho_typ T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
336 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
337 |
Free (name, T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
338 |
| lookup_pred t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
339 |
error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
340 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
341 |
(* mapping from term (predicate term, not function term!) to int *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
342 |
fun get_nparams (Const (name, _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
343 |
the_default 0 (try (ind_package_get_nparams thy) name) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
344 |
| get_nparams (Free (name, _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
345 |
(if member op = prednames name then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
346 |
length pnames |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
347 |
else 0) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
348 |
| get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
349 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
350 |
(* create intro rules *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
351 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
352 |
fun mk_intros ((func, pred), (args, rhs)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
353 |
if (body_type (fastype_of func) = @{typ bool}) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
354 |
(*TODO: preprocess predicate definition of rhs *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
355 |
[Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
356 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
357 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
358 |
val names = Term.add_free_names rhs [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
359 |
in mk_prems thy (lookup_pred, get_nparams) rhs (names, []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
360 |
|> map (fn (resultt, (names', prems)) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
361 |
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
362 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
363 |
fun mk_rewr_thm (func, pred) = @{thm refl} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
364 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
365 |
case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
366 |
NONE => ([], thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
367 |
| SOME intr_ts => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
368 |
if is_some (try (map (cterm_of thy)) intr_ts) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
369 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
370 |
val (ind_result, thy') = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
371 |
Inductive.add_inductive_global (serial ()) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
372 |
{quiet_mode = false, verbose = false, kind = Thm.internalK, |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
373 |
alt_name = Binding.empty, coind = false, no_elim = false, |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
374 |
no_ind = false, skip_mono = false, fork_mono = false} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
375 |
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
376 |
pnames |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
377 |
(map (fn x => (Attrib.empty_binding, x)) intr_ts) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
378 |
[] thy |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
379 |
val prednames = map (fst o dest_Const) (#preds ind_result) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
380 |
(* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
381 |
(* add constants to my table *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
382 |
val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
383 |
val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
384 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
385 |
(specs, thy'') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
386 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
387 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
388 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
389 |
val _ = tracing "Introduction rules of function_predicate are not welltyped" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
390 |
in ([], thy) end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
391 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
392 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
393 |
(* preprocessing intro rules - uses oracle *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
394 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
395 |
(* theory -> thm -> thm *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
396 |
fun rewrite_intro thy intro = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
397 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
398 |
fun lookup_pred (Const (name, T)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
399 |
(case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
400 |
SOME c => Const (c, pred_type T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
401 |
| NONE => error ("Function " ^ name ^ " is not inductified")) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
402 |
| lookup_pred (Free (name, T)) = Free (name, T) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
403 |
| lookup_pred _ = error "lookup function is not defined!" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
404 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
405 |
fun get_nparams (Const (name, _)) = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
406 |
the_default 0 (try (ind_package_get_nparams thy) name) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
407 |
| get_nparams (Free _) = 0 |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
408 |
| get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
409 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
410 |
val intro_t = (Logic.unvarify o prop_of) intro |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
411 |
val (prems, concl) = Logic.strip_horn intro_t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
412 |
val frees = map fst (Term.add_frees intro_t []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
413 |
fun rewrite prem names = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
414 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
415 |
val t = (HOLogic.dest_Trueprop prem) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
416 |
val (lit, mk_lit) = case try HOLogic.dest_not t of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
417 |
SOME t => (t, HOLogic.mk_not) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
418 |
| NONE => (t, I) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
419 |
val (P, args) = (strip_comb lit) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
420 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
421 |
folds_map ( |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
422 |
fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)]) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
423 |
else mk_prems thy (lookup_pred, get_nparams) t) args (names, []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
424 |
|> map (fn (resargs, (names', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
425 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
426 |
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
427 |
in (prem'::prems', names') end) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
428 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
429 |
val intro_ts' = folds_map rewrite prems frees |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
430 |
|> maps (fn (prems', frees') => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
431 |
rewrite concl frees' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
432 |
|> map (fn (concl'::conclprems, _) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
433 |
Logic.list_implies ((flat prems') @ conclprems, concl'))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
434 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
435 |
map (Drule.standard o the_oracle () o cterm_of thy) intro_ts' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
436 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
437 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
438 |
end; |