--- a/Nominal/FSet.thy Thu Apr 22 17:27:24 2010 +0200
+++ b/Nominal/FSet.thy Fri Apr 23 09:54:42 2010 +0200
@@ -73,18 +73,18 @@
text {* Composition Quotient *}
+lemma list_rel_refl:
+ shows "(list_rel op \<approx>) r r"
+ by (rule list_rel_refl) (metis equivp_def fset_equivp)
+
lemma compose_list_refl:
shows "(list_rel op \<approx> OOO op \<approx>) r r"
proof
- show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp)
+ show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
qed
-lemma list_rel_refl:
- shows "(list_rel op \<approx>) r r"
- by (rule list_rel_refl)(metis equivp_def fset_equivp)
-
lemma Quotient_fset_list:
shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
by (fact list_quotient[OF Quotient_fset])
@@ -123,13 +123,14 @@
assume d: "b \<approx> ba"
assume e: "list_rel op \<approx> ba s"
have f: "map abs_fset r = map abs_fset b"
- by (metis Quotient_rel[OF Quotient_fset_list] c)
- have g: "map abs_fset s = map abs_fset ba"
- by (metis Quotient_rel[OF Quotient_fset_list] e)
- show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp
+ using Quotient_rel[OF Quotient_fset_list] c by blast
+ have "map abs_fset ba = map abs_fset s"
+ using Quotient_rel[OF Quotient_fset_list] e by blast
+ then have g: "map abs_fset s = map abs_fset ba" by simp
+ then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
qed
then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
- by (metis Quotient_rel[OF Quotient_fset])
+ using Quotient_rel[OF Quotient_fset] by blast
next
assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
\<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
@@ -256,7 +257,7 @@
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)
+ apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
done
lemma ffold_raw_rsp_pre:
@@ -486,12 +487,12 @@
"{|x|}" == "CONST finsert x {||}"
quotient_definition
- fin ("_ |\<in>| _" [50, 51] 50)
+ fin (infix "|\<in>|" 50)
where
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
abbreviation
- fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
+ fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
where
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
@@ -527,7 +528,7 @@
text {* Compositional Respectfullness and Preservation *}
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
- by (metis nil_rsp list_rel.simps(1) pred_compI)
+ by (fact compose_list_refl)
lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
by simp
@@ -548,7 +549,7 @@
abs_o_rep[OF Quotient_fset] map_id finsert_def)
lemma [quot_preserve]:
- "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
+ "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
@@ -556,15 +557,13 @@
assumes a: "reflp R"
and b: "list_rel R l r"
shows "list_rel R (z @ l) (z @ r)"
- by (induct z) (simp_all add: b, metis a reflp_def)
+ by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
lemma append_rsp2_pre0:
assumes a:"list_rel op \<approx> x x'"
shows "list_rel op \<approx> (x @ z) (x' @ z)"
using a apply (induct x x' rule: list_induct2')
- apply simp_all
- apply (rule list_rel_refl)
- done
+ by simp_all (rule list_rel_refl)
lemma append_rsp2_pre1:
assumes a:"list_rel op \<approx> x x'"
@@ -672,11 +671,7 @@
assumes a: "fcard_raw A = Suc n"
shows "\<exists>a. memb a A"
using a
- apply (induct A)
- apply simp
- apply (rule_tac x="a" in exI)
- apply (simp add: memb_def)
- done
+ by (induct A) (auto simp add: memb_def)
lemma memb_card_not_0:
assumes a: "memb a A"
@@ -781,8 +776,6 @@
apply (simp_all)
apply (case_tac "memb a A")
apply (auto simp add: memb_def)[2]
- apply (case_tac "list_eq2 (a # A) A")
- apply (metis list_eq2.intros(3) list_eq2.intros(6))
apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
@@ -798,39 +791,41 @@
"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"
- shows "list_eq2 l r"
-using a b
-proof (induct n arbitrary: l r)
- case 0
- have "fcard_raw l = 0" by fact
- then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
- then have z: "l = []" using no_memb_nil by auto
- then have "r = []" using `l \<approx> r` by simp
- then show ?case using z list_eq2_refl by simp
-next
- case (Suc m)
- have b: "l \<approx> r" by fact
- have d: "fcard_raw l = Suc m" by fact
- have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
- then obtain a where e: "memb a l" by auto
- then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
- have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
- have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
- have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
- have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
- have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
- have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
- then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
-qed
-
lemma list_eq2_equiv:
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
proof
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
- show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
+next
+ {
+ fix n
+ assume a: "fcard_raw l = n" and b: "l \<approx> r"
+ have "list_eq2 l r"
+ using a b
+ proof (induct n arbitrary: l r)
+ case 0
+ have "fcard_raw l = 0" by fact
+ then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+ then have z: "l = []" using no_memb_nil by auto
+ then have "r = []" using `l \<approx> r` by simp
+ then show ?case using z list_eq2_refl by simp
+ next
+ case (Suc m)
+ have b: "l \<approx> r" by fact
+ have d: "fcard_raw l = Suc m" by fact
+ have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+ then obtain a where e: "memb a l" by auto
+ then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
+ have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+ have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
+ have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+ have i: "list_eq2 l (a # delete_raw l a)"
+ by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+ have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
+ then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+ qed
+ }
+ then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
text {* Lifted theorems *}
@@ -936,10 +931,6 @@
shows "S |\<union>| {||} = S"
by (lifting append_Nil2)
-thm sup.commute[where 'a="'a fset"]
-
-thm sup.assoc[where 'a="'a fset"]
-
lemma singleton_union_left:
"{|a|} |\<union>| S = finsert a S"
by simp
@@ -973,15 +964,7 @@
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
+ by (cases "x |\<in>| S") (simp_all add: asm prem2)
qed
lemma fset_induct2: