more appropriate specification packages; fun_rel_def is no simp rule by default
authorhaftmann
Tue Nov 09 14:02:13 2010 +0100 (2010-11-09)
changeset 404652989f9f3aa10
parent 40464 e1db06cf6254
child 40466 c6587375088e
more appropriate specification packages; fun_rel_def is no simp rule by default
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Nov 09 14:02:12 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Nov 09 14:02:13 2010 +0100
     1.3 @@ -8,13 +8,16 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 -fun
     1.8 -  prod_rel
     1.9 +definition
    1.10 +  prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.11  where
    1.12    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    1.13  
    1.14  declare [[map prod = (prod_fun, prod_rel)]]
    1.15  
    1.16 +lemma prod_rel_apply [simp]:
    1.17 +  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.18 +  by (simp add: prod_rel_def)
    1.19  
    1.20  lemma prod_equivp[quot_equiv]:
    1.21    assumes a: "equivp R1"
    1.22 @@ -22,7 +25,7 @@
    1.23    shows "equivp (prod_rel R1 R2)"
    1.24    apply(rule equivpI)
    1.25    unfolding reflp_def symp_def transp_def
    1.26 -  apply(simp_all add: split_paired_all)
    1.27 +  apply(simp_all add: split_paired_all prod_rel_def)
    1.28    apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    1.29    apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    1.30    apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    1.31 @@ -45,7 +48,7 @@
    1.32    assumes q1: "Quotient R1 Abs1 Rep1"
    1.33    assumes q2: "Quotient R2 Abs2 Rep2"
    1.34    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    1.35 -  by simp
    1.36 +  by (auto simp add: prod_rel_def)
    1.37  
    1.38  lemma Pair_prs[quot_preserve]:
    1.39    assumes q1: "Quotient R1 Abs1 Rep1"
    1.40 @@ -59,33 +62,29 @@
    1.41    assumes "Quotient R1 Abs1 Rep1"
    1.42    assumes "Quotient R2 Abs2 Rep2"
    1.43    shows "(prod_rel R1 R2 ===> R1) fst fst"
    1.44 -  by simp
    1.45 +  by auto
    1.46  
    1.47  lemma fst_prs[quot_preserve]:
    1.48    assumes q1: "Quotient R1 Abs1 Rep1"
    1.49    assumes q2: "Quotient R2 Abs2 Rep2"
    1.50    shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    1.51 -  apply(simp add: fun_eq_iff)
    1.52 -  apply(simp add: Quotient_abs_rep[OF q1])
    1.53 -  done
    1.54 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    1.55  
    1.56  lemma snd_rsp[quot_respect]:
    1.57    assumes "Quotient R1 Abs1 Rep1"
    1.58    assumes "Quotient R2 Abs2 Rep2"
    1.59    shows "(prod_rel R1 R2 ===> R2) snd snd"
    1.60 -  by simp
    1.61 +  by auto
    1.62  
    1.63  lemma snd_prs[quot_preserve]:
    1.64    assumes q1: "Quotient R1 Abs1 Rep1"
    1.65    assumes q2: "Quotient R2 Abs2 Rep2"
    1.66    shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    1.67 -  apply(simp add: fun_eq_iff)
    1.68 -  apply(simp add: Quotient_abs_rep[OF q2])
    1.69 -  done
    1.70 +  by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    1.71  
    1.72  lemma split_rsp[quot_respect]:
    1.73    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    1.74 -  by auto
    1.75 +  by (auto intro!: fun_relI elim!: fun_relE)
    1.76  
    1.77  lemma split_prs[quot_preserve]:
    1.78    assumes q1: "Quotient R1 Abs1 Rep1"
    1.79 @@ -96,7 +95,7 @@
    1.80  lemma [quot_respect]:
    1.81    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
    1.82    prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
    1.83 -  by auto
    1.84 +  by (auto simp add: fun_rel_def)
    1.85  
    1.86  lemma [quot_preserve]:
    1.87    assumes q1: "Quotient R1 abs1 rep1"
    1.88 @@ -114,7 +113,7 @@
    1.89  
    1.90  lemma prod_fun_id[id_simps]:
    1.91    shows "prod_fun id id = id"
    1.92 -  by (simp add: prod_fun_def)
    1.93 +  by (simp add: fun_eq_iff)
    1.94  
    1.95  lemma prod_rel_eq[id_simps]:
    1.96    shows "prod_rel (op =) (op =) = (op =)"
     2.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Nov 09 14:02:12 2010 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Nov 09 14:02:13 2010 +0100
     2.3 @@ -9,15 +9,15 @@
     2.4  begin
     2.5  
     2.6  fun
     2.7 -  sum_rel
     2.8 +  sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     2.9  where
    2.10    "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    2.11  | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    2.12  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    2.13  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    2.14  
    2.15 -fun
    2.16 -  sum_map
    2.17 +primrec
    2.18 +  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
    2.19  where
    2.20    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    2.21  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    2.22 @@ -62,13 +62,13 @@
    2.23    assumes q1: "Quotient R1 Abs1 Rep1"
    2.24    assumes q2: "Quotient R2 Abs2 Rep2"
    2.25    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    2.26 -  by simp
    2.27 +  by auto
    2.28  
    2.29  lemma sum_Inr_rsp[quot_respect]:
    2.30    assumes q1: "Quotient R1 Abs1 Rep1"
    2.31    assumes q2: "Quotient R2 Abs2 Rep2"
    2.32    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    2.33 -  by simp
    2.34 +  by auto
    2.35  
    2.36  lemma sum_Inl_prs[quot_preserve]:
    2.37    assumes q1: "Quotient R1 Abs1 Rep1"