68 finally show "?LHS = ?RHS" by simp |
68 finally show "?LHS = ?RHS" by simp |
69 qed |
69 qed |
70 |
70 |
71 theorem thm11: |
71 theorem thm11: |
72 shows "R r r' = (abs r = abs r')" |
72 shows "R r r' = (abs r = abs r')" |
73 unfolding abs_def |
73 unfolding abs_def |
74 by (simp only: equivp[simplified equivp_def] lem7) |
74 by (simp only: equivp[simplified equivp_def] lem7) |
75 |
75 |
76 lemma rep_refl: |
76 lemma rep_refl: |
77 shows "R (rep a) (rep a)" |
77 shows "R (rep a) (rep a)" |
78 unfolding rep_def |
78 unfolding rep_def |
79 by (simp add: equivp[simplified equivp_def]) |
79 by (simp add: equivp[simplified equivp_def]) |
80 |
80 |
81 |
81 |
82 lemma rep_abs_rsp: |
82 lemma rep_abs_rsp: |
83 shows "R f (rep (abs g)) = R f g" |
83 shows "R f (rep (abs g)) = R f g" |
84 and "R (rep (abs g)) f = R g f" |
84 and "R (rep (abs g)) f = R g f" |
85 by (simp_all add: thm10 thm11) |
85 by (simp_all add: thm10 thm11) |
86 |
86 |
87 lemma Quotient: |
87 lemma Quotient: |
88 shows "Quotient R abs rep" |
88 shows "Quotient R abs rep" |
89 unfolding Quotient_def |
89 unfolding Quotient_def |
90 apply(simp add: thm10) |
90 apply(simp add: thm10) |
91 apply(simp add: rep_refl) |
91 apply(simp add: rep_refl) |
92 apply(subst thm11[symmetric]) |
92 apply(subst thm11[symmetric]) |
93 apply(simp add: equivp[simplified equivp_def]) |
93 apply(simp add: equivp[simplified equivp_def]) |
94 done |
94 done |
95 |
95 |
96 end |
96 end |
97 |
97 |
98 section {* ML setup *} |
98 section {* ML setup *} |
99 |
99 |
140 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
140 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
141 and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" |
141 and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" |
142 and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" |
142 and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" |
143 and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" |
143 and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" |
144 and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" |
144 and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" |
145 by (simp_all add: Quot_True_def ext) |
145 by (simp_all add: Quot_True_def ext) |
146 |
146 |
147 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
147 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
148 by (simp add: Quot_True_def) |
148 by (simp add: Quot_True_def) |
149 |
149 |
150 text {* Tactics for proving the lifted theorems *} |
150 text {* Tactics for proving the lifted theorems *} |
151 use "quotient_tacs.ML" |
151 use "quotient_tacs.ML" |
152 |
152 |
153 section {* Methods / Interface *} |
153 section {* Methods / Interface *} |