--- a/Quot/Examples/FSet3.thy Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/FSet3.thy Mon Dec 21 22:36:31 2009 +0100
@@ -1,37 +1,342 @@
theory FSet3
-imports "../QuotMain" List
+imports "../QuotMain" "../QuotList" List
begin
fun
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
- "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
+ "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
lemma list_eq_equivp:
shows "equivp list_eq"
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
by auto
-quotient_type fset = "'a list" / "list_eq"
- by (rule list_eq_equivp)
+quotient_type
+ fset = "'a list" / "list_eq"
+by (rule list_eq_equivp)
+
+
+section {* empty fset, finsert and membership *}
+
+quotient_definition
+ "fempty :: 'a fset" ("{||}")
+as "[]::'a list"
+
+quotient_definition
+ "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as "op #"
+
+syntax
+ "@Finset" :: "args => 'a fset" ("{|(_)|}")
-lemma not_nil_equiv_cons:
- "\<not>[] \<approx> a # A"
-by auto
+translations
+ "{|x, xs|}" == "CONST finsert x {|xs|}"
+ "{|x|}" == "CONST finsert x {||}"
+
+definition
+ memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+ "memb x xs \<equiv> x \<in> set xs"
+
+quotient_definition
+ "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
+as "memb"
+
+abbreviation
+ fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
+where
+ "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"
+
+lemma memb_rsp[quot_respect]:
+ shows "(op = ===> op \<approx> ===> op =) memb memb"
+by (auto simp add: memb_def)
lemma nil_rsp[quot_respect]:
shows "[] \<approx> []"
- by simp
+by simp
lemma cons_rsp[quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
- by simp
+by simp
+
+
+section {* Augmenting a set -- @{const finsert} *}
+
+text {* raw section *}
+
+lemma nil_not_cons:
+ shows "\<not>[] \<approx> x # xs"
+by auto
+
+lemma memb_cons_iff:
+ shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+by (induct xs) (auto simp add: memb_def)
+
+lemma memb_consI1:
+ shows "memb x (x # xs)"
+by (simp add: memb_def)
+
+lemma memb_consI2:
+ shows "memb x xs \<Longrightarrow> memb x (y # xs)"
+ by (simp add: memb_def)
+
+lemma memb_absorb:
+ shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"
+by (induct xs) (auto simp add: memb_def)
+
+text {* lifted section *}
+
+lemma fempty_not_finsert[simp]:
+ shows "{||} \<noteq> finsert x S"
+by (lifting nil_not_cons)
+
+lemma fin_finsert_iff[simp]:
+ "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
+by (lifting memb_cons_iff)
+
+lemma
+ shows finsertI1: "x |\<in>| finsert x S"
+ and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
+ by (lifting memb_consI1, lifting memb_consI2)
+
+lemma finsert_absorb [simp]:
+ shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
+by (lifting memb_absorb)
+
+
+section {* Singletons *}
+
+text {* raw section *}
+
+lemma singleton_list_eq:
+ shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
+by auto
+
+text {* lifted section *}
+
+lemma fsingleton_eq[simp]:
+ shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
+by (lifting singleton_list_eq)
+
+
+section {* Cardinality of finite sets *}
+
+fun
+ fcard_raw :: "'a list \<Rightarrow> nat"
+where
+ fcard_raw_nil: "fcard_raw [] = 0"
+| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
+
+quotient_definition
+ "fcard :: 'a fset \<Rightarrow> nat"
+as "fcard_raw"
+
+text {* raw section *}
+
+lemma fcard_raw_ge_0:
+ assumes a: "x \<in> set xs"
+ shows "0 < fcard_raw xs"
+using a
+by (induct xs) (auto simp add: memb_def)
+
+lemma fcard_raw_delete_one:
+ "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)
+
+lemma fcard_raw_rsp_aux:
+ assumes a: "a \<approx> b"
+ shows "fcard_raw a = fcard_raw b"
+using a
+apply(induct a arbitrary: b)
+apply(auto simp add: memb_def)
+apply(metis)
+apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)
+apply(simp add: fcard_raw_delete_one)
+apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)
+done
+
+lemma fcard_raw_rsp[quot_respect]:
+ "(op \<approx> ===> op =) fcard_raw fcard_raw"
+ by (simp add: fcard_raw_rsp_aux)
+
+text {* lifted section *}
+
+lemma fcard_fempty [simp]:
+ shows "fcard {||} = 0"
+by (lifting fcard_raw_nil)
+
+lemma fcard_finsert_if [simp]:
+ shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
+by (lifting fcard_raw_cons)
+
+
+section {* Induction and Cases rules for finite sets *}
+
+lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
+ shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (lifting list.exhaust)
+
+lemma fset_induct[case_names fempty finsert]:
+ shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
+by (lifting list.induct)
-(*
-lemma mem_rsp[quot_respect]:
- "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
+lemma fset_induct2[case_names fempty finsert, induct type: fset]:
+ assumes prem1: "P {||}"
+ and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+ shows "P S"
+proof(induct S rule: fset_induct)
+ case fempty
+ show "P {||}" by (rule prem1)
+next
+ case (finsert x S)
+ have asm: "P S" by fact
+ show "P (finsert x S)"
+ proof(cases "x |\<in>| S")
+ case True
+ have "x |\<in>| S" by fact
+ then show "P (finsert x S)" using asm by simp
+ next
+ case False
+ have "x |\<notin>| S" by fact
+ then show "P (finsert x S)" using prem2 asm by simp
+ qed
+qed
+
+
+section {* fmap and fset comprehension *}
+
+quotient_definition
+ "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+as
+ "map"
+
+(* PROPBLEM
+quotient_definition
+ "fconcat :: ('a fset) fset => 'a fset"
+as
+ "concat"
+
+term concat
+term fconcat
*)
+consts
+ fconcat :: "('a fset) fset => 'a fset"
+
+text {* raw section *}
+
+lemma map_rsp_aux:
+ assumes a: "a \<approx> b"
+ shows "map f a \<approx> map f b"
+ using a
+apply(induct a arbitrary: b)
+apply(auto)
+apply(metis rev_image_eqI)
+done
+
+lemma map_rsp[quot_respect]:
+ shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+by (auto simp add: map_rsp_aux)
+
+
+text {* lifted section *}
+
+(* TBD *)
+
+text {* syntax for fset comprehensions (adapted from lists) *}
+
+nonterminals fsc_qual fsc_quals
+
+syntax
+"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset" ("{|_ . __")
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")
+"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")
+"_fsc_end" :: "fsc_quals" ("|}")
+"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")
+"_fsc_abs" :: "'a => 'b fset => 'b fset"
+
+syntax (xsymbols)
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
+syntax (HTML output)
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
+
+parse_translation (advanced) {*
+let
+ val femptyC = Syntax.const @{const_name fempty};
+ val finsertC = Syntax.const @{const_name finsert};
+ val fmapC = Syntax.const @{const_name fmap};
+ val fconcatC = Syntax.const @{const_name fconcat};
+ val IfC = Syntax.const @{const_name If};
+ fun fsingl x = finsertC $ x $ femptyC;
+
+ fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+ let
+ val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+ val e = if opti then fsingl e else e;
+ val case1 = Syntax.const "_case1" $ p $ e;
+ val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
+ $ femptyC;
+ val cs = Syntax.const "_case2" $ case1 $ case2
+ val ft = Datatype_Case.case_tr false Datatype.info_of_constr
+ ctxt [x, cs]
+ in lambda x ft end;
+
+ fun abs_tr ctxt (p as Free(s,T)) e opti =
+ let val thy = ProofContext.theory_of ctxt;
+ val s' = Sign.intern_const thy s
+ in if Sign.declared_const thy s'
+ then (pat_tr ctxt p e opti, false)
+ else (lambda p e, true)
+ end
+ | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
+
+ fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] =
+ let
+ val res = case qs of
+ Const("_fsc_end",_) => fsingl e
+ | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs];
+ in
+ IfC $ b $ res $ femptyC
+ end
+
+ | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] =
+ (case abs_tr ctxt p e true of
+ (f,true) => fmapC $ f $ es
+ | (f, false) => fconcatC $ (fmapC $ f $ es))
+
+ | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] =
+ let
+ val e' = fsc_tr ctxt [e, q, qs];
+ in
+ fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es)
+ end
+
+in [("_fsetcompr", fsc_tr)] end
+*}
+
+(* examles *)
+term "{|(x,y,z). b|}"
+term "{|x. x \<leftarrow> xs|}"
+term "{|(x,y,z). x\<leftarrow>xs|}"
+term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"
+term "{|(x,y,z). x<a, x>b|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs|}"
+term "{|(x,y). Cons True x \<leftarrow> xs|}"
+term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"
+term "{|(x,y,z). x<a, x>b, x=d|}"
+term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"
+term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"
+term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"
+
+
+(* BELOW CONSTRUCTION SITE *)
+
lemma no_mem_nil:
"(\<forall>a. a \<notin> set A) = (A = [])"
@@ -108,49 +413,9 @@
"X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
by (induct X) (auto)
-fun
- card_raw :: "'a list \<Rightarrow> nat"
-where
- card_raw_nil: "card_raw [] = 0"
-| card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))"
-lemma not_mem_card_raw:
- fixes x :: "'a"
- fixes xs :: "'a list"
- shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
- sorry
-
-lemma card_raw_suc:
- assumes c: "card_raw xs = Suc n"
- shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"
- using c apply(induct xs)
- apply(simp)
- sorry
-lemma mem_card_raw_gt_0:
- "a \<in> set A \<Longrightarrow> 0 < card_raw A"
- by (induct A) (auto)
-lemma card_raw_cons_gt_0:
- "0 < card_raw (a # A)"
- by (induct A) (auto)
-
-lemma card_raw_delete_raw:
- "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)"
-sorry
-
-lemma card_raw_rsp_aux:
- assumes e: "a \<approx> b"
- shows "card_raw a = card_raw b"
- using e sorry
-
-lemma card_raw_rsp[quot_respect]:
- "(op \<approx> ===> op =) card_raw card_raw"
- by (simp add: card_raw_rsp_aux)
-
-lemma card_raw_0:
- "(card_raw A = 0) = (A = [])"
- by (induct A) (auto)
lemma list2set_thm:
shows "set [] = {}"
@@ -209,26 +474,6 @@
section {* Constants on the Quotient Type *}
-quotient_definition
- "fempty :: 'a fset"
- as "[]::'a list"
-
-quotient_definition
- "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- as "op #"
-
-quotient_definition
- "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
- as "\<lambda>x X. x \<in> set X"
-
-abbreviation
- fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
-where
- "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
-
-quotient_definition
- "fcard :: 'a fset \<Rightarrow> nat"
- as "card_raw"
quotient_definition
"fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
@@ -271,20 +516,21 @@
thm mem_cons
thm finite_set_raw_strong_cases
-thm card_raw.simps
-thm not_mem_card_raw
-thm card_raw_suc
+(*thm card_raw.simps*)
+(*thm not_mem_card_raw*)
+(*thm card_raw_suc*)
lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
(*by (lifting card_raw_suc)*)
sorry
-thm card_raw_cons_gt_0
+(*thm card_raw_cons_gt_0
thm mem_card_raw_gt_0
thm not_nil_equiv_cons
+*)
thm delete_raw.simps
(*thm mem_delete_raw*)
-thm card_raw_delete_raw
+(*thm card_raw_delete_raw*)
thm cons_delete_raw
thm mem_cons_delete_raw
thm finite_set_raw_delete_raw_cases