adaptions to changes in Equiv_Relation.thy
authorhaftmann
Tue Nov 30 17:19:11 2010 +0100 (2010-11-30)
changeset 4082298a5faa5aec0
parent 40821 9f32d7b8b24f
child 40823 37b25a87d7ef
adaptions to changes in Equiv_Relation.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 15:58:21 2010 +0100
     1.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 17:19:11 2010 +0100
     1.3 @@ -125,14 +125,19 @@
     1.4  | "freeargs (FNCALL F Xs) = Xs"
     1.5  
     1.6  theorem exprel_imp_eqv_freeargs:
     1.7 -     "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
     1.8 -apply (induct set: exprel)
     1.9 -apply (erule_tac [4] listrel.induct) 
    1.10 -apply (simp_all add: listrel.intros)
    1.11 -apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
    1.12 -apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
    1.13 -done
    1.14 -
    1.15 +  assumes "U \<sim> V"
    1.16 +  shows "(freeargs U, freeargs V) \<in> listrel exprel"
    1.17 +proof -
    1.18 +  from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
    1.19 +  from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
    1.20 +  from assms show ?thesis
    1.21 +    apply induct
    1.22 +    apply (erule_tac [4] listrel.induct) 
    1.23 +    apply (simp_all add: listrel.intros)
    1.24 +    apply (blast intro: symD [OF sym])
    1.25 +    apply (blast intro: transD [OF trans])
    1.26 +    done
    1.27 +qed
    1.28  
    1.29  
    1.30  subsection{*The Initial Algebra: A Quotiented Message Type*}
    1.31 @@ -220,7 +225,7 @@
    1.32               Abs_Exp (exprel``{PLUS U V})"
    1.33  proof -
    1.34    have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
    1.35 -    by (simp add: congruent2_def exprel.PLUS)
    1.36 +    by (auto simp add: congruent2_def exprel.PLUS)
    1.37    thus ?thesis
    1.38      by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
    1.39  qed
    1.40 @@ -236,13 +241,13 @@
    1.41  
    1.42  lemma FnCall_respects: 
    1.43       "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
    1.44 -  by (simp add: congruent_def exprel.FNCALL)
    1.45 +  by (auto simp add: congruent_def exprel.FNCALL)
    1.46  
    1.47  lemma FnCall_sing:
    1.48       "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
    1.49  proof -
    1.50    have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
    1.51 -    by (simp add: congruent_def FNCALL_Cons listrel.intros)
    1.52 +    by (auto simp add: congruent_def FNCALL_Cons listrel.intros)
    1.53    thus ?thesis
    1.54      by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
    1.55  qed
    1.56 @@ -255,7 +260,7 @@
    1.57       "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
    1.58  proof -
    1.59    have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
    1.60 -    by (simp add: congruent_def exprel.FNCALL)
    1.61 +    by (auto simp add: congruent_def exprel.FNCALL)
    1.62    thus ?thesis
    1.63      by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
    1.64                    listset_Rep_Exp_Abs_Exp)
    1.65 @@ -275,7 +280,7 @@
    1.66    "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
    1.67  
    1.68  lemma vars_respects: "freevars respects exprel"
    1.69 -by (simp add: congruent_def exprel_imp_eq_freevars) 
    1.70 +by (auto simp add: congruent_def exprel_imp_eq_freevars) 
    1.71  
    1.72  text{*The extension of the function @{term vars} to lists*}
    1.73  primrec vars_list :: "exp list \<Rightarrow> nat set" where
    1.74 @@ -340,7 +345,7 @@
    1.75    "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
    1.76  
    1.77  lemma fun_respects: "(%U. {freefun U}) respects exprel"
    1.78 -by (simp add: congruent_def exprel_imp_eq_freefun) 
    1.79 +by (auto simp add: congruent_def exprel_imp_eq_freefun) 
    1.80  
    1.81  lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
    1.82  apply (cases Xs rule: eq_Abs_ExpList) 
    1.83 @@ -358,7 +363,7 @@
    1.84    by (induct set: listrel) simp_all
    1.85  
    1.86  lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
    1.87 -by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
    1.88 +by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
    1.89  
    1.90  lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
    1.91  apply (cases Xs rule: eq_Abs_ExpList) 
    1.92 @@ -387,7 +392,7 @@
    1.93    "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
    1.94  
    1.95  lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
    1.96 -by (simp add: congruent_def exprel_imp_eq_freediscrim) 
    1.97 +by (auto simp add: congruent_def exprel_imp_eq_freediscrim) 
    1.98  
    1.99  text{*Now prove the four equations for @{term discrim}*}
   1.100  
     2.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 15:58:21 2010 +0100
     2.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 17:19:11 2010 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4  lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
     2.5  proof -
     2.6    have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
     2.7 -    by (simp add: congruent_def)
     2.8 +    by (simp add: congruent_def split_paired_all)
     2.9    then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
    2.10  qed
    2.11  
     3.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 15:58:21 2010 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 17:19:11 2010 +0100
     3.3 @@ -19,11 +19,21 @@
     3.4  where
     3.5    [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
     3.6  
     3.7 +lemma list_eq_reflp:
     3.8 +  "reflp list_eq"
     3.9 +  by (auto intro: reflpI)
    3.10 +
    3.11 +lemma list_eq_symp:
    3.12 +  "symp list_eq"
    3.13 +  by (auto intro: sympI)
    3.14 +
    3.15 +lemma list_eq_transp:
    3.16 +  "transp list_eq"
    3.17 +  by (auto intro: transpI)
    3.18 +
    3.19  lemma list_eq_equivp:
    3.20 -  shows "equivp list_eq"
    3.21 -  unfolding equivp_reflp_symp_transp
    3.22 -  unfolding reflp_def symp_def transp_def
    3.23 -  by auto
    3.24 +  "equivp list_eq"
    3.25 +  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)
    3.26  
    3.27  text {* The @{text fset} type *}
    3.28  
    3.29 @@ -141,7 +151,7 @@
    3.30        \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
    3.31      then have s: "(list_all2 R OOO op \<approx>) s s" by simp
    3.32      have d: "map Abs r \<approx> map Abs s"
    3.33 -      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
    3.34 +      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
    3.35      have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
    3.36        by (rule map_list_eq_cong[OF d])
    3.37      have y: "list_all2 R (map Rep (map Abs s)) s"
    3.38 @@ -267,8 +277,11 @@
    3.39  proof (rule fun_relI, elim pred_compE)
    3.40    fix a b ba bb
    3.41    assume a: "list_all2 op \<approx> a ba"
    3.42 +  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
    3.43    assume b: "ba \<approx> bb"
    3.44 +  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
    3.45    assume c: "list_all2 op \<approx> bb b"
    3.46 +  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
    3.47    have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
    3.48    proof
    3.49      fix x
    3.50 @@ -278,9 +291,6 @@
    3.51        show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
    3.52      next
    3.53        assume e: "\<exists>xa\<in>set b. x \<in> set xa"
    3.54 -      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
    3.55 -      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
    3.56 -      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
    3.57        show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
    3.58      qed
    3.59    qed
    3.60 @@ -288,7 +298,6 @@
    3.61  qed
    3.62  
    3.63  
    3.64 -
    3.65  section {* Quotient definitions for fsets *}
    3.66  
    3.67  
    3.68 @@ -474,7 +483,7 @@
    3.69    assumes a: "reflp R"
    3.70    and b: "list_all2 R l r"
    3.71    shows "list_all2 R (z @ l) (z @ r)"
    3.72 -  by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
    3.73 +  using a b by (induct z) (auto elim: reflpE)
    3.74  
    3.75  lemma append_rsp2_pre0:
    3.76    assumes a:"list_all2 op \<approx> x x'"
    3.77 @@ -489,23 +498,14 @@
    3.78    apply (rule list_all2_refl'[OF list_eq_equivp])
    3.79    apply (simp_all del: list_eq_def)
    3.80    apply (rule list_all2_app_l)
    3.81 -  apply (simp_all add: reflp_def)
    3.82 +  apply (simp_all add: reflpI)
    3.83    done
    3.84  
    3.85  lemma append_rsp2_pre:
    3.86 -  assumes a:"list_all2 op \<approx> x x'"
    3.87 -  and     b: "list_all2 op \<approx> z z'"
    3.88 +  assumes "list_all2 op \<approx> x x'"
    3.89 +    and "list_all2 op \<approx> z z'"
    3.90    shows "list_all2 op \<approx> (x @ z) (x' @ z')"
    3.91 -  apply (rule list_all2_transp[OF fset_equivp])
    3.92 -  apply (rule append_rsp2_pre0)
    3.93 -  apply (rule a)
    3.94 -  using b apply (induct z z' rule: list_induct2')
    3.95 -  apply (simp_all only: append_Nil2)
    3.96 -  apply (rule list_all2_refl'[OF list_eq_equivp])
    3.97 -  apply simp_all
    3.98 -  apply (rule append_rsp2_pre1)
    3.99 -  apply simp
   3.100 -  done
   3.101 +  using assms by (rule list_all2_appendI)
   3.102  
   3.103  lemma append_rsp2 [quot_respect]:
   3.104    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
     4.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 15:58:21 2010 +0100
     4.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 17:19:11 2010 +0100
     4.3 @@ -1288,7 +1288,7 @@
     4.4  proof -
     4.5    have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
     4.6          respects2 realrel"
     4.7 -    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
     4.8 +    by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
     4.9    thus ?thesis
    4.10      by (simp add: real_add_def UN_UN_split_split_eq
    4.11                    UN_equiv_class2 [OF equiv_realrel equiv_realrel])
    4.12 @@ -1297,7 +1297,7 @@
    4.13  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
    4.14  proof -
    4.15    have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
    4.16 -    by (simp add: congruent_def add_commute) 
    4.17 +    by (auto simp add: congruent_def add_commute) 
    4.18    thus ?thesis
    4.19      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
    4.20  qed