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