# HG changeset patch # User Christian Urban # Date 1277208300 -3600 # Node ID d835a277160851ce864378a1813970b5f0334287 # Parent 7c8783d2dcd0ab9906487840d3ad1ae13399cb49 prove that alpha implies alpha_bn (needed for rsp proofs) diff -r 7c8783d2dcd0 -r d835a2771608 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Mon Jun 21 15:41:59 2010 +0100 +++ b/Nominal/Ex/CoreHaskell.thy Tue Jun 22 13:05:00 2010 +0100 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 12]] +declare [[STEPS = 13]] nominal_datatype tkind = KStar diff -r 7c8783d2dcd0 -r d835a2771608 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon Jun 21 15:41:59 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Tue Jun 22 13:05:00 2010 +0100 @@ -4,8 +4,7 @@ atom_decl name -declare [[STEPS = 12]] - +declare [[STEPS = 13]] nominal_datatype trm = Var "name" @@ -16,53 +15,11 @@ | Bar x::"name" y::"name" t::"trm" bind y x in t x y | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 and assg = - As "name" "name" "trm" "name" + As "name" x::"name" t::"trm" bind x in t binder bn::"assg \ atom set" where - "bn (As x y t z) = {atom x}" - - -lemma - shows "alpha_trm_raw x x" - and "alpha_assg_raw y y" - and "alpha_bn_raw y y" -apply(induct rule: trm_raw_assg_raw.inducts) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule refl) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(assumption) -apply(assumption) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(rule alpha_gen_refl) -apply(assumption) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(rule alpha_gen_refl) -apply(assumption) -apply(assumption) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(rule alpha_gen_refl) -apply(simp only: prod_alpha_def split_conv prod_rel.simps) -apply(simp) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule_tac x="0" in exI) -apply(rule alpha_gen_refl) -apply(simp only: prod_alpha_def split_conv prod_rel.simps) -apply(simp) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule refl) -apply(rule refl) -apply(assumption) -apply(rule refl) -apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) -apply(rule refl) -apply(assumption) -apply(rule refl) -done - + "bn (As x y t) = {atom x}" thm trm_assg.fv diff -r 7c8783d2dcd0 -r d835a2771608 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon Jun 21 15:41:59 2010 +0100 +++ b/Nominal/NewParser.thy Tue Jun 22 13:05:00 2010 +0100 @@ -436,14 +436,24 @@ alpha_intros alpha_induct alpha_cases 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 + 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 _ = - if get_STEPS lthy > 12 + if get_STEPS lthy > 13 then true else raise TEST lthy4 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; diff -r 7c8783d2dcd0 -r d835a2771608 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Jun 21 15:41:59 2010 +0100 +++ b/Nominal/nominal_dt_alpha.ML Tue Jun 22 13:05:00 2010 +0100 @@ -19,11 +19,15 @@ 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_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct +fun lookup xs x = the (AList.lookup (op=) xs x) +fun group xs = AList.group (op=) xs + (** definition of the inductive rules for alpha and alpha_bn **) (* construct the compound terms for prod_fv and prod_alpha *) @@ -89,7 +93,7 @@ (NONE, _) => [] | (SOME bn, i) => if member (op=) bodies i then [] - else [the (AList.lookup (op=) alpha_bn_map bn) $ (nth args i) $ (nth args' i)] + else [lookup alpha_bn_map bn $ nth args i $ nth args' i] (* generat the premises for an alpha rule; mk_frees is used if no binders are present *) @@ -102,7 +106,7 @@ val ty = fastype_of arg in if nth is_rec i - then fst (the (AList.lookup (op=) alpha_map ty)) $ arg $ arg' + then fst (lookup alpha_map ty) $ arg $ arg' else HOLogic.mk_eq (arg, arg') end @@ -141,7 +145,7 @@ val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) - val alpha = fst (the (AList.lookup (op=) alpha_map ty)) + val alpha = fst (lookup alpha_map ty) val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in @@ -169,7 +173,7 @@ NONE => [HOLogic.mk_eq (arg, arg')] | SOME (alpha, _) => [alpha $ arg $ arg']) | SOME (NONE) => [] - | SOME (SOME bn) => [the (AList.lookup (op=) alpha_bn_map bn) $ arg $ arg'] + | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg'] end in case bclause of @@ -185,7 +189,7 @@ val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) - val alpha_bn = the (AList.lookup (op=) alpha_bn_map bn_trm) + val alpha_bn = lookup alpha_bn_map bn_trm val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in @@ -361,11 +365,11 @@ |> map fastype_of |> map domain_type val arg_names = Datatype_Prop.make_tnames arg_tys - val arg_bn_names = map (fn ty => the (AList.lookup (op=) (arg_tys ~~ arg_names) ty)) arg_bn_tys + val arg_bn_names = map (lookup (arg_tys ~~ arg_names)) arg_bn_tys val args = map Free (arg_names ~~ arg_tys) val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys) val goal = - AList.group (op=) ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms)) + group ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms)) |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) |> map (foldr1 HOLogic.mk_conj) |> foldr1 HOLogic.mk_conj @@ -538,5 +542,77 @@ |> map (fn th => zero_var_indexes (th RS norm)) end + +(* proves that alpha_raw implies alpha_bn *) + +fun is_true @{term "Trueprop True"} = true + | is_true _ = false + +fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = + Subgoal.FOCUS (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 ]) + end) ctxt + +fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = +let + val alpha_names = map (fst o dest_Const) alpha_trms + + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + val arg_bn_tys = + alpha_bns + |> map fastype_of + |> map domain_type + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys + val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys) + val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys) + + val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2) + val true_trms = map (K @{term True}) arg_tys + + val goal_rhs = + group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms)) + |> map snd + |> map (foldr1 HOLogic.mk_conj) + + val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2) + val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms + + val goal = + (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest + |> foldr1 HOLogic.mk_conj + |> HOLogic.mk_Trueprop +in + 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)) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map (fn th => zero_var_indexes (th RS mp)) + |> map Datatype_Aux.split_conj_thm + |> flat + |> filter_out (is_true o concl_of) +end + + end (* structure *)