--- a/Quot/Examples/FSet3.thy Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/Examples/FSet3.thy Fri Dec 11 19:19:24 2009 +0100
@@ -2,82 +2,89 @@
imports "../QuotMain" List
begin
-definition
+fun
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
- "list_eq x y = (\<forall>e. e mem x = e mem y)"
-
-lemma list_eq_reflp:
- shows "xs \<approx> xs"
- by (metis list_eq_def)
+ "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
lemma list_eq_equivp:
shows "equivp list_eq"
- unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
- apply (auto intro: list_eq_def)
- apply (metis list_eq_def)
- apply (metis list_eq_def)
- sorry
+unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+by auto
quotient fset = "'a list" / "list_eq"
by (rule list_eq_equivp)
-lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
+lemma not_nil_equiv_cons:
+ "\<not>[] \<approx> a # A"
+by auto
-(* The 2 lemmas below are different from the ones in QuotList *)
lemma nil_rsp[quot_respect]:
shows "[] \<approx> []"
-by (rule list_eq_reflp)
+ by simp
-lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *)
- " (op = ===> op \<approx> ===> op \<approx>) op # op #"
- sorry
+lemma cons_rsp[quot_respect]:
+ shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+ by simp
+(*
lemma mem_rsp[quot_respect]:
"(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
- sorry
+*)
+
-lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"
-sorry
+lemma no_mem_nil:
+ "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
+by (induct A) (auto)
-lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"
-sorry
+lemma none_mem_nil:
+ "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
+by simp
-lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"
-sorry
+lemma mem_cons:
+ "a \<in> set A \<Longrightarrow> a # A \<approx> A"
+by auto
-lemma cons_left_comm: "x # y # A \<approx> y # x # A"
-sorry
+lemma cons_left_comm:
+ "x #y # A \<approx> y # x # A"
+by auto
-lemma cons_left_idem: "x # x # A \<approx> x # A"
-sorry
+lemma cons_left_idem:
+ "x # x # A \<approx> x # A"
+by auto
lemma finite_set_raw_strong_cases:
"(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
apply (induct X)
- apply (simp)
+ apply (auto)
sorry
-primrec
+fun
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
where
"delete_raw [] x = []"
| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+(* definitely FALSE
lemma mem_delete_raw:
"x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
+apply(induct A arbitrary: x a)
+apply(auto)
sorry
+*)
lemma mem_delete_raw_ident:
- "\<not>(MEM a (A delete_raw a))"
-sorry
+ "\<not>(a \<in> set (delete_raw A a))"
+by (induct A) (auto)
lemma not_mem_delete_raw_ident:
- "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"
-sorry
+ "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
+by (induct A) (auto)
lemma delete_raw_RSP:
"A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
+apply(induct A arbitrary: B a)
+apply(auto)
sorry
lemma cons_delete_raw:
@@ -115,9 +122,11 @@
shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
using c
apply(induct xs)
-apply(metis mem_delete_raw)
+(*apply(metis mem_delete_raw)
apply(metis mem_delete_raw)
-done
+done*)
+sorry
+
lemma mem_card_raw_not_0:
"a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
@@ -174,13 +183,12 @@
lemma fold_rsp[quot_respect]:
"(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
- apply (auto)
- apply (case_tac "rsp_fold x")
+apply(auto)
sorry
lemma append_rsp[quot_respect]:
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
- sorry
+by auto
primrec
inter_raw
@@ -199,44 +207,61 @@
(* LIFTING DEFS *)
+
+section {* Constants on the Quotient Type *}
+
quotient_def
- "Empty :: 'a fset" as "[]::'a list"
+ "fempty :: 'a fset"
+ as "[]::'a list"
quotient_def
- "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"
+ "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+ as "op #"
quotient_def
- "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"
+ "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+ as "\<lambda>x X. x \<in> set X"
-quotient_def
- "Card :: 'a fset \<Rightarrow> nat" as "card_raw"
+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_def
- "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"
+ "fcard :: 'a fset \<Rightarrow> nat"
+ as "card_raw"
quotient_def
- "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"
+ "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
+ as "delete_raw"
+
+quotient_def
+ "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
+ as "op @"
quotient_def
- "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"
+ "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+ as "inter_raw"
quotient_def
- "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"
+ "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+ as "fold_raw"
quotient_def
- "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"
+ "fset_to_set :: 'a fset \<Rightarrow> 'a set"
+ as "set"
-(* LIFTING THMS *)
+section {* Lifted Theorems *}
thm list.cases (* ??? *)
thm cons_left_comm
-lemma "Insert a (Insert b x) = Insert b (Insert a x)"
+lemma "finsert a (finsert b S) = finsert b (finsert a S)"
by (lifting cons_left_comm)
thm cons_left_idem
-lemma "Insert a (Insert a x) = Insert a x"
+lemma "finsert a (finsert a S) = finsert a S"
by (lifting cons_left_idem)
(* thm MEM:
@@ -248,14 +273,16 @@
thm card_raw.simps
thm not_mem_card_raw
thm card_raw_suc
-lemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"
-by (lifting 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 mem_card_raw_not_0
thm not_nil_equiv_cons
thm delete_raw.simps
-thm mem_delete_raw
+(*thm mem_delete_raw*)
thm card_raw_delete_raw
thm cons_delete_raw
thm mem_cons_delete_raw
@@ -268,7 +295,7 @@
thm list2set_thm
thm list_eq_def
thm list.induct
-lemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"
+lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"
by (lifting list.induct)
(* We also have map and some properties of it in FSet *)
@@ -287,7 +314,7 @@
apply (auto)
sorry
-lemma "fset_case (f1::'t) f2 (Insert a xa) = f2 a xa"
+lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
apply (lifting list.cases(2))
done