--- a/Nominal/FSet.thy Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/FSet.thy Wed Apr 21 10:09:07 2010 +0200
@@ -8,6 +8,8 @@
imports Quotient Quotient_List List
begin
+text {* Definiton of List relation and the quotient type *}
+
fun
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
@@ -15,10 +17,16 @@
lemma list_eq_equivp:
shows "equivp list_eq"
- unfolding equivp_reflp_symp_transp
+ unfolding equivp_reflp_symp_transp
unfolding reflp_def symp_def transp_def
by auto
+quotient_type
+ 'a fset = "'a list" / "list_eq"
+ by (rule list_eq_equivp)
+
+text {* Raw definitions *}
+
definition
memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -29,24 +37,188 @@
where
"sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
-quotient_type
- 'a fset = "'a list" / "list_eq"
-by (rule list_eq_equivp)
+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))"
-lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
- by (simp add: sub_list_def)
+primrec
+ finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ "finter_raw [] l = []"
+| "finter_raw (h # t) l =
+ (if memb h l then h # (finter_raw t l) else finter_raw t l)"
-lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
- by (simp add: sub_list_def)
+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))"
+
+definition
+ rsp_fold
+where
+ "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
-lemma [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
- by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
+primrec
+ ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+where
+ "ffold_raw f z [] = z"
+| "ffold_raw f z (a # A) =
+ (if (rsp_fold f) then
+ if memb a A then ffold_raw f z A
+ else f a (ffold_raw f z A)
+ else z)"
+
+text {* Respectfullness *}
lemma [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
by auto
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+ by (auto simp add: sub_list_def)
+
+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
+
+lemma cons_rsp[quot_respect]:
+ shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+ by simp
+
+lemma map_rsp[quot_respect]:
+ shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+ by auto
+
+lemma set_rsp[quot_respect]:
+ "(op \<approx> ===> op =) set set"
+ by auto
+
+lemma list_equiv_rsp[quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+ by auto
+
+lemma not_memb_nil:
+ shows "\<not> memb x []"
+ by (simp add: memb_def)
+
+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_finter_raw:
+ "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
+ by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
+
+lemma [quot_respect]:
+ "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+ by (simp add: memb_def[symmetric] memb_finter_raw)
+
+lemma memb_delete_raw:
+ "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
+ by (induct xs arbitrary: x y) (auto simp add: memb_def)
+
+lemma [quot_respect]:
+ "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
+ by (simp add: memb_def[symmetric] memb_delete_raw)
+
+lemma fcard_raw_gt_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:
+ shows "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_gt_0 simp add: memb_def)
+
+lemma fcard_raw_rsp_aux:
+ assumes a: "xs \<approx> ys"
+ shows "fcard_raw xs = fcard_raw ys"
+ using a
+ apply (induct xs arbitrary: ys)
+ apply (auto simp add: memb_def)
+ apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
+ apply (auto)
+ apply (drule_tac x="x" in spec)
+ apply (blast)
+ apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
+ apply (simp add: fcard_raw_delete_one memb_def)
+ apply (case_tac "a \<in> set ys")
+ apply (simp only: if_True)
+ apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
+ apply (drule Suc_pred'[OF fcard_raw_gt_0])
+ apply (auto)
+ done
+
+lemma fcard_raw_rsp[quot_respect]:
+ shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+ by (simp add: fcard_raw_rsp_aux)
+
+lemma memb_absorb:
+ shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+ by (induct xs) (auto simp add: memb_def)
+
+lemma none_memb_nil:
+ "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+ by (simp add: memb_def)
+
+lemma not_memb_delete_raw_ident:
+ shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+ by (induct xs) (auto simp add: memb_def)
+
+lemma memb_commute_ffold_raw:
+ "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+ apply (induct b)
+ apply (simp_all add: not_memb_nil)
+ apply (auto)
+ apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
+ done
+
+lemma ffold_raw_rsp_pre:
+ "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+ apply (induct a arbitrary: b)
+ apply (simp add: memb_absorb memb_def none_memb_nil)
+ apply (simp)
+ apply (rule conjI)
+ apply (rule_tac [!] impI)
+ apply (rule_tac [!] conjI)
+ apply (rule_tac [!] impI)
+ apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+ apply (simp)
+ apply (simp add: memb_cons_iff memb_def)
+ apply (auto)[1]
+ apply (drule_tac x="e" in spec)
+ apply (blast)
+ apply (case_tac b)
+ apply (simp_all)
+ apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+ apply (simp only:)
+ apply (rule_tac f="f a1" in arg_cong)
+ apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+ apply (simp)
+ apply (simp add: memb_delete_raw)
+ apply (auto simp add: memb_cons_iff)[1]
+ apply (erule memb_commute_ffold_raw)
+ apply (drule_tac x="a1" in spec)
+ apply (simp add: memb_cons_iff)
+ apply (simp add: memb_cons_iff)
+ apply (case_tac b)
+ apply (simp_all)
+ done
+
+lemma [quot_respect]:
+ "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+ by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+
+text {* Distributive lattice with bot *}
+
lemma sub_list_not_eq:
"(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
by (auto simp add: sub_list_def)
@@ -63,7 +235,42 @@
"sub_list [] x"
by (simp add: sub_list_def)
-instantiation fset :: (type) bot
+lemma sub_list_append_left:
+ "sub_list x (x @ y)"
+ by (simp add: sub_list_def)
+
+lemma sub_list_append_right:
+ "sub_list y (x @ y)"
+ by (simp add: sub_list_def)
+
+lemma sub_list_inter_left:
+ shows "sub_list (finter_raw x y) x"
+ by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma sub_list_inter_right:
+ shows "sub_list (finter_raw x y) y"
+ by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma sub_list_list_eq:
+ "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
+ unfolding sub_list_def list_eq.simps by blast
+
+lemma sub_list_append:
+ "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
+ unfolding sub_list_def by auto
+
+lemma sub_list_inter:
+ "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
+ by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma append_inter_distrib:
+ "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+ apply (induct x)
+ apply (simp_all add: memb_def)
+ apply (simp add: memb_def[symmetric] memb_finter_raw)
+ by (auto simp add: memb_def)
+
+instantiation fset :: (type) "{bot,distrib_lattice}"
begin
quotient_definition
@@ -93,40 +300,6 @@
where
"xs |\<subset>| ys \<equiv> xs < ys"
-instance
-proof
- fix x y z :: "'a fset"
- show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
- unfolding less_fset by (lifting sub_list_not_eq)
- show "x |\<subseteq>| x" by (lifting sub_list_refl)
- show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
-next
- fix x y z :: "'a fset"
- assume a: "x |\<subseteq>| y"
- assume b: "y |\<subseteq>| z"
- show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
-qed
-end
-
-lemma sub_list_append_left:
- "sub_list x (x @ y)"
- by (simp add: sub_list_def)
-
-lemma sub_list_append_right:
- "sub_list y (x @ y)"
- by (simp add: sub_list_def)
-
-lemma sub_list_list_eq:
- "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
- unfolding sub_list_def list_eq.simps by blast
-
-lemma sub_list_append:
- "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
- unfolding sub_list_def by auto
-
-instantiation fset :: (type) "semilattice_sup"
-begin
-
quotient_definition
"sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
is
@@ -137,11 +310,33 @@
where
"xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
+quotient_definition
+ "inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+ "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
+abbreviation
+ finter (infixl "|\<inter>|" 65)
+where
+ "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+
instance
proof
- fix x y :: "'a fset"
+ fix x y z :: "'a fset"
+ show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+ unfolding less_fset by (lifting sub_list_not_eq)
+ show "x |\<subseteq>| x" by (lifting sub_list_refl)
+ show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
+ show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
+ show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
+ show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+next
+ fix x y z :: "'a fset"
+ assume a: "x |\<subseteq>| y"
+ assume b: "y |\<subseteq>| z"
+ show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
next
fix x y :: "'a fset"
assume a: "x |\<subseteq>| y"
@@ -152,10 +347,16 @@
assume a: "y |\<subseteq>| x"
assume b: "z |\<subseteq>| x"
show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+next
+ fix x y z :: "'a fset"
+ assume a: "x |\<subseteq>| y"
+ assume b: "x |\<subseteq>| z"
+ show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
qed
+
end
-section {* Empty fset, Finsert and Membership *}
+section {* Finsert and Membership *}
quotient_definition
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -178,18 +379,6 @@
where
"x |\<notin>| S \<equiv> \<not> (x |\<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
-
-lemma cons_rsp[quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
-
section {* Augmenting an fset -- @{const finsert} *}
lemma nil_not_cons:
@@ -197,22 +386,10 @@
and "\<not> (x # xs \<approx> [])"
by auto
-lemma not_memb_nil:
- shows "\<not> memb x []"
- by (simp add: memb_def)
-
lemma no_memb_nil:
"(\<forall>x. \<not> memb x xs) = (xs = [])"
by (simp add: memb_def)
-lemma none_memb_nil:
- "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
- by (simp add: memb_def)
-
-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)
@@ -221,10 +398,6 @@
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 id_simps)
-
section {* Singletons *}
lemma singleton_list_eq:
@@ -239,12 +412,6 @@
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"
is
@@ -254,10 +421,6 @@
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
by (induct xs) (auto simp add: memb_def)
-lemma fcard_raw_gt_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_not_memb:
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
@@ -284,10 +447,6 @@
apply auto
done
-lemma fcard_raw_delete_one:
- shows "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_gt_0 simp add: memb_def)
-
lemma fcard_raw_suc_memb:
assumes a: "fcard_raw A = Suc n"
shows "\<exists>a. memb a A"
@@ -307,32 +466,7 @@
then show ?thesis using fcard_raw_0[of A] by simp
qed
-lemma fcard_raw_rsp_aux:
- assumes a: "xs \<approx> ys"
- shows "fcard_raw xs = fcard_raw ys"
- using a
- apply(induct xs arbitrary: ys)
- apply(auto simp add: memb_def)
- apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
- apply simp
- apply auto
- apply (drule_tac x="x" in spec)
- apply blast
- apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
- apply(simp add: fcard_raw_delete_one memb_def)
- apply (case_tac "a \<in> set ys")
- apply (simp only: if_True)
- apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
- apply (drule Suc_pred'[OF fcard_raw_gt_0])
- apply auto
- done
-
-lemma fcard_raw_rsp[quot_respect]:
- shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
- by (simp add: fcard_raw_rsp_aux)
-
-
-section {* fmap and fset comprehension *}
+section {* fmap *}
quotient_definition
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
@@ -347,12 +481,6 @@
"memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
-text {* raw section *}
-
-lemma map_rsp[quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) map map"
- by auto
-
lemma cons_left_comm:
"x # y # xs \<approx> y # x # xs"
by auto
@@ -382,32 +510,10 @@
section {* deletion *}
-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 memb_delete_raw:
- "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
- by (induct xs arbitrary: x y) (auto simp add: memb_def)
-
-lemma delete_raw_rsp:
- "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
- by (simp add: memb_def[symmetric] memb_delete_raw)
-
-lemma [quot_respect]:
- "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
- by (simp add: memb_def[symmetric] memb_delete_raw)
-
lemma memb_delete_raw_ident:
shows "\<not> memb x (delete_raw xs x)"
by (induct xs) (auto simp add: memb_def)
-lemma not_memb_delete_raw_ident:
- shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
- by (induct xs) (auto simp add: memb_def)
-
lemma fset_raw_delete_raw_cases:
"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
by (induct xs) (auto simp add: memb_def)
@@ -420,100 +526,14 @@
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
by (simp add: fdelete_raw_filter fcard_raw_delete_one)
-lemma set_rsp[quot_respect]:
- "(op \<approx> ===> op =) set set"
- by auto
-definition
- rsp_fold
-where
- "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
-
-primrec
- ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
-where
- "ffold_raw f z [] = z"
-| "ffold_raw f z (a # A) =
- (if (rsp_fold f) then
- if memb a A then ffold_raw f z A
- else f a (ffold_raw f z A)
- else z)"
-
-lemma memb_commute_ffold_raw:
- "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
- apply (induct b)
- apply (simp add: not_memb_nil)
- apply (simp add: ffold_raw.simps)
- apply (rule conjI)
- apply (rule_tac [!] impI)
- apply (rule_tac [!] conjI)
- apply (rule_tac [!] impI)
- apply (simp_all add: memb_delete_raw)
- apply (simp add: memb_cons_iff)
- apply (simp add: not_memb_delete_raw_ident)
- apply (simp add: memb_cons_iff rsp_fold_def)
- done
-lemma ffold_raw_rsp_pre:
- "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
- apply (induct a arbitrary: b)
- apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
- apply (simp add: ffold_raw.simps)
- apply (rule conjI)
- apply (rule_tac [!] impI)
- apply (rule_tac [!] conjI)
- apply (rule_tac [!] impI)
- apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
- apply (simp)
- apply (simp add: memb_cons_iff memb_def)
- apply auto
- apply (drule_tac x="e" in spec)
- apply blast
- apply (case_tac b)
- apply simp_all
- apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
- apply (simp only:)
- apply (rule_tac f="f a1" in arg_cong)
- apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
- apply simp
- apply (simp add: memb_delete_raw)
- apply (auto simp add: memb_cons_iff)[1]
- apply (erule memb_commute_ffold_raw)
- apply (drule_tac x="a1" in spec)
- apply (simp add: memb_cons_iff)
- apply (simp add: memb_cons_iff)
- apply (case_tac b)
- apply simp_all
- done
-lemma [quot_respect]:
- "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
- by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
-
-primrec
- finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "finter_raw [] l = []"
-| "finter_raw (h # t) l =
- (if memb h l then h # (finter_raw t l) else finter_raw t l)"
lemma finter_raw_empty:
"finter_raw l [] = []"
by (induct l) (simp_all add: not_memb_nil)
-lemma memb_finter_raw:
- "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
- apply (induct xs)
- apply (simp add: not_memb_nil)
- apply (simp add: finter_raw.simps)
- apply (simp add: memb_cons_iff)
- apply auto
- done
-
-lemma [quot_respect]:
- "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
- by (simp add: memb_def[symmetric] memb_finter_raw)
-
section {* Constants on the Quotient Type *}
quotient_definition
@@ -528,16 +548,6 @@
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
is "ffold_raw"
-quotient_definition
- finter (infix "|\<inter>|" 50)
-where
- "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is "finter_raw"
-
-lemma funion_sym_pre:
- "xs @ ys \<approx> ys @ xs"
- by auto
-
lemma set_cong:
shows "(set x = set y) = (x \<approx> y)"
by auto
@@ -551,9 +561,6 @@
is
"concat"
-lemma list_equiv_rsp[quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
- by auto
text {* alternate formulation with a different decomposition principle
and a proof of equivalence *}
@@ -579,7 +586,7 @@
apply (case_tac "memb a (aa # A)")
apply (simp_all only: memb_cons_iff)
apply (case_tac [!] "a = aa")
- apply (simp_all add: delete_raw.simps)
+ apply (simp_all)
apply (case_tac "memb a A")
apply (auto simp add: memb_def)[2]
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
@@ -593,6 +600,10 @@
using a cons_delete_list_eq2[of e r]
by simp
+lemma delete_raw_rsp:
+ "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
+ by (simp add: memb_def[symmetric] memb_delete_raw)
+
lemma list_eq2_equiv_aux:
assumes a: "fcard_raw l = n"
and b: "l \<approx> r"
@@ -731,13 +742,9 @@
shows "S |\<union>| {||} = S"
by (lifting append_Nil2)
-lemma funion_sym:
- shows "S |\<union>| T = T |\<union>| S"
- by (lifting funion_sym_pre)
+thm sup.commute[where 'a="'a fset"]
-lemma funion_assoc:
- shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
- by (lifting append_assoc)
+thm sup.assoc[where 'a="'a fset"]
lemma singleton_union_left:
"{|a|} |\<union>| S = finsert a S"
@@ -745,7 +752,7 @@
lemma singleton_union_right:
"S |\<union>| {|a|} = finsert a S"
- by (subst funion_sym) simp
+ by (subst sup.commute) simp
section {* Induction and Cases rules for finite sets *}
--- a/Nominal/Manual/Term4.thy Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/Manual/Term4.thy Wed Apr 21 10:09:07 2010 +0200
@@ -1,5 +1,5 @@
theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
begin
atom_decl name
@@ -28,7 +28,7 @@
done
thm permute_rtrm4_permute_rtrm4_list.simps
-lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
@@ -48,42 +48,45 @@
apply simp_all
done
-(* We need sth like:
-lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
+ML {* @{term "\<Union>a"} *}
+
+lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
+apply (rule ext)
+apply (induct_tac x)
+apply simp_all
+done
notation
alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
thm alpha4_inj
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
-thm alpha4_inj_no
+lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
thm eqvts(1-2)
local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
- build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt))
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
+ build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt))
*}
-lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
+thm alpha4_eqvt
+lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
- build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}
+ build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
thm alpha4_reflp
-ML build_equivps
+lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
- (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
-lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+ (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3]
quotient_type
trm4 = rtrm4 / alpha_rtrm4
-(*and
- trm4list = "rtrm4 list" / alpha_rtrm4_list*)
by (simp_all add: alpha4_equivp)
local_setup {*
@@ -96,7 +99,6 @@
print_theorems
-
lemma fv_rtrm4_rsp:
"xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
"x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
@@ -115,31 +117,61 @@
lemma [quot_respect]:
"(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
- by (simp add: alpha4_inj)
+ by (simp add: alpha4_inj_fixed)
-(* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *)
local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
[@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
-print_theorems
-setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}
+setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *}
print_theorems
-
+(* Instead of permute for trm4_list we may need the following 2 lemmas: *)
+lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute"
+ apply (simp add: expand_fun_eq)
+ apply clarify
+ apply (rename_tac "pi" x)
+ apply (induct_tac x)
+ apply simp
+ apply simp
+ apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
+ done
-lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
- (trm4 = trm4a \<and> list_rel (op =) list lista)"
- by (lifting alpha4_inj(2))
+lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute"
+ apply simp
+ apply (rule allI)+
+ apply (induct_tac xa y rule: list_induct2')
+ apply simp_all
+ apply clarify
+ apply (erule alpha4_eqvt)
+ done
-thm bla[simplified list_rel_eq]
+ML {*
+ map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
+*}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}
ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
-.
+
+ML {*
+ map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]}
+*}
-(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)
+ML {*
+val liftd =
+ map (Local_Defs.unfold @{context} @{thms id_simps}) (
+ map (Local_Defs.fold @{context} @{thms alphas}) (
+ map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]}
+ )
+ )
+*}
+
+ML {*
+ map (lift_thm [@{typ trm4}] @{context})
+ (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
+*}
+
+ML {*
+ map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
+*}
end
--- a/Nominal/Parser.thy Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/Parser.thy Wed Apr 21 10:09:07 2010 +0200
@@ -336,7 +336,7 @@
Rsp.thy/prove_const_rsp
17) prove respects for all datatype constructors
(unfold eq_iff and alpha_gen; introduce zero permutations; simp)
-Lift.thy/quotient_lift_consts_export
+Perm.thy/quotient_lift_consts_export
18) define lifted constructors, fv, bn, alpha_bn, permutations
Perm.thy/define_lifted_perms
19) lift permutation zero and add properties to show that quotient type is in the pt typeclass