equal
deleted
inserted
replaced
64 apply (rule ext) |
64 apply (rule ext) |
65 apply (rule_tac list="x" in list.induct) |
65 apply (rule_tac list="x" in list.induct) |
66 apply (simp_all) |
66 apply (simp_all) |
67 done |
67 done |
68 |
68 |
69 |
69 lemma cons_prs_aux: |
70 lemma cons_prs: |
|
71 assumes q: "Quotient R Abs Rep" |
70 assumes q: "Quotient R Abs Rep" |
72 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
71 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
73 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
72 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
|
73 |
|
74 lemma cons_prs[quot_preserve]: |
|
75 assumes q: "Quotient R Abs Rep" |
|
76 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
|
77 by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q]) |
|
78 (simp) |
74 |
79 |
75 lemma cons_rsp[quot_respect]: |
80 lemma cons_rsp[quot_respect]: |
76 assumes q: "Quotient R Abs Rep" |
81 assumes q: "Quotient R Abs Rep" |
77 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
82 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
78 by (auto) |
83 by (auto) |
79 |
84 |
80 lemma nil_prs: |
85 lemma nil_prs[quot_preserve]: |
81 assumes q: "Quotient R Abs Rep" |
86 assumes q: "Quotient R Abs Rep" |
82 shows "map Abs [] \<equiv> []" |
87 shows "map Abs [] \<equiv> []" |
83 by (simp) |
88 by (simp) |
84 |
89 |
85 lemma nil_rsp[quot_respect]: |
90 lemma nil_rsp[quot_respect]: |