Cleaning and fixing.
--- a/FSet.thy Mon Oct 26 02:06:01 2009 +0100
+++ b/FSet.thy Mon Oct 26 10:02:50 2009 +0100
@@ -218,8 +218,10 @@
apply(rule list_eq_refl)
done
+(* Need stronger induction... *)
lemma "(a @ b) \<approx> (b @ a)"
-sorry
+ apply(induct a)
+ sorry
lemma (* ho_append_rsp: *)
"op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
@@ -237,23 +239,6 @@
apply (metis)
done
-ML {*
-fun regularize thm rty rel rel_eqv lthy =
- let
- val g = build_regularize_goal thm rty rel lthy;
- fun tac ctxt =
- (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
- [(@{thm equiv_res_forall} OF [rel_eqv]),
- (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
- (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
- (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
- val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
- in
- cthm OF [thm]
- end
-*}
-
-
prove list_induct_r: {*
build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
apply (simp only: equiv_res_forall[OF equiv_list_eq])
@@ -265,94 +250,6 @@
done
ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
-let
- val pat = Drule.strip_imp_concl (cprop_of thm)
- val insts = Thm.match (pat, concl)
-in
- rtac (Drule.instantiate insts thm) 1
-end
-handle _ => no_tac
-)
-*}
-
-ML {*
-fun res_forall_rsp_tac ctxt =
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
- THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
- THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-ML {*
-fun res_exists_rsp_tac ctxt =
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
- THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
- THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-
-ML {*
-fun quotient_tac quot_thm =
- REPEAT_ALL_NEW (FIRST' [
- rtac @{thm FUN_QUOTIENT},
- rtac quot_thm,
- rtac @{thm IDENTITY_QUOTIENT}
- ])
-*}
-
-ML {*
-fun LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | _ => fn _ => no_tac) i st
-*}
-
-ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ _$(Abs(_,_,_)))) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | (_ $ (_ $ (Abs(_,_,_))$_)) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | _ => fn _ => no_tac) i st
-*}
-
-
-ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
- (FIRST' [
- rtac @{thm FUN_QUOTIENT},
- rtac quot_thm,
- rtac @{thm IDENTITY_QUOTIENT},
- rtac @{thm ext},
- rtac trans_thm,
- LAMBDA_RES_TAC ctxt,
- res_forall_rsp_tac ctxt,
- res_exists_rsp_tac ctxt,
- (
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs})))
- THEN_ALL_NEW (fn _ => no_tac)
- ),
- (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
- rtac refl,
- (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
- rtac reflex_thm,
- atac,
- (
- (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
- THEN_ALL_NEW (fn _ => no_tac)
- ),
- WEAK_LAMBDA_RES_TAC ctxt
- ])
-*}
-
-ML {*
fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
let
val rt = build_repabs_term lthy thm constructors rty qty;
@@ -377,10 +274,11 @@
end
*}
-
+(* The all_prs and ex_prs should be proved for the instance... *)
ML {*
fun r_mk_comb_tac_fset ctxt =
- r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
+ r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+ (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs})
*}
@@ -467,20 +365,7 @@
done
thm HOL.sym[OF lambda_prs_lb_b,simplified]
-ML {*
-fun eqsubst_thm ctxt thms thm =
- let
- val goalstate = Goal.init (Thm.cprop_of thm)
- val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
- NONE => error "eqsubst_thm"
- | SOME th => cprem_of th 1
- val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
- val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
- val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
- in
- Simplifier.rewrite_rule [rt] thm
- end
-*}
+
ML {*
@@ -497,9 +382,9 @@
fun simp_allex_prs lthy thm =
let
val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};
- val rwfs = @{thm "HOL.sym"} OF [spec OF [rwf]];
+ val rwfs = @{thm "HOL.sym"} OF [rwf];
val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};
- val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]]
+ val rwes = @{thm "HOL.sym"} OF [rwe]
in
(simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
end
@@ -564,7 +449,7 @@
Toplevel.program (fn () =>
repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
- @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
+ (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs})
)
*}
ML {*
@@ -592,6 +477,7 @@
ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
+
ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
ML {* ObjectLogic.rulify ind_r_s *}
@@ -604,7 +490,7 @@
val (g, t, ot) =
repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
- @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp};
+ (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs});
val ind_r_t = repabs_eq2 @{context} (g, t, ot);
val ind_r_l = simp_lam_prs @{context} ind_r_t;
val ind_r_a = simp_allex_prs @{context} ind_r_l;
@@ -614,6 +500,8 @@
ObjectLogic.rulify ind_r_s
end
*}
+ML fset_defs
+
ML {* lift @{thm m2} *}
ML {* lift @{thm m1} *}
--- a/QuotMain.thy Mon Oct 26 02:06:01 2009 +0100
+++ b/QuotMain.thy Mon Oct 26 10:02:50 2009 +0100
@@ -547,6 +547,22 @@
(regularise (prop_of thm) rty rel lthy))
*}
+ML {*
+fun regularize thm rty rel rel_eqv lthy =
+ let
+ val g = build_regularize_goal thm rty rel lthy;
+ fun tac ctxt =
+ (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+ [(@{thm equiv_res_forall} OF [rel_eqv]),
+ (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
+ (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+ (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
+ val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
+ in
+ cthm OF [thm]
+ end
+*}
+
section {* RepAbs injection *}
(* Needed to have a meta-equality *)
@@ -616,4 +632,110 @@
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
*}
+ML {*
+fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+let
+ val pat = Drule.strip_imp_concl (cprop_of thm)
+ val insts = Thm.match (pat, concl)
+in
+ rtac (Drule.instantiate insts thm) 1
end
+handle _ => no_tac
+)
+*}
+
+ML {*
+fun res_forall_rsp_tac ctxt =
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+ THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
+ML {*
+fun res_exists_rsp_tac ctxt =
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+ THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+ THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
+
+ML {*
+fun quotient_tac quot_thm =
+ REPEAT_ALL_NEW (FIRST' [
+ rtac @{thm FUN_QUOTIENT},
+ rtac quot_thm,
+ rtac @{thm IDENTITY_QUOTIENT}
+ ])
+*}
+
+ML {*
+fun LAMBDA_RES_TAC ctxt i st =
+ (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+ (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ | _ => fn _ => no_tac) i st
+*}
+
+ML {*
+fun WEAK_LAMBDA_RES_TAC ctxt i st =
+ (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ (_ $ (_ $ _$(Abs(_,_,_)))) =>
+ (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ | (_ $ (_ $ (Abs(_,_,_))$_)) =>
+ (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ | _ => fn _ => no_tac) i st
+*}
+
+
+ML {*
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
+ (FIRST' [
+ rtac @{thm FUN_QUOTIENT},
+ rtac quot_thm,
+ rtac @{thm IDENTITY_QUOTIENT},
+ rtac @{thm ext},
+ rtac trans_thm,
+ LAMBDA_RES_TAC ctxt,
+ res_forall_rsp_tac ctxt,
+ res_exists_rsp_tac ctxt,
+ (
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
+ THEN_ALL_NEW (fn _ => no_tac)
+ ),
+ (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+ rtac refl,
+ (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+ rtac reflex_thm,
+ atac,
+ (
+ (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+ THEN_ALL_NEW (fn _ => no_tac)
+ ),
+ WEAK_LAMBDA_RES_TAC ctxt
+ ])
+*}
+
+section {* Cleaning the goal *}
+
+text {* Does the same as 'subst' in a given theorem *}
+ML {*
+fun eqsubst_thm ctxt thms thm =
+ let
+ val goalstate = Goal.init (Thm.cprop_of thm)
+ val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ NONE => error "eqsubst_thm"
+ | SOME th => cprem_of th 1
+ val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+ val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+ val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+ in
+ Simplifier.rewrite_rule [rt] thm
+ end
+*}
+
+end
--- a/QuotScript.thy Mon Oct 26 02:06:01 2009 +0100
+++ b/QuotScript.thy Mon Oct 26 10:02:50 2009 +0100
@@ -495,9 +495,6 @@
|- !R abs rep.
QUOTIENT R abs rep ==>
!f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f),
- |- !R abs rep.
- QUOTIENT R abs rep ==>
- !a b c. (if a then b else c) = abs (if a then rep b else rep c)] :
*)
lemma FORALL_PRS:
assumes a: "QUOTIENT R absf repf"
@@ -512,8 +509,16 @@
using a
unfolding QUOTIENT_def
by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-
-lemma ho_all_prs:
+
+lemma COND_PRS:
+ assumes a: "QUOTIENT R absf repf"
+ shows "(if a then b else c) = absf (if a then repf b else repf c)"
+ using a
+ unfolding QUOTIENT_def
+ sorry
+
+(* These are the fixed versions, general ones need to be proved. *)
+lemma ho_all_prs:
shows "op = ===> op = ===> op = All All"
by auto