equal
deleted
inserted
replaced
50 apply(rule conjI) |
50 apply(rule conjI) |
51 apply(rule allI) |
51 apply(rule allI) |
52 apply(induct_tac a) |
52 apply(induct_tac a) |
53 apply(simp) |
53 apply(simp) |
54 apply(simp) |
54 apply(simp) |
55 apply(simp add: Quotient_REP_reflp[OF q]) |
55 apply(simp add: Quotient_rep_reflp[OF q]) |
56 apply(rule allI)+ |
56 apply(rule allI)+ |
57 apply(rule list_rel_rel[OF q]) |
57 apply(rule list_rel_rel[OF q]) |
58 done |
58 done |
59 |
59 |
60 |
60 |
112 |
112 |
113 |
113 |
114 |
114 |
115 (* TODO: Rest are unused *) |
115 (* TODO: Rest are unused *) |
116 |
116 |
117 lemma LIST_map_id: |
117 lemma list_map_id: |
118 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
118 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
119 by simp |
119 by simp |
120 |
120 |
121 lemma list_rel_EQ: |
121 lemma list_rel_eq: |
122 shows "list_rel (op =) \<equiv> (op =)" |
122 shows "list_rel (op =) \<equiv> (op =)" |
123 apply(rule eq_reflection) |
123 apply(rule eq_reflection) |
124 unfolding expand_fun_eq |
124 unfolding expand_fun_eq |
125 apply(rule allI)+ |
125 apply(rule allI)+ |
126 apply(induct_tac x xa rule: list_induct2') |
126 apply(induct_tac x xa rule: list_induct2') |
127 apply(simp_all) |
127 apply(simp_all) |
128 done |
128 done |
129 |
129 |
130 lemma list_rel_REFL: |
130 lemma list_rel_refl: |
131 assumes a: "\<And>x y. R x y = (R x = R y)" |
131 assumes a: "\<And>x y. R x y = (R x = R y)" |
132 shows "list_rel R x x" |
132 shows "list_rel R x x" |
133 by (induct x) (auto simp add: a) |
133 by (induct x) (auto simp add: a) |
134 |
134 |
135 |
|
136 end |
135 end |