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 \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close> 15ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close> 16ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close> 17ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close> 18ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close> 19ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close> 20ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close> 21ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close> 22ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close> 23ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close> 24ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close> 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>\<open>contains\<close>, 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>\<open>pred_of_set\<close>), (ii, \<^const_name>\<open>contains_pred\<close>)])], 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