# HG changeset patch # User Cezary Kaliszyk # Date 1256746641 -3600 # Node ID 2a28e7ef3048eb39f6744dc5750917617e864dae # Parent 9b8e039ae960a7c380a6dbd94c883b91cca9550a cleaned FSet diff -r 9b8e039ae960 -r 2a28e7ef3048 FSet.thy --- a/FSet.thy Wed Oct 28 16:48:57 2009 +0100 +++ b/FSet.thy Wed Oct 28 17:17:21 2009 +0100 @@ -167,18 +167,6 @@ term fmap thm fmap_def -ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} -(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) - -ML {* - val consts = [@{const_name "Nil"}, @{const_name "Cons"}, - @{const_name "membship"}, @{const_name "card1"}, - @{const_name "append"}, @{const_name "fold1"}, - @{const_name "map"}]; -*} - -ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} - lemma memb_rsp: fixes z assumes a: "list_eq x y" @@ -293,136 +281,43 @@ ((map f a) ::'a list) @ (map f b)" by simp (rule list_eq_refl) -thm list.induct -lemma list_induct_hol4: - fixes P :: "'a list \ bool" - assumes a: "((P []) \ (\t. (P t) \ (\h. (P (h # t)))))" - shows "\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 {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \"} @{context} *} - -prove list_induct_r: {* - build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \"} @{context} *} - apply (simp only: equiv_res_forall[OF equiv_list_eq]) - thm RIGHT_RES_FORALL_REGULAR - apply (rule RIGHT_RES_FORALL_REGULAR) - prefer 2 - apply (assumption) - apply (metis) - done - -(* The all_prs and ex_prs should be proved for the instance... *) +ML {* val rty = @{typ "'a list"} *} +ML {* val qty = @{typ "'a fset"} *} +ML {* val rel = @{term "list_eq"} *} +ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} +ML {* val rel_refl = @{thm list_eq_refl} *} +ML {* val quot = @{thm QUOTIENT_fset} *} +ML {* val rsp_thms = + @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} + @ @{thms ho_all_prs ho_ex_prs} *} +ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} +ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} +ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} +(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) ML {* -fun r_mk_comb_tac_fset ctxt = - r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} - (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) -*} - - -ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} -ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} -ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} - -ML {* val rty = @{typ "'a list"} *} - -ML {* -fun r_mk_comb_tac_fset ctxt = - r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} - (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) + val consts = [@{const_name "Nil"}, @{const_name "Cons"}, + @{const_name "membship"}, @{const_name "card1"}, + @{const_name "append"}, @{const_name "fold1"}, + @{const_name "map"}]; *} - -ML {* trm_r *} -prove list_induct_tr: trm_r -apply (atomize(full)) -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -done - -prove list_induct_t: trm -apply (simp only: list_induct_tr[symmetric]) -apply (tactic {* rtac thm 1 *}) -done - -thm m2 -ML {* atomize_thm @{thm m2} *} - -prove m2_r_p: {* - build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \"} @{context} *} - apply (simp add: equiv_res_forall[OF equiv_list_eq]) -done - -ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *} -ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} -ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} -prove m2_t_p: m2_t_g -apply (atomize(full)) -apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -done - -prove m2_t: m2_t -apply (simp only: m2_t_p[symmetric]) -apply (tactic {* rtac m2_r 1 *}) -done - -lemma id_apply2 [simp]: "id x \ x" - by (simp add: id_def) - -ML {* val quot = @{thm QUOTIENT_fset} *} -ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} -ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} - -ML {* - fun simp_lam_prs lthy thm = - simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) - handle _ => thm +ML {* fun lift_thm_fset lthy t = + lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t *} -ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *} - -ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} - -ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} -ML {* ObjectLogic.rulify rthm *} - - -ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *} - -prove card1_suc_r_p: {* - build_regularize_goal (atomize_thm @{thm card1_suc}) @{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 +lemma eq_r: "a = b \ a \ b" +by (simp add: list_eq_refl) -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 - -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' = simp_lam_prs @{context} @{thm card1_suc_t} *} -ML {* val ithm = simp_allex_prs @{context} quot 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 {* lift_thm_fset @{context} @{thm m1} *} +ML {* lift_thm_fset @{context} @{thm m2} *} +ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} +ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} +ML {* lift_thm_fset @{context} @{thm card1_suc} *} +ML {* lift_thm_fset @{context} @{thm map_append} *} +ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} thm fold1.simps(2) thm list.recs(2) -thm map_append ML {* val ind_r_a = atomize_thm @{thm list.induct} *} (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \"} @{context} *} @@ -438,12 +333,10 @@ 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 +(*prove rg apply(atomize(full)) apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) -done - +done*) ML {* val ind_r_t = Toplevel.program (fn () => repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} @@ -451,7 +344,9 @@ (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) ) *} -ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} +ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} +ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} +ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *} 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 @@ -463,100 +358,30 @@ ML {* val ind_r_a = simp_allex_prs @{context} quot 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 = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *} +ML {* val defs_sym = add_lower_defs @{context} defs *} +ML {* val ind_r_d = repeat_eqsubst_thm @{context} 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 *} ML {* -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 \"} @{thm equiv_list_eq} @{context}; - 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 ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); - val ind_r_l = simp_lam_prs @{context} ind_r_t; - val ind_r_a = simp_allex_prs @{context} quot ind_r_l; - val ind_r_d = repeat_eqsubst_thm @{context} 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 fset_defs - -lemma eq_r: "a = b \ a \ b" -by (simp add: list_eq_refl) - - -ML {* lift @{thm m2} *} -ML {* lift @{thm m1} *} -ML {* lift @{thm list_eq.intros(4)} *} -ML {* lift @{thm list_eq.intros(5)} *} -ML {* lift @{thm card1_suc} *} -ML {* lift @{thm map_append} *} -ML {* lift @{thm eq_r[OF append_assoc]} *} - -thm - - -(*notation ( output) "prop" ("#_" [1000] 1000) *) -notation ( output) "Trueprop" ("#_" [1000] 1000) - -(* -ML {* - fun lift_theorem_fset_aux thm lthy = + fun lift_thm_fset_note name thm lthy = let - val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; - val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; - val cgoal = cterm_of @{theory} goal; - val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); - val tac = transconv_fset_tac' @{context}; - val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); - val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) - val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; - val [nthm3] = ProofContext.export lthy2 lthy [nthm2] - in - nthm3 - end -*} -*) - -(* -ML {* lift_theorem_fset_aux @{thm m1} @{context} *} -ML {* - fun lift_theorem_fset name thm lthy = - let - val lifted_thm = lift_theorem_fset_aux thm lthy; + val lifted_thm = lift_thm_fset lthy thm; val (_, lthy2) = note (name, lifted_thm) lthy; in lthy2 end; *} -*) -local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} -local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} -local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} -local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} -thm m1_lift -thm leqi4_lift -thm leqi5_lift -thm m2_lift -ML {* @{thm card1_suc_r} OF [card1_suc_f] *} -(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} - (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*) -(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) - -thm leqi4_lift -ML {* - val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) - val (_, l) = dest_Type typ - val t = Type ("FSet.fset", l) - val v = Var (nam, t) - val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) +local_setup {* + lift_thm_fset_note @{binding "m1l"} @{thm m1} #> + lift_thm_fset_note @{binding "m2l"} @{thm m2} #> + lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #> + lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)} *} - +thm m1l +thm m2l +thm leqi4l +thm leqi5l end diff -r 9b8e039ae960 -r 2a28e7ef3048 Unused.thy --- a/Unused.thy Wed Oct 28 16:48:57 2009 +0100 +++ b/Unused.thy Wed Oct 28 17:17:21 2009 +0100 @@ -1,3 +1,5 @@ +(*notation ( output) "prop" ("#_" [1000] 1000) *) +notation ( output) "Trueprop" ("#_" [1000] 1000) ML {* fun dest_cbinop t = @@ -72,3 +74,15 @@ lemma trueprop_cong: shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)" by auto + +lemma list_induct_hol4: + fixes P :: "'a list ⇒ bool" + assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))" + shows "∀l. (P l)" + using a + apply (rule_tac allI) + apply (induct_tac "l") + apply (simp) + apply (metis) + done +