60 shows "R (rep a) (rep a)" |
65 shows "R (rep a) (rep a)" |
61 unfolding rep_def |
66 unfolding rep_def |
62 by (simp add: equivp[simplified equivp_def]) |
67 by (simp add: equivp[simplified equivp_def]) |
63 |
68 |
64 lemma lem7: |
69 lemma lem7: |
65 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
70 shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") |
66 apply(rule iffI) |
71 proof - |
67 apply(simp) |
72 have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) |
68 apply(drule rep_inject[THEN iffD2]) |
73 also have "\<dots> = ?LHS" by (simp add: abs_inverse) |
69 apply(simp add: abs_inverse) |
74 finally show "?LHS = ?RHS" by simp |
70 done |
75 qed |
71 |
76 |
72 theorem thm11: |
77 theorem thm11: |
73 shows "R r r' = (abs r = abs r')" |
78 shows "R r r' = (abs r = abs r')" |
74 unfolding abs_def |
79 unfolding abs_def |
75 by (simp only: equivp[simplified equivp_def] lem7) |
80 by (simp only: equivp[simplified equivp_def] lem7) |
79 and "R (rep (abs g)) f = R g f" |
84 and "R (rep (abs g)) f = R g f" |
80 by (simp_all add: thm10 thm11) |
85 by (simp_all add: thm10 thm11) |
81 |
86 |
82 lemma Quotient: |
87 lemma Quotient: |
83 shows "Quotient R abs rep" |
88 shows "Quotient R abs rep" |
84 apply(unfold Quotient_def) |
89 unfolding Quotient_def |
85 apply(simp add: thm10) |
90 apply(simp add: thm10) |
86 apply(simp add: rep_refl) |
91 apply(simp add: rep_refl) |
87 apply(subst thm11[symmetric]) |
92 apply(subst thm11[symmetric]) |
88 apply(simp add: equivp[simplified equivp_def]) |
93 apply(simp add: equivp[simplified equivp_def]) |
89 done |
94 done |
90 |
95 |
91 end |
96 end |
92 |
97 |
93 term Quot_Type.abs |
|
94 |
|
95 section {* ML setup *} |
98 section {* ML setup *} |
96 |
99 |
97 (* Auxiliary data for the quotient package *) |
100 text {* Auxiliary data for the quotient package *} |
98 |
101 |
99 use "quotient_info.ML" |
102 use "quotient_info.ML" |
100 |
103 |
101 declare [[map "fun" = (fun_map, fun_rel)]] |
104 declare [[map "fun" = (fun_map, fun_rel)]] |
102 |
105 |
103 lemmas [quot_thm] = fun_quotient |
106 lemmas [quot_thm] = fun_quotient |
104 lemmas [quot_respect] = quot_rel_rsp |
107 lemmas [quot_respect] = quot_rel_rsp |
105 lemmas [quot_equiv] = identity_equivp |
108 lemmas [quot_equiv] = identity_equivp |
106 |
109 |
107 (* Lemmas about simplifying id's. *) |
110 |
|
111 text {* Lemmas about simplifying id's. *} |
108 lemmas [id_simps] = |
112 lemmas [id_simps] = |
|
113 id_def[symmetric, THEN eq_reflection] |
109 fun_map_id[THEN eq_reflection] |
114 fun_map_id[THEN eq_reflection] |
110 id_apply[THEN eq_reflection] |
115 id_apply[THEN eq_reflection] |
111 id_o[THEN eq_reflection] |
116 id_o[THEN eq_reflection] |
112 id_def[symmetric, THEN eq_reflection] |
|
113 o_id[THEN eq_reflection] |
117 o_id[THEN eq_reflection] |
114 eq_comp_r |
118 eq_comp_r |
115 |
119 |
116 (* The translation functions for the lifting process. *) |
120 text {* Translation functions for the lifting process. *} |
117 use "quotient_term.ML" |
121 use "quotient_term.ML" |
118 |
122 |
119 |
123 |
120 (* Definition of the quotient types *) |
124 text {* Definitions of the quotient types. *} |
121 use "quotient_typ.ML" |
125 use "quotient_typ.ML" |
122 |
126 |
123 |
127 |
124 (* Definitions for quotient constants *) |
128 text {* Definitions for quotient constants. *} |
125 use "quotient_def.ML" |
129 use "quotient_def.ML" |
126 |
130 |
127 (* Tactics for proving the lifted theorems *) |
|
128 |
131 |
129 lemma eq_imp_rel: |
132 text {* |
130 "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
133 An auxiliar constant for recording some information |
131 by (simp add: equivp_reflp) |
134 about the lifted theorem in a tactic. |
132 |
135 *} |
133 (* An auxiliar constant for recording some information *) |
|
134 (* about the lifted theorem in a tactic. *) |
|
135 definition |
136 definition |
136 "Quot_True x \<equiv> True" |
137 "Quot_True x \<equiv> True" |
137 |
138 |
138 lemma |
139 lemma |
139 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
140 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |