Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/FSet.thy
changeset 2536 98e84b56543f
parent 2534 f99578469d08
child 2537 d73fa7a3e04b
equal deleted inserted replaced
2535:05f98e2ee48b 2536:98e84b56543f 
    42   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 
    42   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 
    43 where
 
    43 where
 
    44   "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
 
    44   "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
 
    45 
    45 
    46 definition
 
    46 definition
 
    47   fcard_raw :: "'a list \<Rightarrow> nat"
 
    47   card_list :: "'a list \<Rightarrow> nat"
 
    48 where
 
    48 where
 
    49   "fcard_raw xs = card (set xs)"
 
    49   "card_list xs = card (set xs)"
 
    50 
    50 
    51 primrec
 
    51 primrec
 
    52   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
    52   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
    53 where
 
    53 where
 
    54   "finter_raw [] ys = []"
 
    54   "finter_raw [] ys = []"
 
   210 
   210 
   211 lemma fminus_raw_rsp[quot_respect]:
 
   211 lemma fminus_raw_rsp[quot_respect]:
 
   212   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
 
   212   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
 
   213   by simp
 
   213   by simp
 
   214 
   214 
   215 lemma fcard_raw_rsp[quot_respect]:
 
   215 lemma card_list_rsp[quot_respect]:
 
   216   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 
   216   shows "(op \<approx> ===> op =) card_list card_list"
 
   217   by (simp add: fcard_raw_def)
 
   217   by (simp add: card_list_def)
 
   218 
   218 
   219 
   219 
   220 
   220 
   221 lemma memb_commute_ffold_raw:
 
   221 lemma memb_commute_ffold_raw:
 
   222   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
 
   222   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
 
   425 
   425 
   426 section {* Other constants on the Quotient Type *}
 
   426 section {* Other constants on the Quotient Type *}
 
   427 
   427 
   428 quotient_definition
 
   428 quotient_definition
 
   429   "fcard :: 'a fset \<Rightarrow> nat"
 
   429   "fcard :: 'a fset \<Rightarrow> nat"
 
   430   is fcard_raw
 
   430   is card_list
 
   431 
   431 
   432 quotient_definition
 
   432 quotient_definition
 
   433   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   433   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   434   is map
 
   434   is map
 
   435 
   435 
   620 proof
 
   620 proof
 
   621   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 
   621   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 
   622 next
 
   622 next
 
   623   {
 
   623   {
 
   624     fix n
 
   624     fix n
 
   625     assume a: "fcard_raw l = n" and b: "l \<approx> r"
 
   625     assume a: "card_list l = n" and b: "l \<approx> r"
 
   626     have "list_eq2 l r"
 
   626     have "list_eq2 l r"
 
   627       using a b
 
   627       using a b
 
   628     proof (induct n arbitrary: l r)
 
   628     proof (induct n arbitrary: l r)
 
   629       case 0
 
   629       case 0
 
   630       have "fcard_raw l = 0" by fact
 
   630       have "card_list l = 0" by fact
 
   631       then have "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto
 
   631       then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
 
   632       then have z: "l = []" unfolding memb_def by auto
 
   632       then have z: "l = []" unfolding memb_def by auto
 
   633       then have "r = []" using `l \<approx> r` by simp
 
   633       then have "r = []" using `l \<approx> r` by simp
 
   634       then show ?case using z list_eq2_refl by simp
 
   634       then show ?case using z list_eq2_refl by simp
 
   635     next
 
   635     next
 
   636       case (Suc m)
 
   636       case (Suc m)
 
   637       have b: "l \<approx> r" by fact
 
   637       have b: "l \<approx> r" by fact
 
   638       have d: "fcard_raw l = Suc m" by fact
 
   638       have d: "card_list l = Suc m" by fact
 
   639       then have "\<exists>a. memb a l" 
   639       then have "\<exists>a. memb a l" 
   640 	apply(simp add: fcard_raw_def memb_def)
 
   640 	apply(simp add: card_list_def memb_def)
 
   641 	apply(drule card_eq_SucD)
 
   641 	apply(drule card_eq_SucD)
 
   642 	apply(blast)
 
   642 	apply(blast)
 
   643 	done
 
   643 	done
 
   644       then obtain a where e: "memb a l" by auto
 
   644       then obtain a where e: "memb a l" by auto
 
   645       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
   645       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
   646 	unfolding memb_def by auto
 
   646 	unfolding memb_def by auto
 
   647       have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def)
 
   647       have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
 
   648       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
 
   648       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
 
   649       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
 
   649       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
 
   650       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
 
   650       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
 
   651       have i: "list_eq2 l (a # removeAll a l)"
 
   651       have i: "list_eq2 l (a # removeAll a l)"
 
   652         by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
 
   652         by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
 
   907 
   907 
   908 subsection {* fcard *}
 
   908 subsection {* fcard *}
 
   909 
   909 
   910 lemma fcard_set: 
   910 lemma fcard_set: 
   911   shows "fcard xs = card (fset xs)"
 
   911   shows "fcard xs = card (fset xs)"
 
   912   by (lifting fcard_raw_def)
 
   912   by (lifting card_list_def)
 
   913 
   913 
   914 lemma fcard_finsert_if [simp]:
 
   914 lemma fcard_finsert_if [simp]:
 
   915   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
 
   915   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
 
   916   by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
 
   916   by (descending) (auto simp add: card_list_def memb_def insert_absorb)
 
   917 
   917 
   918 lemma fcard_0[simp]:
 
   918 lemma fcard_0[simp]:
 
   919   shows "fcard S = 0 \<longleftrightarrow> S = {||}"
 
   919   shows "fcard S = 0 \<longleftrightarrow> S = {||}"
 
   920   by (descending) (simp add: fcard_raw_def)
 
   920   by (descending) (simp add: card_list_def)
 
   921 
   921 
   922 lemma fcard_fempty[simp]:
 
   922 lemma fcard_fempty[simp]:
 
   923   shows "fcard {||} = 0"
 
   923   shows "fcard {||} = 0"
 
   924   by (simp add: fcard_0)
 
   924   by (simp add: fcard_0)
 
   925 
   925 
   926 lemma fcard_1:
 
   926 lemma fcard_1:
 
   927   shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
 
   927   shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
 
   928   by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
 
   928   by (descending) (auto simp add: card_list_def card_Suc_eq)
 
   929 
   929 
   930 lemma fcard_gt_0:
 
   930 lemma fcard_gt_0:
 
   931   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
 
   931   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
 
   932   by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
 
   932   by (descending) (auto simp add: card_list_def card_gt_0_iff)
 
   933   
   933   
   934 lemma fcard_not_fin:
 
   934 lemma fcard_not_fin:
 
   935   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
 
   935   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
 
   936   by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
 
   936   by (descending) (auto simp add: memb_def card_list_def insert_absorb)
 
   937 
   937 
   938 lemma fcard_suc: 
   938 lemma fcard_suc: 
   939   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
 
   939   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
 
   940   apply(descending)
 
   940   apply(descending)
 
   941   apply(auto simp add: fcard_raw_def memb_def)
 
   941   apply(auto simp add: card_list_def memb_def)
 
   942   apply(drule card_eq_SucD)
 
   942   apply(drule card_eq_SucD)
 
   943   apply(auto)
 
   943   apply(auto)
 
   944   apply(rule_tac x="b" in exI)
 
   944   apply(rule_tac x="b" in exI)
 
   945   apply(rule_tac x="removeAll b S" in exI)
 
   945   apply(rule_tac x="removeAll b S" in exI)
 
   946   apply(auto)
 
   946   apply(auto)
 
   947   done
 
   947   done
 
   948 
   948 
   949 lemma fcard_delete:
 
   949 lemma fcard_delete:
 
   950   shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
 
   950   shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
 
   951   by (descending) (simp add: fcard_raw_def memb_def)
 
   951   by (descending) (simp add: card_list_def memb_def)
 
   952 
   952 
   953 lemma fcard_suc_memb: 
   953 lemma fcard_suc_memb: 
   954   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
 
   954   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
 
   955   apply(descending)
 
   955   apply(descending)
 
   956   apply(simp add: fcard_raw_def memb_def)
 
   956   apply(simp add: card_list_def memb_def)
 
   957   apply(drule card_eq_SucD)
 
   957   apply(drule card_eq_SucD)
 
   958   apply(auto)
 
   958   apply(auto)
 
   959   done
 
   959   done
 
   960 
   960 
   961 lemma fin_fcard_not_0: 
   961 lemma fin_fcard_not_0: 
   962   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
 
   962   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
 
   963   by (descending) (auto simp add: fcard_raw_def memb_def)
 
   963   by (descending) (auto simp add: card_list_def memb_def)
 
   964 
   964 
   965 lemma fcard_mono: 
   965 lemma fcard_mono: 
   966   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
 
   966   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
 
   967   unfolding fcard_set fsubseteq_set
 
   967   unfolding fcard_set fsubseteq_set
 
   968   by (simp add: card_mono[OF finite_fset])
 
   968   by (simp add: card_mono[OF finite_fset])
nominal2