equal
deleted
inserted
replaced
1 (* Title: QuotMain.thy |
1 (* Title: QuotMain.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 theory QuotMain |
5 theory QuotMain |
6 imports QuotScript Prove |
6 imports QuotBase |
7 uses ("quotient_info.ML") |
7 uses ("quotient_info.ML") |
8 ("quotient_typ.ML") |
8 ("quotient_typ.ML") |
9 ("quotient_def.ML") |
9 ("quotient_def.ML") |
10 ("quotient_term.ML") |
10 ("quotient_term.ML") |
11 ("quotient_tacs.ML") |
11 ("quotient_tacs.ML") |
59 also have "\<dots> = a" using rep_inverse by simp |
59 also have "\<dots> = a" using rep_inverse by simp |
60 finally |
60 finally |
61 show "Abs (R (Eps (Rep a))) = a" by simp |
61 show "Abs (R (Eps (Rep a))) = a" by simp |
62 qed |
62 qed |
63 |
63 |
64 lemma rep_refl: |
|
65 shows "R (rep a) (rep a)" |
|
66 unfolding rep_def |
|
67 by (simp add: equivp[simplified equivp_def]) |
|
68 |
|
69 lemma lem7: |
64 lemma lem7: |
70 shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") |
65 shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") |
71 proof - |
66 proof - |
72 have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) |
67 have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) |
73 also have "\<dots> = ?LHS" by (simp add: abs_inverse) |
68 also have "\<dots> = ?LHS" by (simp add: abs_inverse) |
76 |
71 |
77 theorem thm11: |
72 theorem thm11: |
78 shows "R r r' = (abs r = abs r')" |
73 shows "R r r' = (abs r = abs r')" |
79 unfolding abs_def |
74 unfolding abs_def |
80 by (simp only: equivp[simplified equivp_def] lem7) |
75 by (simp only: equivp[simplified equivp_def] lem7) |
|
76 |
|
77 lemma rep_refl: |
|
78 shows "R (rep a) (rep a)" |
|
79 unfolding rep_def |
|
80 by (simp add: equivp[simplified equivp_def]) |
|
81 |
81 |
82 |
82 lemma rep_abs_rsp: |
83 lemma rep_abs_rsp: |
83 shows "R f (rep (abs g)) = R f g" |
84 shows "R f (rep (abs g)) = R f g" |
84 and "R (rep (abs g)) f = R g f" |
85 and "R (rep (abs g)) f = R g f" |
85 by (simp_all add: thm10 thm11) |
86 by (simp_all add: thm10 thm11) |