nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:7c8783d2dcd0
+:d835a2771608
 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
 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 *)
 fun mk_prod_fv (t1, t2) =
 fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
 case binder of
 (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 *)
 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =
 let
 val arg = nth args i
 val arg' = nth args' i
 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
 fun mk_alpha_fv i =
 let
 let
 val arg_names = Datatype_Prop.make_tnames arg_tys
 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
 Library.foldr Logic.mk_implies (flat prems, concl)
 end
 case AList.lookup (op=) bn_args i of
 NONE => (case (AList.lookup (op=) alpha_map ty) of
 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
 BC (_, [], bodies) =>
 map HOLogic.mk_Trueprop
 let
 val arg_names = Datatype_Prop.make_tnames arg_tys
 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
 Library.foldr Logic.mk_implies (flat prems, concl)
 end
 val arg_bn_tys =
 alpha_bns
 |> 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
 |> HOLogic.mk_Trueprop
 in
 |> singleton (ProofContext.export ctxt' ctxt)
 |> Datatype_Aux.split_conj_thm
 |> 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 *)

changeset 2320	d835a2771608
parent 2316	08bbde090a17
child 2322	24de7e548094