author | wenzelm |
Mon, 12 Apr 2021 14:14:47 +0200 | |
changeset 73563 | 55b66a45bc94 |
parent 69605 | a96320074298 |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Predicate_Compile.thy |
2 |
Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
4 |
|
60758 | 5 |
section \<open>A compiler for predicates defined by introduction rules\<close> |
33250
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 |
theory Predicate_Compile |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50055
diff
changeset
|
8 |
imports Random_Sequence Quickcheck_Exhaustive |
63432 | 9 |
keywords |
10 |
"code_pred" :: thy_goal and |
|
11 |
"values" :: diag |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
begin |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
|
69605 | 14 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close> |
15 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close> |
|
16 |
ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close> |
|
17 |
ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close> |
|
18 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close> |
|
19 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close> |
|
20 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close> |
|
21 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close> |
|
22 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close> |
|
23 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close> |
|
24 |
ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close> |
|
48891 | 25 |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
26 |
|
60758 | 27 |
subsection \<open>Set membership as a generator predicate\<close> |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
28 |
|
60758 | 29 |
text \<open> |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
30 |
Introduce a new constant for membership to allow |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
31 |
fine-grained control in code equations. |
60758 | 32 |
\<close> |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
33 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
34 |
definition contains :: "'a set => 'a => bool" |
67613 | 35 |
where "contains A x \<longleftrightarrow> x \<in> A" |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
36 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
37 |
definition contains_pred :: "'a set => 'a => unit Predicate.pred" |
67613 | 38 |
where "contains_pred A x = (if x \<in> A then Predicate.single () else bot)" |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
39 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
40 |
lemma pred_of_setE: |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
41 |
assumes "Predicate.eval (pred_of_set A) x" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
42 |
obtains "contains A x" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
43 |
using assms by(simp add: contains_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
44 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
45 |
lemma pred_of_setI: "contains A x ==> Predicate.eval (pred_of_set A) x" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
46 |
by(simp add: contains_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
47 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
48 |
lemma pred_of_set_eq: "pred_of_set \<equiv> \<lambda>A. Predicate.Pred (contains A)" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
49 |
by(simp add: contains_def[abs_def] pred_of_set_def o_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
50 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
51 |
lemma containsI: "x \<in> A ==> contains A x" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
52 |
by(simp add: contains_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
53 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
54 |
lemma containsE: assumes "contains A x" |
67613 | 55 |
obtains A' x' where "A = A'" "x = x'" "x \<in> A" |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
56 |
using assms by(simp add: contains_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
57 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
58 |
lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
59 |
by(simp add: contains_pred_def contains_def) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
60 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
61 |
lemma contains_predE: |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
62 |
assumes "Predicate.eval (contains_pred A x) y" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
63 |
obtains "contains A x" |
62390 | 64 |
using assms by(simp add: contains_pred_def contains_def split: if_split_asm) |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
65 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
66 |
lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
67 |
by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
68 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
69 |
lemma contains_pred_notI: |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
70 |
"\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()" |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
71 |
by(simp add: contains_pred_def contains_def not_pred_eq) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
72 |
|
60758 | 73 |
setup \<open> |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
74 |
let |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
75 |
val Fun = Predicate_Compile_Aux.Fun |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
76 |
val Input = Predicate_Compile_Aux.Input |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
77 |
val Output = Predicate_Compile_Aux.Output |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
78 |
val Bool = Predicate_Compile_Aux.Bool |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
79 |
val io = Fun (Input, Fun (Output, Bool)) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
80 |
val ii = Fun (Input, Fun (Input, Bool)) |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
81 |
in |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
82 |
Core_Data.PredData.map (Graph.new_node |
69593 | 83 |
(\<^const_name>\<open>contains\<close>, |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
84 |
Core_Data.PredData { |
55543 | 85 |
pos = Position.thread_data (), |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
86 |
intros = [(NONE, @{thm containsI})], |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
87 |
elim = SOME @{thm containsE}, |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
88 |
preprocessed = true, |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
89 |
function_names = [(Predicate_Compile_Aux.Pred, |
69593 | 90 |
[(io, \<^const_name>\<open>pred_of_set\<close>), (ii, \<^const_name>\<open>contains_pred\<close>)])], |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
91 |
predfun_data = [ |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
92 |
(io, Core_Data.PredfunData { |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
93 |
elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI}, |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
94 |
neg_intro = NONE, definition = @{thm pred_of_set_eq} |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
95 |
}), |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
96 |
(ii, Core_Data.PredfunData { |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
97 |
elim = @{thm contains_predE}, intro = @{thm contains_predI}, |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
98 |
neg_intro = SOME @{thm contains_pred_notI}, definition = @{thm contains_pred_eq} |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
99 |
})], |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
100 |
needs_random = []})) |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset
|
101 |
end |
60758 | 102 |
\<close> |
52023
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
103 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
104 |
hide_const (open) contains contains_pred |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
105 |
hide_fact (open) pred_of_setE pred_of_setI pred_of_set_eq |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
106 |
containsI containsE contains_predI contains_predE contains_pred_eq contains_pred_notI |
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
107 |
|
b477be38a7bb
setup for set membership as a predicate for code_pred
Andreas Lochbihler
parents:
51126
diff
changeset
|
108 |
end |