# HG changeset patch # User haftmann # Date 1291133951 -3600 # Node ID 98a5faa5aec0291026e8232c63622152414187e0 # Parent 9f32d7b8b24fc6b078ecd8421e5312cace912994 adaptions to changes in Equiv_Relation.thy diff -r 9f32d7b8b24f -r 98a5faa5aec0 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 30 15:58:21 2010 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 30 17:19:11 2010 +0100 @@ -125,14 +125,19 @@ | "freeargs (FNCALL F Xs) = Xs" theorem exprel_imp_eqv_freeargs: - "U \ V \ (freeargs U, freeargs V) \ listrel exprel" -apply (induct set: exprel) -apply (erule_tac [4] listrel.induct) -apply (simp_all add: listrel.intros) -apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) -apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]]) -done - + assumes "U \ V" + shows "(freeargs U, freeargs V) \ listrel exprel" +proof - + from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE) + from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE) + from assms show ?thesis + apply induct + apply (erule_tac [4] listrel.induct) + apply (simp_all add: listrel.intros) + apply (blast intro: symD [OF sym]) + apply (blast intro: transD [OF trans]) + done +qed subsection{*The Initial Algebra: A Quotiented Message Type*} @@ -220,7 +225,7 @@ Abs_Exp (exprel``{PLUS U V})" proof - have "(\U V. exprel `` {PLUS U V}) respects2 exprel" - by (simp add: congruent2_def exprel.PLUS) + by (auto simp add: congruent2_def exprel.PLUS) thus ?thesis by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel]) qed @@ -236,13 +241,13 @@ lemma FnCall_respects: "(\Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" - by (simp add: congruent_def exprel.FNCALL) + by (auto simp add: congruent_def exprel.FNCALL) lemma FnCall_sing: "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})" proof - have "(\U. exprel `` {FNCALL F [U]}) respects exprel" - by (simp add: congruent_def FNCALL_Cons listrel.intros) + by (auto simp add: congruent_def FNCALL_Cons listrel.intros) thus ?thesis by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel]) qed @@ -255,7 +260,7 @@ "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" proof - have "(\Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" - by (simp add: congruent_def exprel.FNCALL) + by (auto simp add: congruent_def exprel.FNCALL) thus ?thesis by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel] listset_Rep_Exp_Abs_Exp) @@ -275,7 +280,7 @@ "vars X = (\U \ Rep_Exp X. freevars U)" lemma vars_respects: "freevars respects exprel" -by (simp add: congruent_def exprel_imp_eq_freevars) +by (auto simp add: congruent_def exprel_imp_eq_freevars) text{*The extension of the function @{term vars} to lists*} primrec vars_list :: "exp list \ nat set" where @@ -340,7 +345,7 @@ "fun X = the_elem (\U \ Rep_Exp X. {freefun U})" lemma fun_respects: "(%U. {freefun U}) respects exprel" -by (simp add: congruent_def exprel_imp_eq_freefun) +by (auto simp add: congruent_def exprel_imp_eq_freefun) lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F" apply (cases Xs rule: eq_Abs_ExpList) @@ -358,7 +363,7 @@ by (induct set: listrel) simp_all lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" -by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) +by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs" apply (cases Xs rule: eq_Abs_ExpList) @@ -387,7 +392,7 @@ "discrim X = the_elem (\U \ Rep_Exp X. {freediscrim U})" lemma discrim_respects: "(\U. {freediscrim U}) respects exprel" -by (simp add: congruent_def exprel_imp_eq_freediscrim) +by (auto simp add: congruent_def exprel_imp_eq_freediscrim) text{*Now prove the four equations for @{term discrim}*} diff -r 9f32d7b8b24f -r 98a5faa5aec0 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Tue Nov 30 15:58:21 2010 +0100 +++ b/src/HOL/Library/Fraction_Field.thy Tue Nov 30 17:19:11 2010 +0100 @@ -121,7 +121,7 @@ lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)" proof - have "(\x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel" - by (simp add: congruent_def) + by (simp add: congruent_def split_paired_all) then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel) qed diff -r 9f32d7b8b24f -r 98a5faa5aec0 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Tue Nov 30 15:58:21 2010 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Nov 30 17:19:11 2010 +0100 @@ -19,11 +19,21 @@ where [simp]: "list_eq xs ys \ set xs = set ys" +lemma list_eq_reflp: + "reflp list_eq" + by (auto intro: reflpI) + +lemma list_eq_symp: + "symp list_eq" + by (auto intro: sympI) + +lemma list_eq_transp: + "transp list_eq" + by (auto intro: transpI) + lemma list_eq_equivp: - shows "equivp list_eq" - unfolding equivp_reflp_symp_transp - unfolding reflp_def symp_def transp_def - by auto + "equivp list_eq" + by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp) text {* The @{text fset} type *} @@ -141,7 +151,7 @@ \ abs_fset (map Abs r) = abs_fset (map Abs s)" then have s: "(list_all2 R OOO op \) s s" by simp have d: "map Abs r \ map Abs s" - by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) + by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a) have b: "map Rep (map Abs r) \ map Rep (map Abs s)" by (rule map_list_eq_cong[OF d]) have y: "list_all2 R (map Rep (map Abs s)) s" @@ -267,8 +277,11 @@ proof (rule fun_relI, elim pred_compE) fix a b ba bb assume a: "list_all2 op \ a ba" + with list_symp [OF list_eq_symp] have a': "list_all2 op \ ba a" by (rule sympE) assume b: "ba \ bb" + with list_eq_symp have b': "bb \ ba" by (rule sympE) assume c: "list_all2 op \ bb b" + with list_symp [OF list_eq_symp] have c': "list_all2 op \ b bb" by (rule sympE) have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof fix x @@ -278,9 +291,6 @@ show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) next assume e: "\xa\set b. x \ set xa" - have a': "list_all2 op \ ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) - have b': "bb \ ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) - have c': "list_all2 op \ b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) qed qed @@ -288,7 +298,6 @@ qed - section {* Quotient definitions for fsets *} @@ -474,7 +483,7 @@ assumes a: "reflp R" and b: "list_all2 R l r" shows "list_all2 R (z @ l) (z @ r)" - by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def]) + using a b by (induct z) (auto elim: reflpE) lemma append_rsp2_pre0: assumes a:"list_all2 op \ x x'" @@ -489,23 +498,14 @@ apply (rule list_all2_refl'[OF list_eq_equivp]) apply (simp_all del: list_eq_def) apply (rule list_all2_app_l) - apply (simp_all add: reflp_def) + apply (simp_all add: reflpI) done lemma append_rsp2_pre: - assumes a:"list_all2 op \ x x'" - and b: "list_all2 op \ z z'" + assumes "list_all2 op \ x x'" + and "list_all2 op \ z z'" shows "list_all2 op \ (x @ z) (x' @ z')" - apply (rule list_all2_transp[OF fset_equivp]) - apply (rule append_rsp2_pre0) - apply (rule a) - using b apply (induct z z' rule: list_induct2') - apply (simp_all only: append_Nil2) - apply (rule list_all2_refl'[OF list_eq_equivp]) - apply simp_all - apply (rule append_rsp2_pre1) - apply simp - done + using assms by (rule list_all2_appendI) lemma append_rsp2 [quot_respect]: "(list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) append append" diff -r 9f32d7b8b24f -r 98a5faa5aec0 src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Tue Nov 30 15:58:21 2010 +0100 +++ b/src/HOL/ex/Dedekind_Real.thy Tue Nov 30 17:19:11 2010 +0100 @@ -1288,7 +1288,7 @@ proof - have "(\z w. (\(x,y). (\(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z) respects2 realrel" - by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) + by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma) thus ?thesis by (simp add: real_add_def UN_UN_split_split_eq UN_equiv_class2 [OF equiv_realrel equiv_realrel]) @@ -1297,7 +1297,7 @@ lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" proof - have "(\(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel" - by (simp add: congruent_def add_commute) + by (auto simp add: congruent_def add_commute) thus ?thesis by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) qed