--- a/Nominal/nominal_dt_alpha.ML Fri Sep 10 09:17:40 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML Sat Sep 11 05:56:49 2010 +0800
@@ -45,62 +45,62 @@
(* 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
+ 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
+ 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)
+ 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
+ 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
+ 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 =
@@ -113,59 +113,59 @@
(* 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
+ 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
+ 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
+ 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;
@@ -176,92 +176,91 @@
- 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 =
let
- val arg = nth args i
- val arg' = nth args' i
- val ty = fastype_of arg
+ 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 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
- (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
-end
+ case bclause of
+ BC (_, [], bodies) =>
+ map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies))
+ | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause
+ 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
+ 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
+ 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)
+ 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 (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 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 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 (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_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 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
+ 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
@@ -270,18 +269,18 @@
(* 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
+ 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
@@ -289,27 +288,27 @@
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 *)
- val distinct_thms' = map Thm.legacy_freezeT distinct_thms
- val ty_trm_assoc = alpha_tys ~~ alpha_trms
+ let
+ (* proper import of type-variables does not work,
+ since then they are replaced by new variables, messing
+ 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
+ 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
- Goal.prove ctxt' [] [] goal
- (K (distinct_tac cases_thms distinct_thms 1))
- |> singleton (Variable.export ctxt' ctxt)
+ map (mk_alpha_distinct o prop_of) distinct_thms'
+ |> map Thm.varifyT_global
end
-
-in
- map (mk_alpha_distinct o prop_of) distinct_thms'
- |> map Thm.varifyT_global
-end
@@ -341,15 +340,15 @@
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
+ 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 **)
@@ -358,48 +357,48 @@
| 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
+ 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 ((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 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})
+ 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_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)
+ 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
+ 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
+ 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 **)
@@ -407,48 +406,48 @@
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}
+ let
+ val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
- val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
+ 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
+ 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
+ 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
@@ -459,38 +458,38 @@
(* 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
+ 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
+ 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]
+ 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
-in
- alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt
-end
(** transitivity proof for alphas **)
@@ -516,50 +515,50 @@
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
+ 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
+ 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
+ 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
+ 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 **)
@@ -569,19 +568,19 @@
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
+ 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
+ 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 *)
@@ -602,100 +601,99 @@
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
+ 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)
+ 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 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})
+ 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
+ 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
+ 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)
+ 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 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 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
+ 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
- asm_full_simp_tac pre_ss
- THEN' REPEAT o (resolve_tac @{thms allI impI})
- THEN' resolve_tac alpha_intros
- THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
-end
+ 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
+ in
+ asm_full_simp_tac pre_ss
+ THEN' REPEAT o (resolve_tac @{thms allI impI})
+ THEN' resolve_tac alpha_intros
+ THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
+ 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
+ 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 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 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
+ 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 *)
@@ -708,22 +706,22 @@
(* 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
+ 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
+ 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
+ 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 *)
@@ -732,10 +730,10 @@
"(!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
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) fun_rsp
val permute_rsp = @{lemma
@@ -743,10 +741,10 @@
==> ((op =) ===> R ===> R) permute permute" by simp}
fun mk_alpha_permute_rsp thm =
- thm
- |> atomize
- |> single
- |> curry (op OF) permute_rsp
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) permute_rsp