diff -r 2374d50fc6dd -r c0c41fefeb06 Prove.thy --- a/Prove.thy Mon Oct 12 22:44:16 2009 +0200 +++ b/Prove.thy Mon Oct 12 23:06:14 2009 +0200 @@ -1,7 +1,148 @@ theory Prove -imports Main +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)" 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) *}