10 | "list_rel R [] (x#xs) = False" |
10 | "list_rel R [] (x#xs) = False" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
12 |
12 |
13 declare [[map list = (map, list_rel)]] |
13 declare [[map list = (map, list_rel)]] |
14 |
14 |
15 lemma list_equivp[quotient_equiv]: |
15 lemma list_equivp[quot_equiv]: |
16 assumes a: "equivp R" |
16 assumes a: "equivp R" |
17 shows "equivp (list_rel R)" |
17 shows "equivp (list_rel R)" |
18 unfolding equivp_def |
18 unfolding equivp_def |
19 apply(rule allI)+ |
19 apply(rule allI)+ |
20 apply(induct_tac x y rule: list_induct2') |
20 apply(induct_tac x y rule: list_induct2') |
38 apply(simp_all) |
38 apply(simp_all) |
39 using Quotient_rel[OF q] |
39 using Quotient_rel[OF q] |
40 apply(metis) |
40 apply(metis) |
41 done |
41 done |
42 |
42 |
43 lemma list_quotient[quotient_thm]: |
43 lemma list_quotient[quot_thm]: |
44 assumes q: "Quotient R Abs Rep" |
44 assumes q: "Quotient R Abs Rep" |
45 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
45 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
46 unfolding Quotient_def |
46 unfolding Quotient_def |
47 apply(rule conjI) |
47 apply(rule conjI) |
48 apply(rule allI) |
48 apply(rule allI) |
70 lemma cons_prs: |
70 lemma cons_prs: |
71 assumes q: "Quotient R Abs Rep" |
71 assumes q: "Quotient R Abs Rep" |
72 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
72 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
73 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
73 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
74 |
74 |
75 lemma cons_rsp[quotient_rsp]: |
75 lemma cons_rsp[quot_respect]: |
76 assumes q: "Quotient R Abs Rep" |
76 assumes q: "Quotient R Abs Rep" |
77 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
77 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
78 by (auto) |
78 by (auto) |
79 |
79 |
80 lemma nil_prs: |
80 lemma nil_prs: |
81 assumes q: "Quotient R Abs Rep" |
81 assumes q: "Quotient R Abs Rep" |
82 shows "map Abs [] \<equiv> []" |
82 shows "map Abs [] \<equiv> []" |
83 by (simp) |
83 by (simp) |
84 |
84 |
85 lemma nil_rsp[quotient_rsp]: |
85 lemma nil_rsp[quot_respect]: |
86 assumes q: "Quotient R Abs Rep" |
86 assumes q: "Quotient R Abs Rep" |
87 shows "list_rel R [] []" |
87 shows "list_rel R [] []" |
88 by simp |
88 by simp |
89 |
89 |
90 lemma map_prs: |
90 lemma map_prs: |
91 assumes a: "Quotient R1 abs1 rep1" |
91 assumes a: "Quotient R1 abs1 rep1" |
92 and b: "Quotient R2 abs2 rep2" |
92 and b: "Quotient R2 abs2 rep2" |
93 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
93 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
94 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
94 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
95 |
95 |
96 lemma map_rsp[quotient_rsp]: |
96 lemma map_rsp[quot_respect]: |
97 assumes q1: "Quotient R1 Abs1 Rep1" |
97 assumes q1: "Quotient R1 Abs1 Rep1" |
98 and q2: "Quotient R2 Abs2 Rep2" |
98 and q2: "Quotient R2 Abs2 Rep2" |
99 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
99 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
100 apply(simp) |
100 apply(simp) |
101 apply(rule allI)+ |
101 apply(rule allI)+ |
129 |
129 |
130 (* TODO: induct_tac doesn't accept 'arbitrary'. |
130 (* TODO: induct_tac doesn't accept 'arbitrary'. |
131 induct doesn't accept 'rule'. |
131 induct doesn't accept 'rule'. |
132 that's why the proof uses manual generalisation and needs assumptions |
132 that's why the proof uses manual generalisation and needs assumptions |
133 both in conclusion for induction and in assumptions. *) |
133 both in conclusion for induction and in assumptions. *) |
134 lemma foldl_rsp[quotient_rsp]: |
134 lemma foldl_rsp[quot_respect]: |
135 assumes q1: "Quotient R1 Abs1 Rep1" |
135 assumes q1: "Quotient R1 Abs1 Rep1" |
136 and q2: "Quotient R2 Abs2 Rep2" |
136 and q2: "Quotient R2 Abs2 Rep2" |
137 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
137 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
138 apply auto |
138 apply auto |
139 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
139 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |