nominal2: comparison Nominal/nominal_dt

equal deleted inserted replaced

-:486d4647bb37
+:8f8652a8107f
 (** 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) =
 let
 val ty1 = fastype_of t1
 val ty2 = fastype_of t2
 val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}
 in
 Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2
 end
 fun mk_prod_alpha (t1, t2) =
 let
 val ty1 = fastype_of t1
 val ty2 = fastype_of t2
 val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)
 val resT = [prodT, prodT] ---> @{typ "bool"}
 in
 Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2
 end
 (* generates the compound binder terms *)
 fun mk_binders lthy bmode args binders =
 let
 fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
 | bind_set _ args (SOME bn, i) = bn $ (nth args i)
 fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)
 | bind_lst _ args (SOME bn, i) = bn $ (nth args i)
 val (combine_fn, bind_fn) =
 case bmode of
 Lst => (mk_append, bind_lst)
 | Set => (mk_union,  bind_set)
 | Res => (mk_union,  bind_set)
 in
 binders
 |> map (bind_fn lthy args)
 |> foldl1 combine_fn
 end
 (* produces the term for an alpha with abstraction *)
 fun mk_alpha_term bmode fv alpha args args' binders binders' =
 let
 val (alpha_name, binder_ty) =
 case bmode of
 Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
 | Set => (@{const_name "alpha_set"}, @{typ "atom set"})
 | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
 val ty = fastype_of args
 val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
 val alpha_ty = [ty, ty] ---> @{typ "bool"}
 val fv_ty = ty --> @{typ "atom set"}
 val pair_lhs = HOLogic.mk_prod (binders, args)
 val pair_rhs = HOLogic.mk_prod (binders', args')
 in
 HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},
 Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool})
 $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)
 end
 (* for non-recursive binders we have to produce alpha_bn premises *)
 fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder =
 case binder of
 (NONE, _) => []
 else [lookup alpha_bn_map bn $ nth args i $ nth args' i]
 (* generate 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
 fun mk_frees i =
 let
 val arg = nth args i
 val arg' = nth args' i
 val ty = fastype_of arg
 in
 if nth is_rec i
 then fst (lookup alpha_map ty) $ arg $ arg'
 else HOLogic.mk_eq (arg, arg')
 end
 fun mk_alpha_fv i =
 let
 val ty = fastype_of (nth args i)
 in
 case AList.lookup (op=) alpha_map ty of
 NONE => (HOLogic.eq_const ty, supp_const ty)
 | SOME (alpha, fv) => (alpha, fv)
 end
 in
 case bclause of
 BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies
 | BC (bmode, binders, bodies) =>
 let
 val (alphas, fvs) = split_list (map mk_alpha_fv bodies)
 val comp_fv = foldl1 mk_prod_fv fvs
 val comp_alpha = foldl1 mk_prod_alpha alphas
 val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
 val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
 val comp_binders = mk_binders lthy bmode args binders
 val comp_binders' = mk_binders lthy bmode args' binders
 val alpha_prem =
 mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
 val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)
 in
 map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)
 end
 end
 (* produces the introduction rule for an alpha rule *)
 fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
 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 (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
 (* produces the premise of an alpha-bn rule; we only need to
 treat the case special where the binding clause is empty;
 - if the body is not included in the bn_info, then we either
 produce an equation or an alpha-premise
 - if the body is included in the bn_info, then we create
 either a recursive call to alpha-bn, or no premise  *)
 fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =
 let
-fun mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args') i =
+fun mk_alpha_bn_prem i =
 let
 val arg = nth args i
 val arg' = nth args' i
 val ty = fastype_of arg
 in
 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) => [lookup alpha_bn_map bn $ arg $ arg']
 end
 in
 case bclause of
 BC (_, [], bodies) =>
-map HOLogic.mk_Trueprop
+map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies))
-(flat (map (mk_alpha_bn_prem alpha_map alpha_bn_map bn_args (args, args')) bodies))
+| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
-| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
+end
-end
 fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
 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 = 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
 fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) =
 let
 val nth_constrs_info = nth constrs_info bn_n
 val nth_bclausess = nth bclausesss bn_n
 in
 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =
 let
 val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names
 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys
 val alpha_frees = map Free (alpha_names ~~ alpha_tys)
 val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)
 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
 val alpha_bn_names = map (prefix "alpha_") bn_names
 val alpha_bn_arg_tys = map (nth raw_tys) bn_tys
 val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
 val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
 val alpha_bn_map = bns ~~ alpha_bn_frees
 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss
 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info
 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
 val (alphas, lthy') = Inductive.add_inductive_i
 {quiet_mode = true, verbose = false, alt_name = Binding.empty,
 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
 all_alpha_names [] all_alpha_intros [] lthy
 val all_alpha_trms_loc = #preds alphas;
 val alpha_induct_loc = #raw_induct alphas;
 val alpha_intros_loc = #intrs alphas;
 val alpha_cases_loc = #elims alphas;
 val phi = ProofContext.export_morphism lthy' lthy;
 val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc
 val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy
 val alpha_induct = Morphism.thm phi alpha_induct_loc;
 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms'
 in
 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
 (** produces the distinctness theorems **)
 (* transforms the distinctness theorems of the constructors
 to "not-alphas" of the constructors *)
 fun mk_distinct_goal ty_trm_assoc neq =
 let
 val (lhs, rhs) =
 neq
 |> HOLogic.dest_Trueprop
 |> HOLogic.dest_not
 |> HOLogic.dest_eq
 val ty = fastype_of lhs
 in
 (lookup ty_trm_assoc ty) $ lhs $ rhs
 |> HOLogic.mk_not
 |> HOLogic.mk_Trueprop
 end
 fun distinct_tac cases_thms distinct_thms =
 rtac notI THEN' eresolve_tac cases_thms
 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
 let
 (* proper import of type-variables does not work,
 since then they are replaced by new variables, messing
-up the ty_term assoc list *)
+up the ty_trm assoc list *)
 val distinct_thms' = map Thm.legacy_freezeT distinct_thms
 val ty_trm_assoc = alpha_tys ~~ alpha_trms
 fun mk_alpha_distinct distinct_trm =
 let
 val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt
 val goal = mk_distinct_goal ty_trm_assoc distinct_trm
 in
 Goal.prove ctxt' [] [] goal
 (K (distinct_tac cases_thms distinct_thms 1))
 |> singleton (Variable.export ctxt' ctxt)
 end
 in
 map (mk_alpha_distinct o prop_of) distinct_thms'
 |> map Thm.varifyT_global
 end
 (** produces the alpha_eq_iff simplification rules **)
 if hyps = [] then HOLogic.mk_Trueprop concl
 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
 end;
 fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =
 let
 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
 val goals = map mk_alpha_eq_iff_goal thms_imp;
 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;
 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;
 in
 Variable.export ctxt' ctxt thms
 |> map mk_simp_rule
 end
 (** proof by induction over the alpha-definitions **)
 fun is_true @{term "Trueprop True"} = true
 | is_true _ = false
 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
 let
 val arg_tys = map (domain_type o fastype_of) alphas
 val ((arg_names1, arg_names2), ctxt') =
 ctxt
 |> Variable.variant_fixes (replicate (length alphas) "x")
 ||>> Variable.variant_fixes (replicate (length alphas) "y")
 val args1 = map2 (curry Free) arg_names1 arg_tys
 val args2 = map2 (curry Free) arg_names2 arg_tys
 val true_trms = replicate (length alphas) (K @{term True})
 fun apply_all x fs = map (fn f => f x) fs
 val goals_rhs =
 group (props @ (alphas ~~ true_trms))
 |> map snd
 |> map2 apply_all (args1 ~~ args2)
 |> map fold_conj
 fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
 val goals =
 (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
 |> foldr1 HOLogic.mk_conj
 |> HOLogic.mk_Trueprop
 fun tac ctxt =
 HEADGOAL
 (DETERM o (rtac alpha_induct_thm)
 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
 in
 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
 |> singleton (ProofContext.export ctxt' ctxt)
 |> Datatype_Aux.split_conj_thm
 |> map (fn th => th RS mp)
 |> map Datatype_Aux.split_conj_thm
 |> flat
 |> map zero_var_indexes
 |> filter_out (is_true o concl_of)
 end
 (** reflexivity proof for the alphas **)
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
 fun cases_tac intros =
 let
 val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
 val bound_tac =
 EVERY' [ rtac exi_zero,
 resolve_tac @{thms alpha_refl},
 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
 in
 REPEAT o FIRST' [rtac @{thm conjI},
 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
 end
 fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
 let
 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_names = Datatype_Prop.make_tnames arg_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 =
 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
 Goal.prove ctxt arg_names [] goal
 (fn {context, ...} =>
 HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros))
 |> Datatype_Aux.split_conj_thm
 |> map Datatype_Aux.split_conj_thm
 |> flat
 end
 (** symmetry proof for the alphas **)
 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"
 by (erule exE, rule_tac x="-p" in exI, auto)}
 (* for premises that contain binders *)
 fun prem_bound_tac pred_names ctxt =
 let
 fun trans_prem_tac pred_names ctxt =
 SUBPROOF (fn {prems, context, ...} =>
 let
 val prems' = map (transform_prem1 context pred_names) prems
 in
 resolve_tac prems' 1
 end) ctxt
 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
 in
 EVERY'
 [ etac exi_neg,
 resolve_tac @{thms alpha_sym_eqvt},
 asm_full_simp_tac (HOL_ss addsimps prod_simps),
 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
 trans_prem_tac pred_names ctxt ]
 end
 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
 let
 val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
 fun tac ctxt =
 let
 val alpha_names =  map (fst o dest_Const) alpha_trms
 in
 resolve_tac alpha_intros THEN_ALL_NEW
 FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
 end
 in
 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt
 end
 (** transitivity proof for alphas **)
 (* applies cases rules and resolves them with the last premise *)
 in
 HEADGOAL (rtac exi_inst)
 end)
 fun non_trivial_cases_tac pred_names intros ctxt =
 let
 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
 in
 resolve_tac intros
 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN'
 TRY o EVERY'   (* if binders are present *)
 [ etac @{thm exE},
 etac @{thm exE},
 perm_inst_tac ctxt,
 resolve_tac @{thms alpha_trans_eqvt},
 atac,
 aatac pred_names ctxt,
 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
 asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
 end
 fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
 let
 fun all_cases ctxt =
 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms)
 THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
 in
 EVERY' [ rtac @{thm allI}, rtac @{thm impI},
 ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
 end
 fun prep_trans_goal alpha_trm (arg1, arg2) =
 let
 val arg_ty = fastype_of arg1
 val mid = alpha_trm $ arg2 $ (Bound 0)
 val rhs = alpha_trm $ arg1 $ (Bound 0)
 in
 HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
 end
 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
 let
 val alpha_names =  map (fst o dest_Const) alpha_trms
 val props = map prep_trans_goal alpha_trms
 val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
 in
 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
 end
 (** proves the equivp predicate for all alphas **)
 val transp_def' =
 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)"
 by (rule eq_reflection, auto simp add: transp_def)}
 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt =
 let
 val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
 val symm' = map (fold_rule @{thms symp_def} o atomize) symm
 val trans' = map (fold_rule [transp_def'] o 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 @ alpha_bns))
 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN'
 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
 |> chop (length alphas)
 end
 (* proves that alpha_raw implies alpha_bn *)
 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt =
 resolve_tac prems'',
 resolve_tac alpha_intros ]))
 end) ctxt
 fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
 let
 val arg_ty = domain_type o fastype_of
 val alpha_names =  map (fst o dest_Const) alpha_trms
 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
 val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
 in
 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct
 (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
 end
 (* respectfulness for fv_raw / bn_raw *)
 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
 let
 val arg_ty = domain_type o fastype_of
 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
 fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps}
 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left})
 in
 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct
 (K (asm_full_simp_tac ss)) ctxt
 end
 (* respectfulness for size *)
 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
 let
 val arg_tys = map (domain_type o fastype_of) all_alpha_trms
 fun mk_prop ty (x, y) = HOLogic.mk_eq
 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
 val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys
 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps
 permute_prod_def prod.cases prod.recs})
 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
 in
 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
 end
 (* respectfulness for constructors *)
 fun raw_constr_rsp_tac alpha_intros simps =
 let
 val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
 val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps
 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
-(* funs_rsp alpha_bn_simps *)
+in
-in
+asm_full_simp_tac pre_ss
-asm_full_simp_tac pre_ss
+THEN' REPEAT o (resolve_tac @{thms allI impI})
-THEN' REPEAT o (resolve_tac @{thms allI impI})
+THEN' resolve_tac alpha_intros
-THEN' resolve_tac alpha_intros
+THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
-THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
+end
-end
 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
 let
 val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
 fun lookup ty =
 case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
 NONE => HOLogic.eq_const ty
 | SOME alpha => alpha
 fun fun_rel_app t1 t2 =
 Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
 fun prep_goal trm =
 trm
 |> strip_type o fastype_of
 |>> map lookup
 ||> lookup
 |> uncurry (fold_rev fun_rel_app)
 |> (fn t => t $ trm $ trm)
 |> Syntax.check_term ctxt
 |> HOLogic.mk_Trueprop
 in
 Goal.prove_multi ctxt [] [] (map prep_goal constrs)
 (K (HEADGOAL
 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))
 end
 (* rsp lemmas for alpha_bn relations *)
 val rsp_equivp =
 (* we have to reorder the alpha_bn_imps theorems in order
 to be in order with alpha_bn_trms *)
 fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =
 let
 fun mk_map thm =
 thm |> `prop_of
 |>> List.last  o snd o strip_comb
 |>> HOLogic.dest_Trueprop
 |>> head_of
 |>> fst o dest_Const
 val alpha_bn_imps' =
 map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms
 fun mk_thm thm1 thm2 =
 (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
 in
 map2 mk_thm alpha_bn_equivp alpha_bn_imps'
 end
 (* transformation of the natural rsp-lemmas into standard form *)
 val fun_rsp = @{lemma
 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
 fun mk_funs_rsp thm =
 thm
 |> atomize
 |> single
 |> curry (op OF) fun_rsp
 val permute_rsp = @{lemma
 "(!x y p. R x y --> R (permute p x) (permute p y))
 ==> ((op =) ===> R ===> R) permute permute"  by simp}
 fun mk_alpha_permute_rsp thm =
 thm
 |> atomize
 |> single
 |> curry (op OF) permute_rsp
 end (* structure *)

changeset 2476	8f8652a8107f
parent 2475	486d4647bb37
child 2477	2f289c1f6cf1