--- a/FSet.thy Sat Oct 24 08:34:14 2009 +0200
+++ b/FSet.thy Sat Oct 24 10:16:53 2009 +0200
@@ -235,6 +235,11 @@
apply (simp_all add:memb_rsp)
done
+lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
+ apply (simp add: FUN_REL.simps)
+ apply (metis card1_rsp)
+ done
+
lemma cons_rsp:
fixes z
assumes a: "xs \<approx> ys"
@@ -259,11 +264,32 @@
thm list.induct
lemma list_induct_hol4:
fixes P :: "'a list \<Rightarrow> bool"
- assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
- shows "(\<forall>l. (P l))"
- sorry
+ assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
+ shows "\<forall>l. (P l)"
+ using a
+ apply (rule_tac allI)
+ apply (induct_tac "l")
+ apply (simp)
+ apply (metis)
+ done
-ML {* atomize_thm @{thm list_induct_hol4} *}
+ML {*
+fun regularize thm rty rel rel_eqv lthy =
+ let
+ val g = build_regularize_goal thm rty rel lthy;
+ val tac =
+ (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 []);
+ val cgoal = cterm_of (ProofContext.theory_of lthy) g;
+ val cthm = Goal.prove_internal [] cgoal (fn _ => tac 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} *}
@@ -295,6 +321,14 @@
(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 =
@@ -314,9 +348,21 @@
| _ => 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 res_thms =
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
(FIRST' [
rtac @{thm FUN_QUOTIENT},
rtac quot_thm,
@@ -325,8 +371,9 @@
rtac trans_thm,
LAMBDA_RES_TAC ctxt,
res_forall_rsp_tac ctxt,
+ res_exists_rsp_tac ctxt,
(
- (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs})))
+ (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])),
@@ -337,13 +384,34 @@
(
(simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
THEN_ALL_NEW (fn _ => no_tac)
- )
+ ),
+ WEAK_LAMBDA_RES_TAC ctxt
])
*}
+ML Goal.prove
+
+ML {*
+fun repabs 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
+ 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}
+ 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}
*}
@@ -354,14 +422,6 @@
ML {* trm_r *}
prove list_induct_tr: trm_r
apply (atomize(full))
-(* APPLY_RSP_TAC *)
-ML_prf {* val ctxt = @{context} *}
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* LAMBDA_RES_TAC *)
-apply (subst FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
done
@@ -370,9 +430,16 @@
apply (tactic {* rtac thm 1 *})
done
-ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}
+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
ML {* atomize_thm @{thm m2} *}
@@ -397,10 +464,9 @@
lemma id_apply2 [simp]: "id x \<equiv> x"
by (simp add: id_def)
-thm LAMBDA_PRS
ML {*
val t = prop_of @{thm LAMBDA_PRS}
- val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{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]
*}
@@ -408,6 +474,13 @@
val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt
val zzz = @{thm m2_t}
*}
+prove asdfasdf : {* concl_of tt *}
+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 {*
fun eqsubst_thm ctxt thms thm =
@@ -423,9 +496,10 @@
Simplifier.rewrite_rule [rt] thm
end
*}
-ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *}
+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 [ObjectLogic.rulify rwr] *}
+ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}
ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
ML {* ObjectLogic.rulify rthm *}
@@ -433,14 +507,36 @@
ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
-prove card1_suc_r: {*
- Logic.mk_implies
- ((prop_of card1_suc_f),
- (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+prove card1_suc_r_p: {*
+ build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
- done
+done
+
+ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *}
+ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *}
+prove card1_suc_t_p: card1_suc_t_g
+apply (atomize(full))
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+done
-ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
+prove card1_suc_t: card1_suc_t
+apply (simp only: card1_suc_t_p[symmetric])
+apply (tactic {* rtac card1_suc_r 1 *})
+done
+
+
+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 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: {*
@@ -635,7 +731,6 @@
*}
ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
-
ML {*
fun lift_theorem_fset name thm lthy =
let