equal
deleted
inserted
replaced
1 theory IntEx |
1 theory IntEx |
2 imports QuotMain |
2 imports QuotMain |
3 begin |
3 begin |
4 |
|
5 |
4 |
6 fun |
5 fun |
7 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
8 where |
7 where |
9 "intrel (x, y) (u, v) = (x + v = u + y)" |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
235 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
234 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
236 apply (induct t) |
235 apply (induct t) |
237 by (simp_all add: Quotient_ABS_REP[OF a]) |
236 by (simp_all add: Quotient_ABS_REP[OF a]) |
238 |
237 |
239 lemma cons_rsp[quotient_rsp]: |
238 lemma cons_rsp[quotient_rsp]: |
240 "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #" |
239 "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #" |
241 by simp |
240 by simp |
242 |
241 |
243 (* I believe it's true. *) |
242 (* I believe it's true. *) |
244 lemma foldl_rsp[quotient_rsp]: |
243 lemma foldl_rsp[quotient_rsp]: |
245 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl" |
244 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl" |
246 apply (simp only: fun_rel.simps) |
245 apply (simp only: fun_rel.simps) |
247 apply (rule allI) |
246 apply (rule allI) |
248 apply (rule allI) |
247 apply (rule allI) |
249 apply (rule impI) |
248 apply (rule impI) |
250 apply (rule allI) |
249 apply (rule allI) |
255 apply (rule impI) |
254 apply (rule impI) |
256 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
255 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
257 sorry |
256 sorry |
258 |
257 |
259 lemma nil_listrel_rsp[quotient_rsp]: |
258 lemma nil_listrel_rsp[quotient_rsp]: |
260 "(LIST_REL R) [] []" |
259 "(list_rel R) [] []" |
261 by simp |
260 by simp |
262 |
261 |
263 lemma "foldl PLUS x [] = x" |
262 lemma "foldl PLUS x [] = x" |
264 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
263 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
265 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
264 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |