explicit code equations for some rarely used pred operations
authorhaftmann
Wed Mar 11 08:45:47 2009 +0100 (2009-03-11)
changeset 3043042ea5d85edcc
parent 30429 39acdf031548
child 30431 836b71e950b5
explicit code equations for some rarely used pred operations
src/HOL/Predicate.thy
src/HOL/Wellfounded.thy
     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
     2.1 --- a/src/HOL/Wellfounded.thy	Wed Mar 11 08:45:47 2009 +0100
     2.2 +++ b/src/HOL/Wellfounded.thy	Wed Mar 11 08:45:47 2009 +0100
     2.3 @@ -960,4 +960,10 @@
     2.4  
     2.5  declare "prod.size" [noatp]
     2.6  
     2.7 +lemma [code]:
     2.8 +  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
     2.9 +
    2.10 +lemma [code]:
    2.11 +  "pred_size f P = 0" by (cases P) simp
    2.12 +
    2.13  end