FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri Oct 15 21:46:45 2010 +0900 (2010-10-15)
changeset 399947bd8013b903f
parent 39993 eebfa0b93896
child 39995 849578dd6127
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Oct 14 12:40:14 2010 +0200
     1.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Oct 15 21:46:45 2010 +0900
     1.3 @@ -26,7 +26,9 @@
     1.4    'a fset = "'a list" / "list_eq"
     1.5    by (rule list_eq_equivp)
     1.6  
     1.7 -text {* Raw definitions *}
     1.8 +text {* Raw definitions of membership, sublist, cardinality,
     1.9 +  intersection
    1.10 +*}
    1.11  
    1.12  definition
    1.13    memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
    1.14 @@ -80,7 +82,7 @@
    1.15  
    1.16  text {* Composition Quotient *}
    1.17  
    1.18 -lemma list_all2_refl:
    1.19 +lemma list_all2_refl1:
    1.20    shows "(list_all2 op \<approx>) r r"
    1.21    by (rule list_all2_refl) (metis equivp_def fset_equivp)
    1.22  
    1.23 @@ -88,7 +90,7 @@
    1.24    shows "(list_all2 op \<approx> OOO op \<approx>) r r"
    1.25  proof
    1.26    have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
    1.27 -  show "list_all2 op \<approx> r r" by (rule list_all2_refl)
    1.28 +  show "list_all2 op \<approx> r r" by (rule list_all2_refl1)
    1.29    with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
    1.30  qed
    1.31  
    1.32 @@ -112,11 +114,11 @@
    1.33    show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
    1.34      by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
    1.35    have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
    1.36 -    by (rule list_all2_refl)
    1.37 +    by (rule list_all2_refl1)
    1.38    have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
    1.39      by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
    1.40    show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
    1.41 -    by (rule, rule list_all2_refl) (rule c)
    1.42 +    by (rule, rule list_all2_refl1) (rule c)
    1.43    show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
    1.44          (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
    1.45    proof (intro iffI conjI)
    1.46 @@ -148,11 +150,11 @@
    1.47      have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
    1.48        by (rule map_rel_cong[OF d])
    1.49      have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
    1.50 -      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl[of s]])
    1.51 +      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]])
    1.52      have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
    1.53        by (rule pred_compI) (rule b, rule y)
    1.54      have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
    1.55 -      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl[of r]])
    1.56 +      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]])
    1.57      then show "(list_all2 op \<approx> OOO op \<approx>) r s"
    1.58        using a c pred_compI by simp
    1.59    qed
    1.60 @@ -160,11 +162,11 @@
    1.61  
    1.62  text {* Respectfullness *}
    1.63  
    1.64 -lemma [quot_respect]:
    1.65 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
    1.66 -  by auto
    1.67 +lemma append_rsp[quot_respect]:
    1.68 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
    1.69 +  by (simp)
    1.70  
    1.71 -lemma [quot_respect]:
    1.72 +lemma sub_list_rsp[quot_respect]:
    1.73    shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
    1.74    by (auto simp add: sub_list_def)
    1.75  
    1.76 @@ -173,11 +175,11 @@
    1.77    by (auto simp add: memb_def)
    1.78  
    1.79  lemma nil_rsp[quot_respect]:
    1.80 -  shows "[] \<approx> []"
    1.81 +  shows "(op \<approx>) Nil Nil"
    1.82    by simp
    1.83  
    1.84  lemma cons_rsp[quot_respect]:
    1.85 -  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
    1.86 +  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
    1.87    by simp
    1.88  
    1.89  lemma map_rsp[quot_respect]:
    1.90 @@ -350,7 +352,7 @@
    1.91    then show ?thesis using f i by auto
    1.92  qed
    1.93  
    1.94 -lemma [quot_respect]:
    1.95 +lemma concat_rsp[quot_respect]:
    1.96    shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
    1.97  proof (rule fun_relI, elim pred_compE)
    1.98    fix a b ba bb
    1.99 @@ -374,7 +376,7 @@
   1.100  qed
   1.101  
   1.102  lemma [quot_respect]:
   1.103 -  "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   1.104 +  shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   1.105    by auto
   1.106  
   1.107  text {* Distributive lattice with bot *}
   1.108 @@ -420,7 +422,7 @@
   1.109  quotient_definition
   1.110    "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
   1.111  is
   1.112 -  "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
   1.113 +  "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.114  
   1.115  abbreviation
   1.116    funion (infixl "|\<union>|" 65)
   1.117 @@ -490,7 +492,7 @@
   1.118  
   1.119  quotient_definition
   1.120    "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.121 -is "op #"
   1.122 +is "Cons"
   1.123  
   1.124  syntax
   1.125    "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
   1.126 @@ -552,7 +554,7 @@
   1.127    by simp
   1.128  
   1.129  lemma [quot_respect]:
   1.130 -  "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op # op #"
   1.131 +  shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
   1.132    apply auto
   1.133    apply (simp add: set_in_eq)
   1.134    apply (rule_tac b="x # b" in pred_compI)
   1.135 @@ -581,13 +583,13 @@
   1.136    assumes a:"list_all2 op \<approx> x x'"
   1.137    shows "list_all2 op \<approx> (x @ z) (x' @ z)"
   1.138    using a apply (induct x x' rule: list_induct2')
   1.139 -  by simp_all (rule list_all2_refl)
   1.140 +  by simp_all (rule list_all2_refl1)
   1.141  
   1.142  lemma append_rsp2_pre1:
   1.143    assumes a:"list_all2 op \<approx> x x'"
   1.144    shows "list_all2 op \<approx> (z @ x) (z @ x')"
   1.145    using a apply (induct x x' arbitrary: z rule: list_induct2')
   1.146 -  apply (rule list_all2_refl)
   1.147 +  apply (rule list_all2_refl1)
   1.148    apply (simp_all del: list_eq.simps)
   1.149    apply (rule list_all2_app_l)
   1.150    apply (simp_all add: reflp_def)
   1.151 @@ -602,7 +604,7 @@
   1.152    apply (rule a)
   1.153    using b apply (induct z z' rule: list_induct2')
   1.154    apply (simp_all only: append_Nil2)
   1.155 -  apply (rule list_all2_refl)
   1.156 +  apply (rule list_all2_refl1)
   1.157    apply simp_all
   1.158    apply (rule append_rsp2_pre1)
   1.159    apply simp
   1.160 @@ -1001,7 +1003,8 @@
   1.161    shows "S |\<union>| {|a|} = finsert a S"
   1.162    by (subst sup.commute) simp
   1.163  
   1.164 -section {* Induction and Cases rules for finite sets *}
   1.165 +
   1.166 +section {* Induction and Cases rules for fsets *}
   1.167  
   1.168  lemma fset_strong_cases:
   1.169    obtains "xs = {||}"
   1.170 @@ -1256,11 +1259,11 @@
   1.171  
   1.172  lemma subseteq_filter: 
   1.173    shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
   1.174 -  by (lifting sub_list_filter)
   1.175 +  by  (descending) (auto simp add: memb_def sub_list_def)
   1.176  
   1.177  lemma eq_ffilter: 
   1.178    shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
   1.179 -  by (lifting list_eq_filter)
   1.180 +  by (descending) (auto simp add: memb_def)
   1.181  
   1.182  lemma subset_ffilter: 
   1.183    shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
   1.184 @@ -1269,7 +1272,8 @@
   1.185  section {* lemmas transferred from Finite_Set theory *}
   1.186  
   1.187  text {* finiteness for finite sets holds *}
   1.188 -lemma finite_fset: "finite (fset_to_set S)"
   1.189 +lemma finite_fset [simp]: 
   1.190 +  shows "finite (fset_to_set S)"
   1.191    by (induct S) auto
   1.192  
   1.193  lemma fset_choice: