--- a/FSet.thy Sat Oct 24 10:16:53 2009 +0200
+++ b/FSet.thy Sat Oct 24 13:00:54 2009 +0200
@@ -278,11 +278,11 @@
let
val g = build_regularize_goal thm rty rel lthy;
val tac =
- (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
+ atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
[(@{thm equiv_res_forall} OF [rel_eqv]),
- (@{thm equiv_res_exists} OF [rel_eqv])])) THEN'
- (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'
- (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []);
+ (@{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 lthy []));
val cgoal = cterm_of (ProofContext.theory_of lthy) g;
val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1);
in
@@ -392,23 +392,31 @@
ML Goal.prove
ML {*
-fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+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;
val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
(REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
-(* val tac2 =
- (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm]))
- THEN' (rtac thm);
- val cgoal = cterm_of (ProofContext.theory_of lthy) rt;
- val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *)
+ in
+ (rt, cthm, thm)
+ end
+*}
+
+ML {*
+fun repabs_eq2 lthy (rt, thm, othm) =
+ let
+ fun tac2 ctxt =
+ (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+ THEN' (rtac othm);
+ val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
in
cthm
end
*}
+
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}
@@ -430,14 +438,6 @@
apply (tactic {* rtac thm 1 *})
done
-ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
-ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
-ML {* val ind_r_t =
- repabs @{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}
-*}
-
thm list.recs(2)
thm m2
@@ -465,21 +465,21 @@
by (simp add: id_def)
ML {*
- val t = prop_of @{thm LAMBDA_PRS}
- val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}
- val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
- val tttt = @{thm "HOL.sym"} OF [ttt]
+ val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];
+ val lpist = @{thm "HOL.sym"} OF [lpis];
+ val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist
*}
+
+text {* the proper way to do it *}
ML {*
- val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt
- val zzz = @{thm m2_t}
+ val lpi = Drule.instantiate'
+ [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS};
*}
-prove asdfasdf : {* concl_of tt *}
+prove asdfasdf : {* concl_of lpi *}
apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
done
-
thm HOL.sym[OF asdfasdf,simplified]
ML {*
@@ -496,11 +496,31 @@
Simplifier.rewrite_rule [rt] thm
end
*}
-ML ttttt
-ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *}
-ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}
-ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
-ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}
+
+(* @{thms HOL.sym[OF asdfasdf,simplified]} *)
+
+ML {*
+ fun simp_lam_prs lthy thm =
+ simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm)
+ handle _ => thm
+*}
+
+ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
+
+ML {*
+ 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 rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};
+ val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]]
+ in
+ (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
+ end
+ handle _ => thm
+*}
+
+ML {* val ithm = simp_allex_prs @{context} m2_t' *}
ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
ML {* ObjectLogic.rulify rthm *}
@@ -529,101 +549,71 @@
ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *}
ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *}
-ML {* val ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *}
-ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *}
-ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
-ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *}
-ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *}
+ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}
+ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
ML {* ObjectLogic.rulify qthm *}
-
-ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
-prove fold1_def_2_r: {*
- Logic.mk_implies
- ((prop_of li),
- (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
- apply (simp add: equiv_res_forall[OF equiv_list_eq])
- done
-
-ML {* @{thm fold1_def_2_r} OF [li] *}
+thm fold1.simps(2)
-lemma yy:
- shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
-unfolding IN_def EMPTY_def
-apply(rule_tac f="(op =) False" in arg_cong)
-apply(rule memb_rsp)
-apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply(rule list_eq.intros)
-done
-
-lemma
- shows "IN (x::nat) EMPTY = False"
-using m1
-apply -
-apply(rule yy[THEN iffD1, symmetric])
-apply(simp)
-done
-
-lemma
- shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
- ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
-unfolding IN_def INSERT_def
-apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
-apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
-apply(rule memb_rsp)
-apply(rule list_eq.intros(3))
-apply(unfold REP_fset_def ABS_fset_def)
-apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
-apply(rule list_eq_refl)
-done
-
-lemma yyy:
- shows "
- (
- (UNION EMPTY s = s) &
- ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
- ) = (
- ((ABS_fset ([] @ REP_fset s)) = s) &
- ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
- )"
- unfolding UNION_def EMPTY_def INSERT_def
- apply(rule_tac f="(op &)" in arg_cong2)
- apply(rule_tac f="(op =)" in arg_cong2)
- apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
- apply(rule append_respects_fst)
- apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
- apply(rule list_eq_refl)
- apply(simp)
- apply(rule_tac f="(op =)" in arg_cong2)
- apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
- apply(rule append_respects_fst)
- apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
- apply(rule list_eq_refl)
- apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
- apply(rule list_eq.intros(5))
- apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
- apply(rule list_eq_refl)
-done
-
-lemma
- shows "
- (UNION EMPTY s = s) &
- ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
- apply (simp add: yyy)
- apply (simp add: QUOT_TYPE_I_fset.thm10)
- done
+ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *}
+ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
+ML {*
+ val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+ val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
+*}
+(*prove rg
+apply(atomize(full))
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})*)
+ML {* val (g, thm, othm) =
+ 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}
+ )
+*}
+ML {*
+ fun tac2 ctxt =
+ (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+ THEN' (rtac othm); *}
+(* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
+*} *)
ML {*
- val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+ val ind_r_t2 =
+ Toplevel.program (fn () =>
+ repabs_eq2 @{context} (g, thm, othm)
+ )
*}
+ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *}
+ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}
+ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
ML {*
-cterm_of @{theory} (prop_of m1_novars);
-cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
+fun lift thm =
+let
+ val ind_r_a = atomize_thm thm;
+ val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
+ 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};
+ 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;
+ val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
+ val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
+in
+ ObjectLogic.rulify ind_r_s
+end
*}
+ML {* lift @{thm m2} *}
+ML {* lift @{thm m1} *}
+ML {* lift @{thm list_eq.intros(4)} *}
+ML {* lift @{thm list_eq.intros(5)} *}
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
ML {*