--- 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)"
*)
+
+