src/HOL/Predicate_Compile.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 63432 ba7901e94e7b
child 67613 ce654b0e6d69
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Predicate_Compile.thy
     2     Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>A compiler for predicates defined by introduction rules\<close>
     6 
     7 theory Predicate_Compile
     8 imports Random_Sequence Quickcheck_Exhaustive
     9 keywords
    10   "code_pred" :: thy_goal and
    11   "values" :: diag
    12 begin
    13 
    14 ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
    15 ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
    16 ML_file "Tools/Predicate_Compile/core_data.ML"
    17 ML_file "Tools/Predicate_Compile/mode_inference.ML"
    18 ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
    19 ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
    20 ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
    21 ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
    22 ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
    23 ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
    24 ML_file "Tools/Predicate_Compile/predicate_compile.ML"
    25 
    26 
    27 subsection \<open>Set membership as a generator predicate\<close>
    28 
    29 text \<open>
    30   Introduce a new constant for membership to allow 
    31   fine-grained control in code equations. 
    32 \<close>
    33 
    34 definition contains :: "'a set => 'a => bool"
    35 where "contains A x \<longleftrightarrow> x : A"
    36 
    37 definition contains_pred :: "'a set => 'a => unit Predicate.pred"
    38 where "contains_pred A x = (if x : A then Predicate.single () else bot)"
    39 
    40 lemma pred_of_setE:
    41   assumes "Predicate.eval (pred_of_set A) x"
    42   obtains "contains A x"
    43 using assms by(simp add: contains_def)
    44 
    45 lemma pred_of_setI: "contains A x ==> Predicate.eval (pred_of_set A) x"
    46 by(simp add: contains_def)
    47 
    48 lemma pred_of_set_eq: "pred_of_set \<equiv> \<lambda>A. Predicate.Pred (contains A)"
    49 by(simp add: contains_def[abs_def] pred_of_set_def o_def)
    50 
    51 lemma containsI: "x \<in> A ==> contains A x" 
    52 by(simp add: contains_def)
    53 
    54 lemma containsE: assumes "contains A x"
    55   obtains A' x' where "A = A'" "x = x'" "x : A"
    56 using assms by(simp add: contains_def)
    57 
    58 lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
    59 by(simp add: contains_pred_def contains_def)
    60 
    61 lemma contains_predE: 
    62   assumes "Predicate.eval (contains_pred A x) y"
    63   obtains "contains A x"
    64 using assms by(simp add: contains_pred_def contains_def split: if_split_asm)
    65 
    66 lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)"
    67 by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI)
    68 
    69 lemma contains_pred_notI:
    70    "\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()"
    71 by(simp add: contains_pred_def contains_def not_pred_eq)
    72 
    73 setup \<open>
    74 let
    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))
    81 in
    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 = []}))
   101 end
   102 \<close>
   103 
   104 hide_const (open) contains contains_pred
   105 hide_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 
   108 end