--- 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 \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> 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 \<sim> V"
+ shows "(freeargs U, freeargs V) \<in> 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 "(\<lambda>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:
"(\<lambda>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 "(\<lambda>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 "(\<lambda>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 = (\<Union>U \<in> 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 \<Rightarrow> nat set" where
@@ -340,7 +345,7 @@
"fun X = the_elem (\<Union>U \<in> 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 (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
lemma discrim_respects: "(\<lambda>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}*}
--- 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 "(\<lambda>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
--- 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 \<longleftrightarrow> 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 @@
\<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
then have s: "(list_all2 R OOO op \<approx>) s s" by simp
have d: "map Abs r \<approx> 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) \<approx> 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 \<approx> a ba"
+ with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
assume b: "ba \<approx> bb"
+ with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
assume c: "list_all2 op \<approx> bb b"
+ with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
proof
fix x
@@ -278,9 +291,6 @@
show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
next
assume e: "\<exists>xa\<in>set b. x \<in> set xa"
- have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
- have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
- have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
show "\<exists>xa\<in>set a. x \<in> 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 \<approx> 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 \<approx> x x'"
- and b: "list_all2 op \<approx> z z'"
+ assumes "list_all2 op \<approx> x x'"
+ and "list_all2 op \<approx> z z'"
shows "list_all2 op \<approx> (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 \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
--- 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 "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(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 "(\<lambda>(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