src/HOL/Predicate_Compile.thy
changeset 52023 b477be38a7bb
parent 51126 df86080de4cb
child 55543 f0ef75c6c0d8
     1.1 --- a/src/HOL/Predicate_Compile.thy	Thu May 16 13:49:18 2013 +1000
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Thu May 16 10:08:28 2013 +0200
     1.3 @@ -23,4 +23,84 @@
     1.4  
     1.5  setup Predicate_Compile.setup
     1.6  
     1.7 +subsection {* Set membership as a generator predicate *}
     1.8 +
     1.9 +text {* 
    1.10 +  Introduce a new constant for membership to allow 
    1.11 +  fine-grained control in code equations. 
    1.12 +*}
    1.13 +
    1.14 +definition contains :: "'a set => 'a => bool"
    1.15 +where "contains A x \<longleftrightarrow> x : A"
    1.16 +
    1.17 +definition contains_pred :: "'a set => 'a => unit Predicate.pred"
    1.18 +where "contains_pred A x = (if x : A then Predicate.single () else bot)"
    1.19 +
    1.20 +lemma pred_of_setE:
    1.21 +  assumes "Predicate.eval (pred_of_set A) x"
    1.22 +  obtains "contains A x"
    1.23 +using assms by(simp add: contains_def)
    1.24 +
    1.25 +lemma pred_of_setI: "contains A x ==> Predicate.eval (pred_of_set A) x"
    1.26 +by(simp add: contains_def)
    1.27 +
    1.28 +lemma pred_of_set_eq: "pred_of_set \<equiv> \<lambda>A. Predicate.Pred (contains A)"
    1.29 +by(simp add: contains_def[abs_def] pred_of_set_def o_def)
    1.30 +
    1.31 +lemma containsI: "x \<in> A ==> contains A x" 
    1.32 +by(simp add: contains_def)
    1.33 +
    1.34 +lemma containsE: assumes "contains A x"
    1.35 +  obtains A' x' where "A = A'" "x = x'" "x : A"
    1.36 +using assms by(simp add: contains_def)
    1.37 +
    1.38 +lemma contains_predI: "contains A x ==> Predicate.eval (contains_pred A x) ()"
    1.39 +by(simp add: contains_pred_def contains_def)
    1.40 +
    1.41 +lemma contains_predE: 
    1.42 +  assumes "Predicate.eval (contains_pred A x) y"
    1.43 +  obtains "contains A x"
    1.44 +using assms by(simp add: contains_pred_def contains_def split: split_if_asm)
    1.45 +
    1.46 +lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)"
    1.47 +by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI)
    1.48 +
    1.49 +lemma contains_pred_notI:
    1.50 +   "\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()"
    1.51 +by(simp add: contains_pred_def contains_def not_pred_eq)
    1.52 +
    1.53 +setup {*
    1.54 +let
    1.55 +  val Fun = Predicate_Compile_Aux.Fun
    1.56 +  val Input = Predicate_Compile_Aux.Input
    1.57 +  val Output = Predicate_Compile_Aux.Output
    1.58 +  val Bool = Predicate_Compile_Aux.Bool
    1.59 +  val io = Fun (Input, Fun (Output, Bool))
    1.60 +  val ii = Fun (Input, Fun (Input, Bool))
    1.61 +in
    1.62 +  Core_Data.PredData.map (Graph.new_node 
    1.63 +    (@{const_name contains}, 
    1.64 +     Core_Data.PredData {
    1.65 +       intros = [(NONE, @{thm containsI})], 
    1.66 +       elim = SOME @{thm containsE}, 
    1.67 +       preprocessed = true,
    1.68 +       function_names = [(Predicate_Compile_Aux.Pred, 
    1.69 +         [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], 
    1.70 +       predfun_data = [
    1.71 +         (io, Core_Data.PredfunData {
    1.72 +            elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI},
    1.73 +            neg_intro = NONE, definition = @{thm pred_of_set_eq}
    1.74 +          }),
    1.75 +         (ii, Core_Data.PredfunData {
    1.76 +            elim = @{thm contains_predE}, intro = @{thm contains_predI}, 
    1.77 +            neg_intro = SOME @{thm contains_pred_notI}, definition = @{thm contains_pred_eq}
    1.78 +          })],
    1.79 +       needs_random = []}))
    1.80  end
    1.81 +*}
    1.82 +
    1.83 +hide_const (open) contains contains_pred
    1.84 +hide_fact (open) pred_of_setE pred_of_setI pred_of_set_eq 
    1.85 +  containsI containsE contains_predI contains_predE contains_pred_eq contains_pred_notI
    1.86 +
    1.87 +end