82 assumes a: "Quotient R1 abs1 rep1" |
82 assumes a: "Quotient R1 abs1 rep1" |
83 and b: "Quotient R2 abs2 rep2" |
83 and b: "Quotient R2 abs2 rep2" |
84 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
84 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
85 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
85 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
86 |
86 |
87 (* We need an ho version *) |
|
88 lemma map_rsp: |
87 lemma map_rsp: |
|
88 assumes q1: "Quotient R1 Abs1 Rep1" |
|
89 and q2: "Quotient R2 Abs2 Rep2" |
|
90 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
|
91 apply(simp) |
|
92 apply(rule allI)+ |
|
93 apply(rule impI) |
|
94 apply(rule allI)+ |
|
95 apply (induct_tac xa ya rule: list_induct2') |
|
96 apply simp_all |
|
97 done |
|
98 |
|
99 (* TODO: if the above is correct, we can remove this one *) |
|
100 lemma map_rsp_lo: |
89 assumes q1: "Quotient R1 Abs1 Rep1" |
101 assumes q1: "Quotient R1 Abs1 Rep1" |
90 and q2: "Quotient R2 Abs2 Rep2" |
102 and q2: "Quotient R2 Abs2 Rep2" |
91 and a: "(R1 ===> R2) f1 f2" |
103 and a: "(R1 ===> R2) f1 f2" |
92 and b: "list_rel R1 l1 l2" |
104 and b: "list_rel R1 l1 l2" |
93 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
105 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
104 assumes a: "Quotient R1 abs1 rep1" |
116 assumes a: "Quotient R1 abs1 rep1" |
105 and b: "Quotient R2 abs2 rep2" |
117 and b: "Quotient R2 abs2 rep2" |
106 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
118 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
107 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
119 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
108 |
120 |
|
121 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0" |
|
122 by (induct b) (simp_all) |
109 |
123 |
|
124 lemma list_rel_len: "list_rel R a b \<Longrightarrow> length a = length b" |
|
125 apply (induct a arbitrary: b) |
|
126 apply (simp add: list_rel_empty) |
|
127 apply (case_tac b) |
|
128 apply simp_all |
|
129 done |
110 |
130 |
|
131 (* TODO: induct_tac doesn't accept 'arbitrary'. |
|
132 induct doesn't accept 'rule'. |
|
133 that's why the proof uses manual generalisation and needs assumptions |
|
134 both in conclusion for induction and in assumptions. *) |
|
135 lemma foldl_rsp[quotient_rsp]: |
|
136 assumes q1: "Quotient R1 Abs1 Rep1" |
|
137 and q2: "Quotient R2 Abs2 Rep2" |
|
138 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
|
139 apply auto |
|
140 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
|
141 apply simp |
|
142 apply (rule_tac x="xa" in spec) |
|
143 apply (rule_tac x="ya" in spec) |
|
144 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
|
145 apply (rule list_rel_len) |
|
146 apply (simp_all) |
|
147 done |
|
148 |
|
149 (* TODO: foldr_rsp should be similar *) |
111 |
150 |
112 |
151 |
113 |
152 |
114 |
153 |
115 (* TODO: Rest are unused *) |
154 (* TODO: Rest are unused *) |