src/HOL/Predicate.thy
changeset 30430 42ea5d85edcc
parent 30378 e0247e990702
child 30948 7f699568a877
child 31105 95f66b234086
     1.1 --- a/src/HOL/Predicate.thy	Wed Mar 11 08:45:47 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Wed Mar 11 08:45:47 2009 +0100
     1.3 @@ -588,7 +588,39 @@
     1.4      by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute)
     1.5  qed
     1.6  
     1.7 -declare eq_pred_def [code, code del]
     1.8 +primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
     1.9 +    "contained Empty Q \<longleftrightarrow> True"
    1.10 +  | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
    1.11 +  | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
    1.12 +
    1.13 +lemma single_less_eq_eval:
    1.14 +  "single x \<le> P \<longleftrightarrow> eval P x"
    1.15 +  by (auto simp add: single_def less_eq_pred_def mem_def)
    1.16 +
    1.17 +lemma contained_less_eq:
    1.18 +  "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
    1.19 +  by (induct xq) (simp_all add: single_less_eq_eval)
    1.20 +
    1.21 +lemma less_eq_pred_code [code]:
    1.22 +  "Seq f \<le> Q = (case f ()
    1.23 +   of Empty \<Rightarrow> True
    1.24 +    | Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q
    1.25 +    | Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)"
    1.26 +  by (cases "f ()")
    1.27 +    (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
    1.28 +
    1.29 +lemma eq_pred_code [code]:
    1.30 +  fixes P Q :: "'a::eq pred"
    1.31 +  shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
    1.32 +  unfolding eq by auto
    1.33 +
    1.34 +lemma [code]:
    1.35 +  "pred_case f P = f (eval P)"
    1.36 +  by (cases P) simp
    1.37 +
    1.38 +lemma [code]:
    1.39 +  "pred_rec f P = f (eval P)"
    1.40 +  by (cases P) simp
    1.41  
    1.42  no_notation
    1.43    inf (infixl "\<sqinter>" 70) and
    1.44 @@ -601,6 +633,6 @@
    1.45  
    1.46  hide (open) type pred seq
    1.47  hide (open) const Pred eval single bind if_pred not_pred
    1.48 -  Empty Insert Join Seq member "apply" adjunct
    1.49 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct
    1.50  
    1.51  end