# HG changeset patch # User Cezary Kaliszyk # Date 1287146865 -32400 # Node ID 849578dd61274e36ebd9703ca5f6d3c5dcaca805 # Parent 7bd8013b903fdee835dde124a653760c0552e564 FSet tuned diff -r 7bd8013b903f -r 849578dd6127 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Fri Oct 15 21:46:45 2010 +0900 +++ b/src/HOL/Quotient_Examples/FSet.thy Fri Oct 15 21:47:45 2010 +0900 @@ -333,8 +333,8 @@ apply (simp_all) done -lemma [quot_respect]: - "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" +lemma ffold_raw_rsp[quot_respect]: + shows "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) lemma concat_rsp_pre: @@ -411,8 +411,9 @@ "xs |\| ys \ xs \ ys" definition - less_fset: - "(xs :: 'a fset) < ys \ xs \ ys \ xs \ ys" + less_fset :: "'a fset \ 'a fset \ bool" +where + "xs < ys \ xs \ ys \ xs \ (ys::'a fset)" abbreviation f_subset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) @@ -420,7 +421,7 @@ "xs |\| ys \ xs < ys" quotient_definition - "sup \ ('a fset \ 'a fset \ 'a fset)" + "sup :: 'a fset \ 'a fset \ 'a fset" is "append :: 'a list \ 'a list \ 'a list" @@ -430,9 +431,9 @@ "xs |\| ys \ sup (xs :: 'a fset) ys" quotient_definition - "inf \ ('a fset \ 'a fset \ 'a fset)" + "inf :: 'a fset \ 'a fset \ 'a fset" is - "finter_raw \ ('a list \ 'a list \ 'a list)" + "finter_raw :: 'a list \ 'a list \ 'a list" abbreviation finter (infixl "|\|" 65) @@ -448,7 +449,7 @@ proof fix x y z :: "'a fset" show "x |\| y \ x |\| y \ \ y |\| x" - unfolding less_fset + unfolding less_fset_def by (descending) (auto simp add: sub_list_def) show "x |\| x" by (descending) (simp add: sub_list_def) show "{||} |\| x" by (descending) (simp add: sub_list_def) @@ -516,12 +517,12 @@ quotient_definition "fcard :: 'a fset \ nat" is - "fcard_raw" + fcard_raw quotient_definition "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" is - "map" + map quotient_definition "fdelete :: 'a fset \ 'a \ 'a fset" @@ -1104,7 +1105,7 @@ lemma fsubset_set: shows "xs |\| ys \ fset_to_set xs \ fset_to_set ys" - unfolding less_fset by (lifting sub_list_neq_set) + unfolding less_fset_def by (lifting sub_list_neq_set) lemma ffilter_set: shows "fset_to_set (ffilter P xs) = P \ fset_to_set xs" @@ -1213,7 +1214,7 @@ lemma expand_fset_eq: shows "S = T \ (\x. (x |\| S) = (x |\| T))" - by (lifting list_eq.simps[simplified memb_def[symmetric]]) + by (descending) (auto simp add: memb_def) (* We cannot write it as "assumes .. shows" since Isabelle changes the quantifiers to schematic variables and reintroduces them in @@ -1265,9 +1266,10 @@ shows "(ffilter P xs = ffilter Q xs) = (\x. x |\| xs \ P x = Q x)" by (descending) (auto simp add: memb_def) -lemma subset_ffilter: +lemma subset_ffilter: shows "(\x. x |\| xs \ P x \ Q x) \ (x |\| xs & \ P x & Q x) \ ffilter P xs < ffilter Q xs" - unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter) + unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter) + section {* lemmas transferred from Finite_Set theory *}