author | wenzelm |
Fri, 24 May 2013 17:00:46 +0200 | |
changeset 52131 | 366fa32ee2a3 |
parent 51317 | 0e70cc4e94e8 |
child 54229 | ca638d713ff8 |
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 |
33630
68e058d061f5
removed unnecessary oracle in the predicate compiler
bulwahn
parents:
33522
diff
changeset
|
9 |
val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory |
33250
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 pred_of_function : theory -> string -> string option |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
12 |
val add_function_predicate_translation : (term * term) -> theory -> theory |
33250
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 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33752
diff
changeset
|
18 |
open Predicate_Compile_Aux; |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
20 |
(* Table from function to inductive predicate *) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
21 |
structure Fun_Pred = Theory_Data |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
( |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
23 |
type T = (term * term) Item_Net.T; |
38760 | 24 |
val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
25 |
val extend = I; |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
26 |
val merge = Item_Net.merge; |
33250
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 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
29 |
fun lookup thy net t = |
36051
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
30 |
let |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
31 |
val poss_preds = map_filter (fn (f, p) => |
36039 | 32 |
SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p) |
36051
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
33 |
handle Pattern.MATCH => NONE) (Item_Net.retrieve net t) |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
34 |
in |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
35 |
case poss_preds of |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
36 |
[p] => SOME p |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
37 |
| _ => NONE |
810357220388
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents:
36039
diff
changeset
|
38 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
39 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
40 |
fun pred_of_function thy name = |
49323 | 41 |
case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
42 |
[] => NONE |
50056 | 43 |
| [(_, p)] => SOME (fst (dest_Const p)) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
44 |
| _ => error ("Multiple matches possible for lookup of constant " ^ name) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
45 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
46 |
fun defined_const thy name = is_some (pred_of_function thy name) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
47 |
|
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
48 |
fun add_function_predicate_translation (f, p) = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
49 |
Fun_Pred.map (Item_Net.update (f, p)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
50 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
51 |
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
|
52 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
53 |
val (Ts, T') = strip_type T |
38553
56965d8e4e11
use HOLogic.boolT and @{typ bool} more pervasively
haftmann
parents:
37591
diff
changeset
|
54 |
in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
55 |
| transform_ho_typ t = t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
56 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
57 |
fun transform_ho_arg arg = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
58 |
case (fastype_of arg) of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
59 |
(T as Type ("fun", _)) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
60 |
(case arg of |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
61 |
Free (name, _) => Free (name, transform_ho_typ T) |
35878 | 62 |
| _ => raise Fail "A non-variable term at a higher-order position") |
63 |
| _ => arg |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
64 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
65 |
fun pred_type T = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
66 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
67 |
val (Ts, T') = strip_type T |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
68 |
val Ts' = map transform_ho_typ Ts |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
69 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
70 |
(Ts' @ [T']) ---> HOLogic.boolT |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
71 |
end; |
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 |
(* 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
|
74 |
(* theory -> term -> (string list, term list list) *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
75 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
fun dest_code_eqn eqn = let |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
77 |
val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
78 |
val (func, args) = strip_comb lhs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
79 |
in ((func, args), rhs) end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
80 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
81 |
fun folds_map f xs y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
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
|
84 |
| folds_map' acc (x :: xs) y = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
85 |
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
|
86 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
folds_map' [] xs y |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
88 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
89 |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
90 |
fun keep_functions thy t = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
91 |
case try dest_Const (fst (strip_comb t)) of |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
92 |
SOME (c, _) => Predicate_Compile_Data.keep_function thy c |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
93 |
| _ => false |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
94 |
|
35875 | 95 |
fun flatten thy lookup_pred t (names, prems) = |
96 |
let |
|
97 |
fun lift t (names, prems) = |
|
98 |
case lookup_pred (Envir.eta_contract t) of |
|
99 |
SOME pred => [(pred, (names, prems))] |
|
100 |
| NONE => |
|
101 |
let |
|
102 |
val (vars, body) = strip_abs t |
|
42816
ba14eafef077
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents:
42361
diff
changeset
|
103 |
val _ = @{assert} (fastype_of body = body_type (fastype_of body)) |
35875 | 104 |
val absnames = Name.variant_list names (map fst vars) |
105 |
val frees = map2 (curry Free) absnames (map snd vars) |
|
106 |
val body' = subst_bounds (rev frees, body) |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
107 |
val resname = singleton (Name.variant_list (absnames @ names)) "res" |
35875 | 108 |
val resvar = Free (resname, fastype_of body) |
109 |
val t = flatten' body' ([], []) |
|
110 |
|> map (fn (res, (inner_names, inner_prems)) => |
|
111 |
let |
|
112 |
fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t) |
|
113 |
val vTs = |
|
114 |
fold Term.add_frees inner_prems [] |
|
50056 | 115 |
|> filter (fn (x, _) => member (op =) inner_names x) |
35875 | 116 |
val t = |
117 |
fold mk_exists vTs |
|
118 |
(foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) :: |
|
119 |
map HOLogic.dest_Trueprop inner_prems)) |
|
120 |
in |
|
121 |
t |
|
122 |
end) |
|
123 |
|> foldr1 HOLogic.mk_disj |
|
124 |
|> fold lambda (resvar :: rev frees) |
|
125 |
in |
|
126 |
[(t, (names, prems))] |
|
127 |
end |
|
128 |
and flatten_or_lift (t, T) (names, prems) = |
|
129 |
if fastype_of t = T then |
|
130 |
flatten' t (names, prems) |
|
131 |
else |
|
132 |
(* note pred_type might be to general! *) |
|
133 |
if (pred_type (fastype_of t) = T) then |
|
134 |
lift t (names, prems) |
|
135 |
else |
|
136 |
error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^ |
|
137 |
", " ^ Syntax.string_of_typ_global thy T) |
|
50056 | 138 |
and flatten' (t as Const _) (names, prems) = [(t, (names, prems))] |
139 |
| flatten' (t as Free _) (names, prems) = [(t, (names, prems))] |
|
35875 | 140 |
| flatten' (t as Abs _) (names, prems) = [(t, (names, prems))] |
141 |
| flatten' (t as _ $ _) (names, prems) = |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
142 |
if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
143 |
[(t, (names, prems))] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
144 |
else |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
145 |
case (fst (strip_comb t)) of |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
146 |
Const (@{const_name "If"}, _) => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
147 |
(let |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
148 |
val (_, [B, x, y]) = strip_comb t |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
149 |
in |
35875 | 150 |
flatten' B (names, prems) |
151 |
|> maps (fn (B', (names, prems)) => |
|
152 |
(flatten' x (names, prems) |
|
153 |
|> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B') :: prems)))) |
|
154 |
@ (flatten' y (names, prems) |
|
155 |
|> map (fn (res, (names, prems)) => |
|
156 |
(* in general unsound! *) |
|
157 |
(res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems))))) |
|
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
158 |
end) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
159 |
| Const (@{const_name "Let"}, _) => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
160 |
(let |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
161 |
val (_, [f, g]) = strip_comb t |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
162 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
163 |
flatten' f (names, prems) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
164 |
|> maps (fn (res, (names, prems)) => |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
165 |
flatten' (betapply (g, res)) (names, prems)) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
166 |
end) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
167 |
| _ => |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35878
diff
changeset
|
168 |
case find_split_thm thy (fst (strip_comb t)) of |
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35878
diff
changeset
|
169 |
SOME raw_split_thm => |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
170 |
let |
42361 | 171 |
val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35878
diff
changeset
|
172 |
val (assms, concl) = Logic.strip_horn (prop_of split_thm) |
50056 | 173 |
val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) |
39802
7cadad6a18cc
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
bulwahn
parents:
39797
diff
changeset
|
174 |
val t' = case_betapply thy t |
7cadad6a18cc
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
bulwahn
parents:
39797
diff
changeset
|
175 |
val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty) |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
176 |
fun flatten_of_assm assm = |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
177 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
183 |
val (lhss : term list, rhss) = |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
184 |
split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems') |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
185 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
186 |
folds_map flatten' lhss (var_names @ names, prems) |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
187 |
|> map (fn (ress, (names, prems)) => |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
188 |
let |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
189 |
val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss) |
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
190 |
in (names, prems' @ prems) end) |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
191 |
|> maps (flatten' inner_t) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
192 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
193 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
194 |
maps flatten_of_assm assms |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
195 |
end |
36029
a790b94e090c
removing fishing for split thm in the predicate compiler
bulwahn
parents:
35878
diff
changeset
|
196 |
| NONE => |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
197 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
198 |
val (f, args) = strip_comb t |
52131 | 199 |
val args = map (Envir.eta_long []) args |
42816
ba14eafef077
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents:
42361
diff
changeset
|
200 |
val _ = @{assert} (fastype_of t = body_type (fastype_of t)) |
35875 | 201 |
val f' = lookup_pred f |
202 |
val Ts = case f' of |
|
35873 | 203 |
SOME pred => (fst (split_last (binder_types (fastype_of pred)))) |
35875 | 204 |
| NONE => binder_types (fastype_of f) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
205 |
in |
35875 | 206 |
folds_map flatten_or_lift (args ~~ Ts) (names, prems) |> |
207 |
(case f' of |
|
208 |
NONE => |
|
209 |
map (fn (argvs, (names', prems')) => (list_comb (f, argvs), (names', prems'))) |
|
210 |
| SOME pred => |
|
211 |
map (fn (argvs, (names', prems')) => |
|
212 |
let |
|
213 |
fun lift_arg T t = |
|
214 |
if (fastype_of t) = T then t |
|
215 |
else |
|
216 |
let |
|
42816
ba14eafef077
eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents:
42361
diff
changeset
|
217 |
val _ = @{assert} (T = |
35875 | 218 |
(binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool})) |
219 |
fun mk_if T (b, t, e) = |
|
220 |
Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e |
|
221 |
val Ts = binder_types (fastype_of t) |
|
35878 | 222 |
in |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
43326
diff
changeset
|
223 |
fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})]) |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
43326
diff
changeset
|
224 |
(mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)), |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
43326
diff
changeset
|
225 |
HOLogic.mk_eq (@{term True}, Bound 0), |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
43326
diff
changeset
|
226 |
HOLogic.mk_eq (@{term False}, Bound 0))) |
35875 | 227 |
end |
228 |
val argvs' = map2 lift_arg Ts argvs |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42816
diff
changeset
|
229 |
val resname = singleton (Name.variant_list names') "res" |
35875 | 230 |
val resvar = Free (resname, body_type (fastype_of t)) |
231 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar])) |
|
232 |
in (resvar, (resname :: names', prem :: prems')) end)) |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
233 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
234 |
in |
52131 | 235 |
map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems)) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
236 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
237 |
|
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
238 |
(* FIXME: create new predicate name -- does not avoid nameclashing *) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
239 |
fun pred_of thy f = |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
240 |
let |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
241 |
val (name, T) = dest_Const f |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
242 |
val base_name' = (Long_Name.base_name name ^ "P") |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
243 |
val name' = Sign.full_bname thy base_name' |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
244 |
val T' = if (body_type T = @{typ bool}) then T else pred_type T |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
245 |
in |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
246 |
(name', Const (name', T')) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
247 |
end |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
248 |
|
35878 | 249 |
(* assumption: mutual recursive predicates all have the same parameters. *) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
250 |
fun define_predicates specs thy = |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
251 |
if forall (fn (const, _) => defined_const thy const) specs then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
252 |
([], thy) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
253 |
else |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
254 |
let |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
255 |
val eqns = maps snd specs |
35878 | 256 |
(* create prednames *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
257 |
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
258 |
val dst_funs = distinct (op =) funs |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
259 |
val argss' = map (map transform_ho_arg) argss |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
260 |
fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1)) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
261 |
(* FIXME: higher order arguments also occur in tuples! *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
262 |
val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss')) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
263 |
val (prednames, preds) = split_list (map (pred_of thy) funs) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
264 |
val dst_preds = distinct (op =) preds |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
265 |
val dst_prednames = distinct (op =) prednames |
35878 | 266 |
(* mapping from term (Free or Const) to term *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
267 |
val net = fold Item_Net.update |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
268 |
((dst_funs ~~ dst_preds) @ lifted_args) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
269 |
(Fun_Pred.get thy) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
270 |
fun lookup_pred t = lookup thy net t |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
271 |
(* create intro rules *) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
272 |
fun mk_intros ((func, pred), (args, rhs)) = |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
273 |
if (body_type (fastype_of func) = @{typ bool}) then |
35878 | 274 |
(* TODO: preprocess predicate definition of rhs *) |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
275 |
[Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
276 |
else |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
277 |
let |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
278 |
val names = Term.add_free_names rhs [] |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
279 |
in flatten thy lookup_pred rhs (names, []) |
50056 | 280 |
|> map (fn (resultt, (_, prems)) => |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
281 |
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
282 |
end |
35878 | 283 |
val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
284 |
val (intrs, thy') = thy |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
285 |
|> Sign.add_consts_i |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
286 |
(map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn)) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
287 |
dst_preds) |
51317 | 288 |
|> fold_map Specification.axiom |
289 |
(map (fn t => ((Binding.name ("unnamed_axiom_" ^ serial_string ()), []), t)) intr_ts) |
|
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
290 |
val specs = map (fn predname => (predname, |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
291 |
map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs))) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
292 |
dst_prednames |
35878 | 293 |
val thy'' = Fun_Pred.map |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
294 |
(fold Item_Net.update (map (pairself Logic.varify_global) |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
295 |
(dst_funs ~~ dst_preds))) thy' |
36035
d82682936c52
adding registration of functions in the function flattening
bulwahn
parents:
36029
diff
changeset
|
296 |
fun functional_mode_of T = |
d82682936c52
adding registration of functions in the function flattening
bulwahn
parents:
36029
diff
changeset
|
297 |
list_fun_mode (replicate (length (binder_types T)) Input @ [Output]) |
d82682936c52
adding registration of functions in the function flattening
bulwahn
parents:
36029
diff
changeset
|
298 |
val thy''' = fold |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
39802
diff
changeset
|
299 |
(fn (predname, Const (name, T)) => Core_Data.register_alternative_function |
36035
d82682936c52
adding registration of functions in the function flattening
bulwahn
parents:
36029
diff
changeset
|
300 |
predname (functional_mode_of T) name) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
301 |
(dst_prednames ~~ dst_funs) thy'' |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
302 |
in |
36035
d82682936c52
adding registration of functions in the function flattening
bulwahn
parents:
36029
diff
changeset
|
303 |
(specs, thy''') |
35876
ac44e2312f0a
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents:
35875
diff
changeset
|
304 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
305 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
306 |
fun rewrite_intro thy intro = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
307 |
let |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
308 |
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
309 |
(*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*) |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35411
diff
changeset
|
310 |
val intro_t = Logic.unvarify_global (prop_of intro) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
311 |
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
|
312 |
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
|
313 |
fun rewrite prem names = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
314 |
let |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
35021
diff
changeset
|
315 |
(*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
316 |
val t = HOLogic.dest_Trueprop prem |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
317 |
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
|
318 |
SOME t => (t, HOLogic.mk_not) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
319 |
| NONE => (t, I) |
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
320 |
val (P, args) = strip_comb lit |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
321 |
in |
35874
bcfa6b4b21c6
renaming mk_prems to flatten in the function flattening
bulwahn
parents:
35873
diff
changeset
|
322 |
folds_map (flatten thy lookup_pred) args (names, []) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
323 |
|> map (fn (resargs, (names', prems')) => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
324 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
325 |
val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs))) |
38954
80ce658600b0
changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
bulwahn
parents:
38760
diff
changeset
|
326 |
in (prems' @ [prem'], names') end) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
327 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
328 |
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
|
329 |
|> maps (fn (prems', frees') => |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
330 |
rewrite concl frees' |
38956 | 331 |
|> map (fn (conclprems, _) => |
332 |
let |
|
333 |
val (conclprems', concl') = split_last conclprems |
|
334 |
in |
|
335 |
Logic.list_implies ((flat prems') @ conclprems', concl') |
|
336 |
end)) |
|
36249
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
337 |
(*val _ = tracing ("Rewritten intro to " ^ |
24f2ab79b506
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents:
36051
diff
changeset
|
338 |
commas (map (Syntax.string_of_term_global thy) intro_ts'))*) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
339 |
in |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
34954
diff
changeset
|
340 |
map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts' |
33630
68e058d061f5
removed unnecessary oracle in the predicate compiler
bulwahn
parents:
33522
diff
changeset
|
341 |
end |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
342 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
343 |
end; |