# HG changeset patch # User Christian Urban # Date 1256797752 -3600 # Node ID 38810e1df801d25e1d3a6eb29b4a934bf146075a # Parent c643938b846ae5c4ee8cadaf40163ab5ec5cb896# Parent 268a727b0f10ae7b391fab512f4f328eb66c1006 merged diff -r c643938b846a -r 38810e1df801 FSet.thy --- a/FSet.thy Wed Oct 28 20:01:20 2009 +0100 +++ b/FSet.thy Thu Oct 29 07:29:12 2009 +0100 @@ -206,7 +206,7 @@ shows "card1 a = card1 b" using e by induct (simp_all add:memb_rsp) -lemma ho_card1_rsp: "op \ ===> op = card1 card1" +lemma ho_card1_rsp: "(op \ ===> op =) card1 card1" by (simp add: card1_rsp) lemma cons_rsp: @@ -216,7 +216,7 @@ using a by (rule list_eq.intros(5)) lemma ho_cons_rsp: - "op = ===> op \ ===> op \ op # op #" + "(op = ===> op \ ===> op \) op # op #" by (simp add: cons_rsp) lemma append_rsp_fst: @@ -273,7 +273,7 @@ done lemma ho_append_rsp: - "op \ ===> op \ ===> op \ op @ op @" + "(op \ ===> op \ ===> op \) op @ op @" by (simp add: append_rsp) lemma map_rsp: @@ -285,7 +285,7 @@ done lemma fun_rel_id: - "op = ===> op = \ op =" + "(op = ===> op =) \ op =" apply (rule eq_reflection) apply (rule ext) apply (rule ext) @@ -296,7 +296,7 @@ done lemma ho_map_rsp: - "op = ===> op = ===> op \ ===> op \ map map" + "((op = ===> op =) ===> op \ ===> op \) map map" by (simp add: fun_rel_id map_rsp) lemma map_append : @@ -304,136 +304,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} *} @@ -449,12 +356,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"} @@ -462,7 +367,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 @@ -474,98 +381,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]} *} - - -(*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 c643938b846a -r 38810e1df801 IntEx.thy --- a/IntEx.thy Wed Oct 28 20:01:20 2009 +0100 +++ b/IntEx.thy Thu Oct 29 07:29:12 2009 +0100 @@ -111,7 +111,7 @@ done lemma ho_plus_rsp: - "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" + "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) ML {* val consts = [@{const_name "my_plus"}] *} diff -r c643938b846a -r 38810e1df801 LamEx.thy --- a/LamEx.thy Wed Oct 28 20:01:20 2009 +0100 +++ b/LamEx.thy Thu Oct 29 07:29:12 2009 +0100 @@ -119,21 +119,11 @@ ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} -thm a3 -ML {* val t_a = atomize_thm @{thm a3} *} -ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* val abs = findabs rty (prop_of t_a) *} -ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} -ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} -ML {* val t_c = simp_allex_prs @{context} quot t_l *} -ML {* val t_defs_sym = add_lower_defs @{context} defs *} -ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} -ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* ObjectLogic.rulify t_b *} - -thm fresh_def -thm supp_def +ML {* +fun lift_thm_lam lthy t = + lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t +*} +ML {* lift_thm_lam @{context} @{thm a3} *} local_setup {* old_make_const_def @{binding lperm} @{term "perm :: ('a \ 'a) list \ rlam \ rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd @@ -141,17 +131,12 @@ ML {* val consts = @{const_name perm} :: consts *} ML {* val defs = @{thms lperm_def} @ defs *} -ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} -ML {* val t_a = atomize_thm @{thm a3} *} -ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} -ML {* val t_c = simp_allex_prs @{context} quot t_l *} -ML {* val t_defs_sym = add_lower_defs @{context} defs *} -ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} -ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} -ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *} +ML {* +fun lift_thm_lam lthy t = + lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t +*} +ML {* val t_b = lift_thm_lam @{context} @{thm a3} *} +ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *} lemma prod_fun_id: "prod_fun id id = id" apply (simp add: prod_fun_def) done @@ -160,21 +145,9 @@ apply (simp_all add: map.simps) done -ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *} -ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *} +ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} +ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} ML {* ObjectLogic.rulify t_b' *} - - -local_setup {* - make_const_def @{binding lfresh} @{term "fresh :: 'a \ rlam \ bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> -*} -@{const_name fresh} :: -lfresh_def -ML {* -fun lift_thm_lam lthy t = - lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t -*} - -ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} - +ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} +ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) diff -r c643938b846a -r 38810e1df801 QuotScript.thy --- a/QuotScript.thy Wed Oct 28 20:01:20 2009 +0100 +++ b/QuotScript.thy Thu Oct 29 07:29:12 2009 +0100 @@ -131,9 +131,9 @@ "FUN_REL E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" abbreviation - FUN_REL_syn ("_ ===> _") + FUN_REL_syn (infixr "===>" 55) where - "E1 ===> E2 \ FUN_REL E1 E2" + "E1 ===> E2 \ FUN_REL E1 E2" lemma FUN_REL_EQ: "(op =) ===> (op =) = (op =)" @@ -512,11 +512,11 @@ (* These are the fixed versions, general ones need to be proved. *) lemma ho_all_prs: - shows "op = ===> op = ===> op = All All" + shows "((op = ===> op =) ===> op =) All All" by auto -lemma ho_ex_prs: - shows "op = ===> op = ===> op = Ex Ex" +lemma ho_ex_prs: + shows "((op = ===> op =) ===> op =) Ex Ex" by auto end diff -r c643938b846a -r 38810e1df801 Unused.thy --- a/Unused.thy Wed Oct 28 20:01:20 2009 +0100 +++ b/Unused.thy Thu Oct 29 07:29:12 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 +