# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1287154728 -3600 # Node ID 98e84b56543f38f4cd334bf2162df3976fcf69f7 # Parent 05f98e2ee48b44530d3cb25baffcdcd8f9c1ae4f renamed fcard_raw to card_list diff -r 05f98e2ee48b -r 98e84b56543f Nominal/FSet.thy --- a/Nominal/FSet.thy Fri Oct 15 15:56:16 2010 +0100 +++ b/Nominal/FSet.thy Fri Oct 15 15:58:48 2010 +0100 @@ -44,9 +44,9 @@ "sub_list xs ys \<equiv> set xs \<subseteq> set ys" definition - fcard_raw :: "'a list \<Rightarrow> nat" + card_list :: "'a list \<Rightarrow> nat" where - "fcard_raw xs = card (set xs)" + "card_list xs = card (set xs)" primrec finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" @@ -212,9 +212,9 @@ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw" by simp -lemma fcard_raw_rsp[quot_respect]: - shows "(op \<approx> ===> op =) fcard_raw fcard_raw" - by (simp add: fcard_raw_def) +lemma card_list_rsp[quot_respect]: + shows "(op \<approx> ===> op =) card_list card_list" + by (simp add: card_list_def) @@ -427,7 +427,7 @@ quotient_definition "fcard :: 'a fset \<Rightarrow> nat" - is fcard_raw + is card_list quotient_definition "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" @@ -622,29 +622,29 @@ next { fix n - assume a: "fcard_raw l = n" and b: "l \<approx> r" + assume a: "card_list l = n" and b: "l \<approx> r" have "list_eq2 l r" using a b proof (induct n arbitrary: l r) case 0 - have "fcard_raw l = 0" by fact - then have "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto + have "card_list l = 0" by fact + then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto then have z: "l = []" unfolding memb_def by auto then have "r = []" using `l \<approx> r` by simp then show ?case using z list_eq2_refl by simp next case (Suc m) have b: "l \<approx> r" by fact - have d: "fcard_raw l = Suc m" by fact + have d: "card_list l = Suc m" by fact then have "\<exists>a. memb a l" - apply(simp add: fcard_raw_def memb_def) + apply(simp add: card_list_def memb_def) apply(drule card_eq_SucD) apply(blast) done then obtain a where e: "memb a l" by auto then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b unfolding memb_def by auto - have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def) + have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def) have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g]) then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5)) @@ -909,15 +909,15 @@ lemma fcard_set: shows "fcard xs = card (fset xs)" - by (lifting fcard_raw_def) + by (lifting card_list_def) lemma fcard_finsert_if [simp]: shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))" - by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb) + by (descending) (auto simp add: card_list_def memb_def insert_absorb) lemma fcard_0[simp]: shows "fcard S = 0 \<longleftrightarrow> S = {||}" - by (descending) (simp add: fcard_raw_def) + by (descending) (simp add: card_list_def) lemma fcard_fempty[simp]: shows "fcard {||} = 0" @@ -925,20 +925,20 @@ lemma fcard_1: shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})" - by (descending) (auto simp add: fcard_raw_def card_Suc_eq) + by (descending) (auto simp add: card_list_def card_Suc_eq) lemma fcard_gt_0: shows "x \<in> fset S \<Longrightarrow> 0 < fcard S" - by (descending) (auto simp add: fcard_raw_def card_gt_0_iff) + by (descending) (auto simp add: card_list_def card_gt_0_iff) lemma fcard_not_fin: shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))" - by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb) + by (descending) (auto simp add: memb_def card_list_def insert_absorb) lemma fcard_suc: shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n" apply(descending) - apply(auto simp add: fcard_raw_def memb_def) + apply(auto simp add: card_list_def memb_def) apply(drule card_eq_SucD) apply(auto) apply(rule_tac x="b" in exI) @@ -948,19 +948,19 @@ lemma fcard_delete: shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)" - by (descending) (simp add: fcard_raw_def memb_def) + by (descending) (simp add: card_list_def memb_def) lemma fcard_suc_memb: shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" apply(descending) - apply(simp add: fcard_raw_def memb_def) + apply(simp add: card_list_def memb_def) apply(drule card_eq_SucD) apply(auto) done lemma fin_fcard_not_0: shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" - by (descending) (auto simp add: fcard_raw_def memb_def) + by (descending) (auto simp add: card_list_def memb_def) lemma fcard_mono: shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"