diff -r c3d27aada589 -r e8f352546ad8 Prove.thy --- a/Prove.thy Tue Oct 13 00:02:22 2009 +0200 +++ b/Prove.thy Tue Oct 13 09:26:19 2009 +0200 @@ -1,148 +1,7 @@ theory Prove -imports Main QuotScript QuotList -uses ("quotient.ML") -begin - -locale QUOT_TYPE = - fixes R :: "'a \ 'a \ bool" - and Abs :: "('a \ bool) \ 'b" - and Rep :: "'b \ ('a \ bool)" - assumes equiv: "EQUIV R" - and rep_prop: "\y. \x. Rep y = R x" - and rep_inverse: "\x. Abs (Rep x) = x" - and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" - and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +imports Main begin -definition - "ABS x \ Abs (R x)" - -definition - "REP a = Eps (Rep a)" - -lemma lem9: - shows "R (Eps (R x)) = R x" -proof - - have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) - then have "R x (Eps (R x))" by (rule someI) - then show "R (Eps (R x)) = R x" - using equiv unfolding EQUIV_def by simp -qed - -theorem thm10: - shows "ABS (REP a) \ a" - apply (rule eq_reflection) - unfolding ABS_def REP_def -proof - - from rep_prop - obtain x where eq: "Rep a = R x" by auto - have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp - also have "\ = Abs (R x)" using lem9 by simp - also have "\ = Abs (Rep a)" using eq by simp - also have "\ = a" using rep_inverse by simp - finally - show "Abs (R (Eps (Rep a))) = a" by simp -qed - -lemma REP_refl: - shows "R (REP a) (REP a)" -unfolding REP_def -by (simp add: equiv[simplified EQUIV_def]) - -lemma lem7: - shows "(R x = R y) = (Abs (R x) = Abs (R y))" -apply(rule iffI) -apply(simp) -apply(drule rep_inject[THEN iffD2]) -apply(simp add: abs_inverse) -done - -theorem thm11: - shows "R r r' = (ABS r = ABS r')" -unfolding ABS_def -by (simp only: equiv[simplified EQUIV_def] lem7) - - -lemma REP_ABS_rsp: - shows "R f (REP (ABS g)) = R f g" - and "R (REP (ABS g)) f = R g f" -by (simp_all add: thm10 thm11) - -lemma QUOTIENT: - "QUOTIENT R ABS REP" -apply(unfold QUOTIENT_def) -apply(simp add: thm10) -apply(simp add: REP_refl) -apply(subst thm11[symmetric]) -apply(simp add: equiv[simplified EQUIV_def]) -done - -lemma R_trans: - assumes ab: "R a b" - and bc: "R b c" - shows "R a c" -proof - - have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - moreover have ab: "R a b" by fact - moreover have bc: "R b c" by fact - ultimately show "R a c" unfolding TRANS_def by blast -qed - -lemma R_sym: - assumes ab: "R a b" - shows "R b a" -proof - - have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - then show "R b a" using ab unfolding SYM_def by blast -qed - -lemma R_trans2: - assumes ac: "R a c" - and bd: "R b d" - shows "R a b = R c d" -proof - assume "R a b" - then have "R b a" using R_sym by blast - then have "R b c" using ac R_trans by blast - then have "R c b" using R_sym by blast - then show "R c d" using bd R_trans by blast -next - assume "R c d" - then have "R a d" using ac R_trans by blast - then have "R d a" using R_sym by blast - then have "R b a" using bd R_trans by blast - then show "R a b" using R_sym by blast -qed - -lemma REPS_same: - shows "R (REP a) (REP b) \ (a = b)" -proof - - have "R (REP a) (REP b) = (a = b)" - proof - assume as: "R (REP a) (REP b)" - from rep_prop - obtain x y - where eqs: "Rep a = R x" "Rep b = R y" by blast - from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp - then have "R x (Eps (R y))" using lem9 by simp - then have "R (Eps (R y)) x" using R_sym by blast - then have "R y x" using lem9 by simp - then have "R x y" using R_sym by blast - then have "ABS x = ABS y" using thm11 by simp - then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp - then show "a = b" using rep_inverse by simp - next - assume ab: "a = b" - have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto - qed - then show "R (REP a) (REP b) \ (a = b)" by simp -qed - -end - -use "quotient.ML" - ML {* val r = ref (NONE:(unit -> term) option) *}