diff -r 37285ec4387d -r e9e205b904e2 Quot/Examples/FSet3.thy
--- 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