Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotProd.thy
changeset 922 a2589b4bc442
parent 913 b1f55dd64481
child 925 8d51795ef54d
equal deleted inserted replaced
921:dae038c8cd69 922:a2589b4bc442 
     3 begin
 
     3 begin
 
     4 
     4 
     5 fun
 
     5 fun
 
     6   prod_rel
 
     6   prod_rel
 
     7 where
 
     7 where
 
     8   "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
 
     8   "prod_rel R1 R2 = (\<lambda>(a,b) (c,d). R1 a c \<and> R2 b d)"
 
     9 
     9 
    10 (* prod_fun is a good mapping function *)
 
    10 declare [[map * = (prod_fun, prod_rel)]]
 
    11 
    11 
    12 lemma prod_equivp:
 
    12 
       
    13 lemma prod_equivp[quot_equiv]:
 
    13   assumes a: "equivp R1"
 
    14   assumes a: "equivp R1"
 
    14   assumes b: "equivp R2"
 
    15   assumes b: "equivp R2"
 
    15   shows "equivp (prod_rel R1 R2)"
 
    16   shows "equivp (prod_rel R1 R2)"
 
    16 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 
    17 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 
    17 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])
 
    18 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])
 
    19 apply(simp only: equivp_symp[OF b])
 
    20 apply(simp only: equivp_symp[OF b])
 
    20 using equivp_transp[OF a] apply blast
 
    21 using equivp_transp[OF a] apply blast
 
    21 using equivp_transp[OF b] apply blast
 
    22 using equivp_transp[OF b] apply blast
 
    22 done
 
    23 done
 
    23 
    24 
    24 lemma prod_quotient:
 
    25 lemma prod_quotient[quot_thm]:
 
    25   assumes q1: "Quotient R1 Abs1 Rep1"
 
    26   assumes q1: "Quotient R1 Abs1 Rep1"
 
    26   assumes q2: "Quotient R2 Abs2 Rep2"
 
    27   assumes q2: "Quotient R2 Abs2 Rep2"
 
    27   shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
 
    28   shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
 
    28 unfolding Quotient_def
 
    29 unfolding Quotient_def
 
    29 using q1 q2
 
    30 using q1 q2
 
    30 apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep)
 
    31 apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep)
 
    31 using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast
 
    32 using Quotient_rel[OF q1] Quotient_rel[OF q2] 
       
    33 by blast
 
    32 
    34 
    33 lemma pair_rsp:
 
    35 lemma pair_rsp[quot_respect]:
 
    34   assumes q1: "Quotient R1 Abs1 Rep1"
 
    36   assumes q1: "Quotient R1 Abs1 Rep1"
 
    35   assumes q2: "Quotient R2 Abs2 Rep2"
 
    37   assumes q2: "Quotient R2 Abs2 Rep2"
 
    36   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
 
    38   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
 
    37 by auto
 
    39 by simp
 
    38 
       
    39 lemma pair_prs_aux:
 
       
    40   assumes q1: "Quotient R1 Abs1 Rep1"
 
       
    41   assumes q2: "Quotient R2 Abs2 Rep2"
 
       
    42   shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)"
 
       
    43   by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
       
    44 
    40 
    45 lemma pair_prs[quot_preserve]:
 
    41 lemma pair_prs[quot_preserve]:
 
    46   assumes q1: "Quotient R1 Abs1 Rep1"
 
    42   assumes q1: "Quotient R1 Abs1 Rep1"
 
    47   assumes q2: "Quotient R2 Abs2 Rep2"
 
    43   assumes q2: "Quotient R2 Abs2 Rep2"
 
    48   shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
 
    44   shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
 
    49 apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2])
 
    45 apply(simp add: expand_fun_eq)
 
    50 apply(simp)
 
    46 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
    51 done
 
    47 done
 
    52 
    48 
       
    49 lemma fst_rsp[quot_respect]:
 
       
    50   assumes "Quotient R1 Abs1 Rep1"
 
       
    51   assumes "Quotient R2 Abs2 Rep2"
 
       
    52   shows "(prod_rel R1 R2 ===> R1) fst fst"
 
       
    53   by simp
 
    53 
    54 
    54 
    55 lemma fst_prs[quot_preserve]:
 
    55 
       
    56 lemma fst_rsp:
 
       
    57   assumes q1: "Quotient R1 Abs1 Rep1"
 
    56   assumes q1: "Quotient R1 Abs1 Rep1"
 
    58   assumes q2: "Quotient R2 Abs2 Rep2"
 
    57   assumes q2: "Quotient R2 Abs2 Rep2"
 
    59   assumes a: "(prod_rel R1 R2) p1 p2"
 
    58   shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
 
    60   shows "R1 (fst p1) (fst p2)"
 
    59 apply(simp add: expand_fun_eq)
 
    61   using a
 
    60 apply(simp add: Quotient_abs_rep[OF q1])
 
    62   apply(case_tac p1)
 
    61 done
 
    63   apply(case_tac p2)
 
       
    64   apply(auto)
 
       
    65   done
 
       
    66 
    62 
    67 lemma snd_rsp:
 
    63 lemma snd_rsp[quot_respect]:
 
       
    64   assumes "Quotient R1 Abs1 Rep1"
 
       
    65   assumes "Quotient R2 Abs2 Rep2"
 
       
    66   shows "(prod_rel R1 R2 ===> R2) snd snd"
 
       
    67   by simp
 
       
    68   
       
    69 lemma snd_prs[quot_preserve]:
 
    68   assumes q1: "Quotient R1 Abs1 Rep1"
 
    70   assumes q1: "Quotient R1 Abs1 Rep1"
 
    69   assumes q2: "Quotient R2 Abs2 Rep2"
 
    71   assumes q2: "Quotient R2 Abs2 Rep2"
 
    70   assumes a: "(prod_rel R1 R2) p1 p2"
 
    72   shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
 
    71   shows "R2 (snd p1) (snd p2)"
 
    73 apply(simp add: expand_fun_eq)
 
    72   using a
 
    74 apply(simp add: Quotient_abs_rep[OF q2])
 
    73   apply(case_tac p1)
 
    75 done
 
    74   apply(case_tac p2)
 
       
    75   apply(auto)
 
       
    76   done
 
       
    77 
    76 
    78 lemma fst_prs:
 
    77 lemma prod_fun_id[id_simps]: 
    79   assumes q1: "Quotient R1 Abs1 Rep1"
 
    78   shows "prod_fun id id \<equiv> id"
 
    80   assumes q2: "Quotient R2 Abs2 Rep2"
 
    79   by (rule eq_reflection) 
    81   shows "Abs1 (fst ((prod_fun Rep1 Rep2) p)) = fst p"
 
    80      (simp add: prod_fun_def)
 
    82 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q1])
 
       
    83 
    81 
    84 lemma snd_prs:
 
    82 lemma prod_rel_eq[id_simps]: 
    85   assumes q1: "Quotient R1 Abs1 Rep1"
 
    83   shows "prod_rel op = op = \<equiv> op ="
 
    86   assumes q2: "Quotient R2 Abs2 Rep2"
 
       
    87   shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p"
 
       
    88 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2])
 
       
    89 
       
    90 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
 
       
    91   by (rule eq_reflection) (simp add: prod_fun_def)
 
       
    92 
       
    93 lemma prod_rel_eq[id_simps]: "prod_rel op = op = \<equiv> op ="
 
       
    94   apply (rule eq_reflection)
 
    84   apply (rule eq_reflection)
 
    95   apply (rule ext)+
 
    85   apply (rule ext)+
 
    96   apply auto
 
    86   apply auto
 
    97   done
 
    87   done
 
    98 
    88 
    99 section {* general setup for products *}
 
       
   100 
       
   101 declare [[map * = (prod_fun, prod_rel)]]
 
       
   102 
       
   103 lemmas [quot_thm] = prod_quotient
 
       
   104 lemmas [quot_respect] = pair_rsp
 
       
   105 lemmas [quot_equiv] = prod_equivp
 
       
   106 
       
   107 end
 
    89 end
nominal2