theory Prove+
−
imports Main QuotScript QuotList+
−
uses ("quotient.ML")+
−
begin+
−
+
−
locale QUOT_TYPE =+
−
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+
−
  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"+
−
  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"+
−
  assumes equiv: "EQUIV R"+
−
  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"+
−
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"+
−
  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"+
−
  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"+
−
begin+
−
+
−
definition+
−
  "ABS x \<equiv> 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) \<equiv> 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 "\<dots> = Abs (R x)" using lem9 by simp+
−
  also have "\<dots> = Abs (Rep a)" using eq by simp+
−
  also have "\<dots> = 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) \<equiv> (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) \<equiv> (a = b)" by simp+
−
qed+
−
+
−
end+
−
+
−
use "quotient.ML"+
−
+
−
ML {*+
−
val r = ref (NONE:(unit -> term) option)+
−
*}+
−
+
−
ML {*+
−
let+
−
  fun after_qed thm_name thms lthy =+
−
       LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd+
−
    +
−
  fun setup_proof (name_spec, (txt, pos)) lthy =+
−
  let+
−
    val trm = ML_Context.evaluate lthy true ("r", r) txt+
−
  in+
−
    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy+
−
  end+
−
+
−
  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source+
−
in+
−
  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" +
−
    OuterKeyword.thy_goal (parser >> setup_proof)+
−
end+
−
*}+
−
+
−
end+
−