equal
deleted
inserted
replaced
72 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
72 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
73 |
73 |
74 lemma cons_prs[quot_preserve]: |
74 lemma cons_prs[quot_preserve]: |
75 assumes q: "Quotient R Abs Rep" |
75 assumes q: "Quotient R Abs Rep" |
76 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
76 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
77 by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q]) |
77 by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) |
78 (simp) |
78 (simp) |
79 |
79 |
80 lemma cons_rsp[quot_respect]: |
80 lemma cons_rsp[quot_respect]: |
81 assumes q: "Quotient R Abs Rep" |
81 assumes q: "Quotient R Abs Rep" |
82 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
82 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
101 |
101 |
102 lemma map_prs[quot_preserve]: |
102 lemma map_prs[quot_preserve]: |
103 assumes a: "Quotient R1 abs1 rep1" |
103 assumes a: "Quotient R1 abs1 rep1" |
104 and b: "Quotient R2 abs2 rep2" |
104 and b: "Quotient R2 abs2 rep2" |
105 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
105 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
106 by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b]) |
106 by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) |
107 (simp) |
107 (simp) |
108 |
108 |
109 |
109 |
110 lemma map_rsp[quot_respect]: |
110 lemma map_rsp[quot_respect]: |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
127 |
127 |
128 lemma foldr_prs[quot_preserve]: |
128 lemma foldr_prs[quot_preserve]: |
129 assumes a: "Quotient R1 abs1 rep1" |
129 assumes a: "Quotient R1 abs1 rep1" |
130 and b: "Quotient R2 abs2 rep2" |
130 and b: "Quotient R2 abs2 rep2" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
132 by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b]) |
132 by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) |
133 (simp) |
133 (simp) |
134 |
134 |
135 lemma foldl_prs_aux: |
135 lemma foldl_prs_aux: |
136 assumes a: "Quotient R1 abs1 rep1" |
136 assumes a: "Quotient R1 abs1 rep1" |
137 and b: "Quotient R2 abs2 rep2" |
137 and b: "Quotient R2 abs2 rep2" |
141 |
141 |
142 lemma foldl_prs[quot_preserve]: |
142 lemma foldl_prs[quot_preserve]: |
143 assumes a: "Quotient R1 abs1 rep1" |
143 assumes a: "Quotient R1 abs1 rep1" |
144 and b: "Quotient R2 abs2 rep2" |
144 and b: "Quotient R2 abs2 rep2" |
145 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
145 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
146 by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b]) |
146 by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) |
147 (simp) |
147 (simp) |
148 |
148 |
149 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0" |
149 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0" |
150 by (induct b) (simp_all) |
150 by (induct b) (simp_all) |
151 |
151 |