# HG changeset patch # User Cezary Kaliszyk # Date 1256393758 -7200 # Node ID f7602653dddd8ca6014ac76459befa6cfa26a83d # Parent 7cf227756e2a2fdc2982db715c241f65e0968f51 Preparing infrastructire for LAMBDA_PRS diff -r 7cf227756e2a -r f7602653dddd FSet.thy --- a/FSet.thy Sat Oct 24 14:00:18 2009 +0200 +++ b/FSet.thy Sat Oct 24 16:15:58 2009 +0200 @@ -252,15 +252,22 @@ apply (metis cons_rsp) done -lemma append_respects_fst: +lemma append_rsp_fst: assumes a : "list_eq l1 l2" shows "list_eq (l1 @ s) (l2 @ s)" using a apply(induct) apply(auto intro: list_eq.intros) - apply(simp add: list_eq_refl) + apply(rule list_eq_refl) done +lemma "(a @ b) \ (b @ a)" +sorry + +lemma (* ho_append_rsp: *) + "op \ ===> op \ ===> op \ op @ op @" +sorry + thm list.induct lemma list_induct_hol4: fixes P :: "'a list \ bool" @@ -281,8 +288,8 @@ (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])) ORELSE' - (MetisTools.metis_tac ctxt [])); + (((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] @@ -388,8 +395,6 @@ ]) *} -ML Goal.prove - ML {* fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = let @@ -469,15 +474,41 @@ text {* the proper way to do it *} ML {* + fun findabs rty tm = + case tm of + Abs(_, T, b) => + let + val b' = subst_bound ((Free ("x", T)), b); + val tys = findabs rty b' + val ty = fastype_of tm + in if needs_lift rty ty then (ty :: tys) else tys + end + | f $ a => (findabs rty f) @ (findabs rty a) + | _ => [] +*} + +ML {* findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} + +ML {* val lpi = Drule.instantiate' - [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}; + [SOME @{ctyp "'a list"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; *} -prove asdfasdf : {* concl_of lpi *} +prove lambda_prs_l_b : {* 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] +thm HOL.sym[OF lambda_prs_l_b,simplified] +ML {* + val lpi = Drule.instantiate' + [SOME @{ctyp "'a list \ bool"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; +*} +prove lambda_prs_lb_b : {* 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 lambda_prs_lb_b,simplified] ML {* fun eqsubst_thm ctxt thms thm = @@ -494,11 +525,12 @@ end *} -(* @{thms HOL.sym[OF asdfasdf,simplified]} *) ML {* - fun simp_lam_prs lthy thm = - simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm) + fun simp_lam_prs lthy thm = + simp_lam_prs lthy (eqsubst_thm lthy + @{thms HOL.sym[OF lambda_prs_lb_b,simplified] HOL.sym[OF lambda_prs_l_b,simplified]} + thm) handle _ => thm *} @@ -544,8 +576,8 @@ 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 card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *} +ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *} 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 *} @@ -554,10 +586,15 @@ thm fold1.simps(2) thm list.recs(2) -ML {* val ind_r_a = atomize_thm @{thm m2} *} - (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} - apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *) - +ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} +(* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} + ML_prf {* fun tac ctxt = + (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps + [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), + (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) 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 [])); *} + apply (tactic {* tac @{context} 1 *}) *) ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \"} @{thm equiv_list_eq} @{context} *} ML {* val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @@ -590,6 +627,9 @@ 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 *} +lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" + apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) +done ML {* fun lift thm = @@ -614,7 +654,8 @@ ML {* lift @{thm m1} *} ML {* lift @{thm list_eq.intros(4)} *} ML {* lift @{thm list_eq.intros(5)} *} -(* ML {* lift @{thm length_append} *} *) +ML {* lift @{thm card1_suc} *} +(* ML {* lift @{thm append_assoc} *} *) (*notation ( output) "prop" ("#_" [1000] 1000) *) notation ( output) "Trueprop" ("#_" [1000] 1000)