# HG changeset patch # User Cezary Kaliszyk # Date 1272009282 -7200 # Node ID 3641d055b260dfb4af798644d543996ec8ac0a1f # Parent ffca58ce9fbc03baddf0b70c9e8928be41ae46c7 Further cleaning of proofs in FSet diff -r ffca58ce9fbc -r 3641d055b260 Nominal/FSet.thy --- 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 \) r r" + by (rule list_rel_refl) (metis equivp_def fset_equivp) + lemma compose_list_refl: shows "(list_rel op \ OOO op \) r r" proof - show c: "list_rel op \ r r" by (rule list_rel_refl) (metis equivp_def fset_equivp) + show c: "list_rel op \ r r" by (rule list_rel_refl) have d: "r \ r" by (rule equivp_reflp[OF fset_equivp]) show b: "(op \ OO list_rel op \) r r" by (rule pred_compI) (rule d, rule c) qed -lemma list_rel_refl: - shows "(list_rel op \) r r" - by (rule list_rel_refl)(metis equivp_def fset_equivp) - lemma Quotient_fset_list: shows "Quotient (list_rel op \) (map abs_fset) (map rep_fset)" by (fact list_quotient[OF Quotient_fset]) @@ -123,13 +123,14 @@ assume d: "b \ ba" assume e: "list_rel op \ 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 \ 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 \ 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 \ OOO op \) r r \ (list_rel op \ OOO op \) s s \ 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 ("_ |\| _" [50, 51] 50) + fin (infix "|\|" 50) where "fin :: 'a \ 'a fset \ bool" is "memb" abbreviation - fnotin :: "'a \ 'a fset \ bool" ("_ |\| _" [50, 51] 50) + fnotin :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" @@ -527,7 +528,7 @@ text {* Compositional Respectfullness and Preservation *} lemma [quot_respect]: "(list_rel op \ OOO op \) [] []" - by (metis nil_rsp list_rel.simps(1) pred_compI) + by (fact compose_list_refl) lemma [quot_preserve]: "(abs_fset \ 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 \ rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) op @ = funion" + "((map rep_fset \ rep_fset) ---> (map rep_fset \ rep_fset) ---> (abs_fset \ 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 \ x x'" shows "list_rel op \ (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 \ x x'" @@ -672,11 +671,7 @@ assumes a: "fcard_raw A = Suc n" shows "\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 \ ys \ delete_raw xs x \ 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 \ 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 "\x. \ 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 \ r` by simp - then show ?case using z list_eq2_refl by simp -next - case (Suc m) - have b: "l \ r" by fact - have d: "fcard_raw l = Suc m" by fact - have "\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 \ 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 \ r) \ (list_eq2 l r)" proof show "list_eq2 l r \ l \ r" by (induct rule: list_eq2.induct) auto - show "l \ r \ list_eq2 l r" using list_eq2_equiv_aux by blast +next + { + fix n + assume a: "fcard_raw l = n" and b: "l \ 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 "\x. \ 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 \ r` by simp + then show ?case using z list_eq2_refl by simp + next + case (Suc m) + have b: "l \ r" by fact + have d: "fcard_raw l = Suc m" by fact + have "\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 \ 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 \ r \ list_eq2 l r" by blast qed text {* Lifted theorems *} @@ -936,10 +931,6 @@ shows "S |\| {||} = S" by (lifting append_Nil2) -thm sup.commute[where 'a="'a fset"] - -thm sup.assoc[where 'a="'a fset"] - lemma singleton_union_left: "{|a|} |\| 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 |\| S") - case True - have "x |\| S" by fact - then show "P (finsert x S)" using asm by simp - next - case False - have "x |\| S" by fact - then show "P (finsert x S)" using prem2 asm by simp - qed + by (cases "x |\| S") (simp_all add: asm prem2) qed lemma fset_induct2: