# HG changeset patch # User Christian Urban # Date 1277226473 -3600 # Node ID 24de7e54809478e94c75efbbcdf8dad3aae16c70 # Parent e9b0728061a840df6e75e6ae24f8696a55fb50ff proved eqvip theorems for alphas diff -r e9b0728061a8 -r 24de7e548094 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue Jun 22 13:31:42 2010 +0100 +++ b/Nominal/Ex/CoreHaskell.thy Tue Jun 22 18:07:53 2010 +0100 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 13]] +declare [[STEPS = 14]] nominal_datatype tkind = KStar diff -r e9b0728061a8 -r 24de7e548094 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jun 22 13:31:42 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Tue Jun 22 18:07:53 2010 +0100 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 13]] +declare [[STEPS = 14]] nominal_datatype trm = Var "name" @@ -21,7 +21,6 @@ where "bn (As x y t) = {atom x}" - thm trm_assg.fv thm trm_assg.supp thm trm_assg.eq_iff diff -r e9b0728061a8 -r 24de7e548094 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Tue Jun 22 13:31:42 2010 +0100 +++ b/Nominal/NewParser.thy Tue Jun 22 18:07:53 2010 +0100 @@ -436,44 +436,36 @@ alpha_intros alpha_induct alpha_cases lthy_tmp'' else raise TEST lthy4 + val alpha_equivp_thms = + if get_STEPS lthy > 12 + then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp'' + else raise TEST lthy4 + (* proving alpha implies alpha_bn *) val _ = warning "Proving alpha implies bn" val alpha_bn_imp_thms = - if get_STEPS lthy > 12 + if get_STEPS lthy > 13 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' else raise TEST lthy4 - - + val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) val _ = tracing ("alpha_refl\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) val _ = tracing ("alpha_bn_imp\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) + val _ = tracing ("alpha_equivp\n" ^ + cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms)) (* old stuff *) val _ = - if get_STEPS lthy > 13 - then true else raise TEST lthy4 - - val bn_nos = map (fn (_, i, _) => i) raw_bn_info; - val bns = raw_bn_funs ~~ bn_nos; - - val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos - - val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; - - val _ = tracing ("reflps\n" ^ - cat_lines (map (Syntax.string_of_term lthy4 o prop_of) reflps)) - - val _ = - if get_STEPS lthy > 13 + if get_STEPS lthy > 14 then true else raise TEST lthy4 val alpha_equivp = if !cheat_equivp then map (equivp_hack lthy4) alpha_trms - else build_equivps alpha_trms reflps alpha_induct + else build_equivps alpha_trms alpha_refl_thms alpha_induct inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; val qty_binds = map (fn (_, b, _, _) => b) dts; @@ -488,6 +480,10 @@ Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = warning "Proving respects"; + + val bn_nos = map (fn (_, i, _) => i) raw_bn_info; + val bns = raw_bn_funs ~~ bn_nos; + val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; val (bns_rsp_pre, lthy9) = fold_map ( fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => @@ -496,6 +492,9 @@ fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy else fvbv_rsp_tac alpha_induct raw_fv_defs lthy8 1; + + val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos + val fv_rsps = prove_fv_rsp fv_alpha_all alpha_trms fv_rsp_tac lthy9; val (fv_rsp_pre, lthy10) = fold_map (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] @@ -510,7 +509,7 @@ alpha_bn_rsp_tac) alpha_bn_trms lthy11 fun const_rsp_tac _ = let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a - in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end + in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] const_rsp_tac) raw_consts lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) diff -r e9b0728061a8 -r 24de7e548094 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Tue Jun 22 13:31:42 2010 +0100 +++ b/Nominal/nominal_dt_alpha.ML Tue Jun 22 18:07:53 2010 +0100 @@ -19,6 +19,7 @@ val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list + val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list end @@ -542,6 +543,26 @@ |> map (fn th => zero_var_indexes (th RS norm)) end +(* proves the equivp predicate for all alphas *) + +val equivp_intro = + @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R" + by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} + +fun raw_prove_equivp alphas refl symm trans ctxt = +let + val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars + val refl' = map atomize refl + val symm' = map atomize symm + val trans' = map atomize trans + fun prep_goal t = + HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) +in + Goal.prove_multi ctxt [] [] (map prep_goal alphas) + (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' + RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) +end + (* proves that alpha_raw implies alpha_bn *) @@ -549,17 +570,18 @@ | is_true _ = false fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = - Subgoal.FOCUS (fn {prems, context, ...} => + SUBPROOF (fn {prems, context, ...} => let val prems' = flat (map Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 context pred_names) prems' in - HEADGOAL (REPEAT o - FIRST' [ rtac @{thm TrueI}, - rtac @{thm conjI}, - resolve_tac prems', - resolve_tac prems'', - resolve_tac alpha_intros ]) + HEADGOAL + (REPEAT_ALL_NEW + (FIRST' [ rtac @{thm TrueI}, + rtac @{thm conjI}, + resolve_tac prems', + resolve_tac prems'', + resolve_tac alpha_intros ])) end) ctxt fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = @@ -604,7 +626,7 @@ Goal.prove ctxt' [] [] goal (fn {context, ...} => HEADGOAL (DETERM o (rtac alpha_induct) - THEN_ALL_NEW raw_prove_bn_imp_tac alpha_names alpha_intros context)) + THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context))) |> singleton (ProofContext.export ctxt' ctxt) |> Datatype_Aux.split_conj_thm |> map (fn th => zero_var_indexes (th RS mp)) @@ -613,6 +635,5 @@ |> filter_out (is_true o concl_of) end - end (* structure *)