90 lemma nil_rsp[quot_respect]: |
90 lemma nil_rsp[quot_respect]: |
91 assumes q: "Quotient R Abs Rep" |
91 assumes q: "Quotient R Abs Rep" |
92 shows "list_rel R [] []" |
92 shows "list_rel R [] []" |
93 by simp |
93 by simp |
94 |
94 |
95 lemma map_prs: |
95 lemma map_prs_aux: |
96 assumes a: "Quotient R1 abs1 rep1" |
96 assumes a: "Quotient R1 abs1 rep1" |
97 and b: "Quotient R2 abs2 rep2" |
97 and b: "Quotient R2 abs2 rep2" |
98 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
98 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
99 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
99 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
|
100 |
|
101 |
|
102 lemma map_prs[quot_preserve]: |
|
103 assumes a: "Quotient R1 abs1 rep1" |
|
104 and b: "Quotient R2 abs2 rep2" |
|
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]) |
|
107 (simp) |
|
108 |
100 |
109 |
101 lemma map_rsp[quot_respect]: |
110 lemma map_rsp[quot_respect]: |
102 assumes q1: "Quotient R1 Abs1 Rep1" |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
103 and q2: "Quotient R2 Abs2 Rep2" |
112 and q2: "Quotient R2 Abs2 Rep2" |
104 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
113 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
108 apply(rule allI)+ |
117 apply(rule allI)+ |
109 apply (induct_tac xa ya rule: list_induct2') |
118 apply (induct_tac xa ya rule: list_induct2') |
110 apply simp_all |
119 apply simp_all |
111 done |
120 done |
112 |
121 |
113 lemma foldr_prs: |
122 lemma foldr_prs_aux: |
114 assumes a: "Quotient R1 abs1 rep1" |
123 assumes a: "Quotient R1 abs1 rep1" |
115 and b: "Quotient R2 abs2 rep2" |
124 and b: "Quotient R2 abs2 rep2" |
116 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
125 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
117 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
126 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
118 |
127 |
119 lemma foldl_prs: |
128 lemma foldr_prs[quot_respect]: |
|
129 assumes a: "Quotient R1 abs1 rep1" |
|
130 and b: "Quotient R2 abs2 rep2" |
|
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]) |
|
133 (simp) |
|
134 |
|
135 lemma foldl_prs_aux: |
120 assumes a: "Quotient R1 abs1 rep1" |
136 assumes a: "Quotient R1 abs1 rep1" |
121 and b: "Quotient R2 abs2 rep2" |
137 and b: "Quotient R2 abs2 rep2" |
122 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
138 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
123 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
139 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
|
140 |
|
141 |
|
142 lemma foldl_prs[quot_preserve]: |
|
143 assumes a: "Quotient R1 abs1 rep1" |
|
144 and b: "Quotient R2 abs2 rep2" |
|
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]) |
|
147 (simp) |
124 |
148 |
125 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" |
126 by (induct b) (simp_all) |
150 by (induct b) (simp_all) |
127 |
151 |
128 lemma list_rel_len: "list_rel R a b \<Longrightarrow> length a = length b" |
152 lemma list_rel_len: "list_rel R a b \<Longrightarrow> length a = length b" |