diff -r ccc220a23887 -r d15121412caa QuotMain.thy
--- a/QuotMain.thy	Fri Sep 18 13:44:06 2009 +0200
+++ b/QuotMain.thy	Fri Sep 18 17:30:33 2009 +0200
@@ -79,6 +79,62 @@
 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 ?thesis 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 ?thesis 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 ab: "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 ccd: "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
+  assume as: "R (REP a) (REP b)"
+  from rep_prop
+  obtain x where eq: "Rep a = R x" by auto
+  also 
+  from rep_prop
+  obtain y where eq2: "Rep b = R y" by auto
+  then have "R (Eps (R x)) (Eps (R y))" using as eq 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 eq eq2 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
+
 end
 
 section {* type definition for the quotient type *}
@@ -301,6 +357,8 @@
 (* Test interpretation *)
 thm QUOT_TYPE_I_qtrm.thm11
 
+print_theorems
+
 thm Rep_qtrm
 
 text {* another test *}
@@ -745,12 +803,8 @@
 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
-
-notation ( output) "prop" ("#_" [1000] 1000)
-
-ML {* @{thm arg_cong2} *}
-ML {* rtac *}
-ML {* Term.dest_Const @{term "op ="} *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *}
+ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
 
 ML {*
   fun dest_cbinop t =
@@ -792,8 +846,6 @@
     end
 *}
 
-ML ORELSE
-
 ML {*
   fun foo_tac n thm =
     let
@@ -827,12 +879,12 @@
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' 1 *})
-  unfolding IN_def EMPTY_def
   apply (tactic {* foo_tac' 1 *})
   apply (tactic {* foo_tac' 1 *})
   apply (tactic {* foo_tac' 1 *})
@@ -845,39 +897,90 @@
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 2 *})
-apply (tactic {* foo_tac' 2 *})
-apply (tactic {* foo_tac' 2 *})
-unfolding CARD_def UNION_def
-apply (tactic {* foo_tac' 1 *}) *)
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 2 *})
+  apply (tactic {* foo_tac' 2 *})
+  apply (tactic {* foo_tac' 2 *})
+  apply (tactic {* foo_tac' 1 *}) *)
 
 thm m2
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-apply (tactic {* foo_tac' 1 *})
-unfolding IN_def INSERT_def
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-apply (tactic {* foo_tac' 1 *})
-done
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  done
+
+thm list_eq.intros(4)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+    (* Why doesn't this work? *)
+  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10 QUOT_TYPE_I_fset.REPS_same} cgoal2)
+*}
+thm QUOT_TYPE_I_fset.thm10
+thm QUOT_TYPE_I_fset.REPS_same
+
+(* keep it commented out, until we get a proving mechanism *)
+(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}*)
+lemma zzz : 
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> 
+    REP_fset (INSERT a (ABS_fset xs))) =  (a # a # xs \<approx> a # xs)"
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
+(*  apply (simp only: QUOT_TYPE_I_fset.thm10)*)
+  apply (rule QUOT_TYPE_I_fset.R_trans2)
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  done
+
+thm list_eq.intros(5)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
+  apply (rule QUOT_TYPE_I_fset.R_trans2)
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  done
 
 (*
 datatype obj1 =
@@ -886,3 +989,5 @@
 | INVOKE1 "obj1 \<Rightarrow> string"
 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 *)
+
+