# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271838279 -7200
# Node ID c8b31085cb5b59467085d1e511a4a10fa734cb39
# Parent 72cdd2af7eb4419c4ba676f80f77eec9a357b957
FSet3 cleaning part2
diff -r 72cdd2af7eb4 -r c8b31085cb5b Attic/Quot/Examples/FSet3.thy
--- a/Attic/Quot/Examples/FSet3.thy Wed Apr 21 10:20:48 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy Wed Apr 21 10:24:39 2010 +0200
@@ -150,24 +150,6 @@
apply cleaning
done
-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) *}
@@ -267,210 +249,4 @@
(* BELOW CONSTRUCTION SITE *)
-lemma no_mem_nil:
- "(\<forall>a. a \<notin> set A) = (A = [])"
-by (induct A) (auto)
-
-lemma none_mem_nil:
- "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
-by simp
-
-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"
-by (auto simp add: id_simps)
-
-lemma cons_left_idem:
- "x # x # A \<approx> x # A"
-by (auto simp add: id_simps)
-
-lemma finite_set_raw_strong_cases:
- "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
- apply (induct X)
- apply (simp)
- apply (rule disjI2)
- apply (erule disjE)
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="[]" in exI)
- apply (simp)
- apply (erule exE)+
- apply (case_tac "a = aa")
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="Y" in exI)
- apply (simp)
- apply (rule_tac x="aa" in exI)
- apply (rule_tac x="a # Y" in exI)
- apply (auto)
- done
-
-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))"
-
-lemma mem_delete_raw:
- "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
- by (induct A arbitrary: x a) (auto)
-
-lemma mem_delete_raw_ident:
- "\<not>(a \<in> set (delete_raw A a))"
-by (induct A) (auto)
-
-lemma not_mem_delete_raw_ident:
- "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:
- "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"
-sorry
-
-lemma mem_cons_delete_raw:
- "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
-sorry
-
-lemma finite_set_raw_delete_raw_cases:
- "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
- by (induct X) (auto)
-
-
-
-
-
-lemma list2set_thm:
- shows "set [] = {}"
- and "set (h # t) = insert h (set t)"
- by (auto)
-
-lemma list2set_RSP:
- "A \<approx> B \<Longrightarrow> set A = set B"
- by auto
-
-definition
- rsp_fold
-where
- "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
-
-primrec
- fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
-where
- "fold_raw f z [] = z"
-| "fold_raw f z (a # A) =
- (if (rsp_fold f) then
- if a mem A then fold_raw f z A
- else f a (fold_raw f z A)
- else z)"
-
-lemma mem_lcommuting_fold_raw:
- "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"
-sorry
-
-lemma fold_rsp[quot_respect]:
- "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
-apply(auto)
-sorry
-
-primrec
- inter_raw
-where
- "inter_raw [] B = []"
-| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"
-
-lemma mem_inter_raw:
- "x mem (inter_raw A B) = x mem A \<and> x mem B"
-sorry
-
-lemma inter_raw_RSP:
- "A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"
-sorry
-
-
-(* LIFTING DEFS *)
-
-
-section {* Constants on the Quotient Type *}
-
-
-quotient_definition
- "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
- is "delete_raw"
-
-quotient_definition
- finter ("_ \<inter>f _" [70, 71] 70)
-where
- "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is "inter_raw"
-
-quotient_definition
- "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
- is "fold_raw"
-
-quotient_definition
- "fset_to_set :: 'a fset \<Rightarrow> 'a set"
- is "set"
-
-
-section {* Lifted Theorems *}
-
-thm list.cases (* ??? *)
-
-thm cons_left_comm
-lemma "finsert a (finsert b S) = finsert b (finsert a S)"
-by (lifting cons_left_comm)
-
-thm cons_left_idem
-lemma "finsert a (finsert a S) = finsert a S"
-by (lifting cons_left_idem)
-
-(* thm MEM:
- MEM x [] = F
- MEM x (h::t) = (x=h) \/ MEM x t *)
-thm none_mem_nil
-(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)
-
-thm mem_cons
-thm finite_set_raw_strong_cases
-(*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 mem_card_raw_gt_0
-thm not_nil_equiv_cons
-*)
-thm delete_raw.simps
-(*thm mem_delete_raw*)
-(*thm card_raw_delete_raw*)
-thm cons_delete_raw
-thm mem_cons_delete_raw
-thm finite_set_raw_delete_raw_cases
-thm append.simps
-(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)
-thm inter_raw.simps
-thm mem_inter_raw
-thm fold_raw.simps
-thm list2set_thm
-thm list_eq_def
-thm list.induct
-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 *)
-(* and the following which still lifts ok *)
-lemma "funion (funion x xa) xb = funion x (funion xa xb)"
-by (lifting append_assoc)
-
end