# HG changeset patch # User Christian Urban # Date 1284155809 -28800 # Node ID 8f8652a8107fed4cc41d466eaac7cb77854bee88 # Parent 486d4647bb371938d0d35a9948666af346f22573 tuned (to conform with indentation policy of Markus) diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_alpha.ML --- 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 diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Fri Sep 10 09:17:40 2010 +0800 +++ b/Nominal/nominal_dt_quot.ML Sat Sep 11 05:56:49 2010 +0800 @@ -29,63 +29,63 @@ (* defines the quotient types *) fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = -let - val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms - val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms -in - fold_map Quotient_Type.add_quotient_type qty_args2 lthy -end + let + val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms + val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms + in + fold_map Quotient_Type.add_quotient_type qty_args2 lthy + end (* defines quotient constants *) fun define_qconsts qtys consts_specs lthy = -let - val (qconst_infos, lthy') = - fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy - val phi = ProofContext.export_morphism lthy' lthy -in - (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') -end + let + val (qconst_infos, lthy') = + fold_map (Quotient_Def.lift_raw_const qtys) consts_specs lthy + val phi = ProofContext.export_morphism lthy' lthy + in + (map (Quotient_Info.transform_qconsts phi) qconst_infos, lthy') + end (* defines the quotient permutations and proves pt-class *) fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = -let - val lthy1 = - lthy - |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) + let + val lthy1 = + lthy + |> Local_Theory.exit_global + |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) - val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 + val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 - val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 + val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 - val lifted_perm_laws = - map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' - |> Variable.exportT lthy3 lthy2 + val lifted_perm_laws = + map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' + |> Variable.exportT lthy3 lthy2 - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac lifted_perm_laws)) -in - lthy2 - |> Class.prove_instantiation_exit tac - |> Named_Target.theory_init -end + fun tac _ = + Class.intro_classes_tac [] THEN + (ALLGOALS (resolve_tac lifted_perm_laws)) + in + lthy2 + |> Class.prove_instantiation_exit tac + |> Named_Target.theory_init + end (* defines the size functions and proves size-class *) fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = -let - fun tac _ = Class.intro_classes_tac [] -in - lthy - |> Local_Theory.exit_global - |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) - |> snd o (define_qconsts qtys size_specs) - |> Class.prove_instantiation_exit tac - |> Named_Target.theory_init -end + let + val tac = K (Class.intro_classes_tac []) + in + lthy + |> Local_Theory.exit_global + |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) + |> snd o (define_qconsts qtys size_specs) + |> Class.prove_instantiation_exit tac + |> Named_Target.theory_init + end (* lifts a theorem and cleans all "_raw" parts @@ -99,28 +99,28 @@ val parser = Scan.repeat (exclude || any) in fun unraw_str s = - s |> explode - |> Scan.finite Symbol.stopper parser >> implode - |> fst + s |> explode + |> Scan.finite Symbol.stopper parser >> implode + |> fst end fun unraw_vars_thm thm = -let - fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) + let + fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) - val vars = Term.add_vars (prop_of thm) [] - val vars' = map (Var o unraw_var_str) vars -in - Thm.certify_instantiate ([], (vars ~~ vars')) thm -end + val vars = Term.add_vars (prop_of thm) [] + val vars' = map (Var o unraw_var_str) vars + in + Thm.certify_instantiate ([], (vars ~~ vars')) thm + end fun unraw_bounds_thm th = -let - val trm = Thm.prop_of th - val trm' = Term.map_abs_vars unraw_str trm -in - Thm.rename_boundvars trm trm' th -end + let + val trm = Thm.prop_of th + val trm' = Term.map_abs_vars unraw_str trm + in + Thm.rename_boundvars trm trm' th + end fun lift_thms qtys simps thms ctxt = (map (Quotient_Tacs.lifted ctxt qtys simps diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Fri Sep 10 09:17:40 2010 +0800 +++ b/Nominal/nominal_dt_rawfuns.ML Sat Sep 11 05:56:49 2010 +0800 @@ -82,64 +82,64 @@ (* functions for producing sets, fsets and lists of general atom type out from concrete atom types *) fun mk_atom_set t = -let - val ty = fastype_of t; - val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; - val img_ty = atom_ty --> ty --> @{typ "atom set"}; -in - Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t -end + let + val ty = fastype_of t; + val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; + val img_ty = atom_ty --> ty --> @{typ "atom set"}; + in + Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t + end fun dest_fsetT (Type (@{type_name fset}, [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); fun mk_atom_fset t = -let - val ty = fastype_of t; - val atom_ty = dest_fsetT ty --> @{typ "atom"}; - val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; - val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} -in - fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) -end + let + val ty = fastype_of t; + val atom_ty = dest_fsetT ty --> @{typ "atom"}; + val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; + val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} + in + fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) + end -fun mk_atom_list t = -let - val ty = fastype_of t; - val atom_ty = dest_listT ty --> @{typ atom}; - val map_ty = atom_ty --> ty --> @{typ "atom list"}; -in - Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t -end + fun mk_atom_list t = + let + val ty = fastype_of t; + val atom_ty = dest_listT ty --> @{typ atom}; + val map_ty = atom_ty --> ty --> @{typ "atom list"}; + in + Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t + end (* functions that coerces singletons, sets and fsets of concrete atoms into sets of general atoms *) fun setify ctxt t = -let - val ty = fastype_of t; -in - if is_atom ctxt ty - then HOLogic.mk_set @{typ atom} [mk_atom t] - else if is_atom_set ctxt ty - then mk_atom_set t - else if is_atom_fset ctxt ty - then mk_atom_fset t - else raise TERM ("setify", [t]) -end + let + val ty = fastype_of t; + in + if is_atom ctxt ty + then HOLogic.mk_set @{typ atom} [mk_atom t] + else if is_atom_set ctxt ty + then mk_atom_set t + else if is_atom_fset ctxt ty + then mk_atom_fset t + else raise TERM ("setify", [t]) + end (* functions that coerces singletons and lists of concrete atoms into lists of general atoms *) fun listify ctxt t = -let - val ty = fastype_of t; -in - if is_atom ctxt ty - then HOLogic.mk_list @{typ atom} [mk_atom t] - else if is_atom_list ctxt ty - then mk_atom_set t - else raise TERM ("listify", [t]) -end + let + val ty = fastype_of t; + in + if is_atom ctxt ty + then HOLogic.mk_list @{typ atom} [mk_atom t] + else if is_atom_list ctxt ty + then mk_atom_set t + else raise TERM ("listify", [t]) + end (* coerces a list into a set *) fun to_set t = @@ -152,136 +152,136 @@ (** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = -let - fun mk_fv_body fv_map args i = let - val arg = nth args i - val ty = fastype_of arg - in - case AList.lookup (op=) fv_map ty of - NONE => mk_supp arg - | SOME fv => fv $ arg - end + fun mk_fv_body fv_map args i = + let + val arg = nth args i + val ty = fastype_of arg + in + case AList.lookup (op=) fv_map ty of + NONE => mk_supp arg + | SOME fv => fv $ arg + end fun mk_fv_binder lthy fv_bn_map args binders = - let - fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) - | bind_set _ args (SOME bn, i) = (bn $ (nth args i), - if member (op=) bodies i then @{term "{}::atom set"} - else lookup fv_bn_map bn $ (nth args i)) - fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) - | bind_lst _ args (SOME bn, i) = (bn $ (nth args i), - if member (op=) bodies i then @{term "[]::atom list"} - else lookup fv_bn_map bn $ (nth args i)) + let + fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) + | bind_set _ args (SOME bn, i) = (bn $ (nth args i), + if member (op=) bodies i then @{term "{}::atom set"} + else lookup fv_bn_map bn $ (nth args i)) + fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) + | bind_lst _ args (SOME bn, i) = (bn $ (nth args i), + if member (op=) bodies i then @{term "[]::atom list"} + else lookup fv_bn_map bn $ (nth args i)) - val (combine_fn, bind_fn) = - case bmode of - Lst => (fold_append, bind_lst) - | Set => (fold_union, bind_set) - | Res => (fold_union, bind_set) - in - binders - |> map (bind_fn lthy args) - |> split_list - |> pairself combine_fn - end + val (combine_fn, bind_fn) = + case bmode of + Lst => (fold_append, bind_lst) + | Set => (fold_union, bind_set) + | Res => (fold_union, bind_set) + in + binders + |> map (bind_fn lthy args) + |> split_list + |> pairself combine_fn + end - val t1 = map (mk_fv_body fv_map args) bodies - val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders -in - mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) -end + val t1 = map (mk_fv_body fv_map args) bodies + val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders + in + mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) + end (* in case of fv_bn we have to treat the case special, where an "empty" binding clause is given *) fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = -let - fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = let - val arg = nth args i - val ty = fastype_of arg + fun mk_fv_bn_body i = + let + val arg = nth args i + val ty = fastype_of arg + in + case AList.lookup (op=) bn_args i of + NONE => (case (AList.lookup (op=) fv_map ty) of + NONE => mk_supp arg + | SOME fv => fv $ arg) + | SOME (NONE) => @{term "{}::atom set"} + | SOME (SOME bn) => lookup fv_bn_map bn $ arg + end in - case AList.lookup (op=) bn_args i of - NONE => (case (AList.lookup (op=) fv_map ty) of - NONE => mk_supp arg - | SOME fv => fv $ arg) - | SOME (NONE) => @{term "{}::atom set"} - | SOME (SOME bn) => lookup fv_bn_map bn $ arg - end -in - case bclause of - BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) - | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause -end + case bclause of + BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies) + | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause + end fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = -let - val arg_names = Datatype_Prop.make_tnames arg_tys - val args = map Free (arg_names ~~ arg_tys) - val fv = lookup fv_map ty - val lhs = fv $ list_comb (constr, args) - val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses - val rhs = fold_union rhs_trms -in - HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -end + let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv = lookup fv_map ty + val lhs = fv $ list_comb (constr, args) + val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses + val rhs = fold_union rhs_trms + in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + end fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = -let - val arg_names = Datatype_Prop.make_tnames arg_tys - val args = map Free (arg_names ~~ arg_tys) - val fv_bn = lookup fv_bn_map bn_trm - val lhs = fv_bn $ list_comb (constr, args) - val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses - val rhs = fold_union rhs_trms -in - HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -end + let + val arg_names = Datatype_Prop.make_tnames arg_tys + val args = map Free (arg_names ~~ arg_tys) + val fv_bn = lookup fv_bn_map bn_trm + val lhs = fv_bn $ list_comb (constr, args) + val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses + val rhs = fold_union rhs_trms + in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + end fun mk_fv_bn_eqs lthy fv_map fv_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_fv_bn_eq lthy bn_trm fv_map fv_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_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess + end fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms size_simps lthy = -let - val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names - val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys - val fv_frees = map Free (fv_names ~~ fv_tys); - val fv_map = raw_tys ~~ fv_frees + let + val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names + val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys + val fv_frees = map Free (fv_names ~~ fv_tys); + val fv_map = raw_tys ~~ fv_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 fv_bn_names = map (prefix "fv_") bn_names - val fv_bn_arg_tys = map (nth raw_tys) bn_tys - val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys - val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) - val fv_bn_map = bns ~~ fv_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 fv_bn_names = map (prefix "fv_") bn_names + val fv_bn_arg_tys = map (nth raw_tys) bn_tys + val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys + val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) + val fv_bn_map = bns ~~ fv_bn_frees - val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss - val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info + val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss + val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info - val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) - val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) + val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) + val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) - val (_, lthy') = Function.add_function all_fun_names all_fun_eqs - Function_Common.default_config (pat_completeness_simp constr_thms) lthy + val (_, lthy') = Function.add_function all_fun_names all_fun_eqs + Function_Common.default_config (pat_completeness_simp constr_thms) lthy - val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') + val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') - val {fs, simps, inducts, ...} = info; + val {fs, simps, inducts, ...} = info; - val morphism = ProofContext.export_morphism lthy'' lthy - val simps_exp = map (Morphism.thm morphism) (the simps) - val inducts_exp = map (Morphism.thm morphism) (the inducts) + val morphism = ProofContext.export_morphism lthy'' lthy + val simps_exp = map (Morphism.thm morphism) (the simps) + val inducts_exp = map (Morphism.thm morphism) (the inducts) - val (fvs', fv_bns') = chop (length fv_frees) fs -in - (fvs', fv_bns', simps_exp, inducts_exp, lthy'') -end + val (fvs', fv_bns') = chop (length fv_frees) fs + in + (fvs', fv_bns', simps_exp, inducts_exp, lthy'') + end (** equivarance proofs **) @@ -302,12 +302,12 @@ THEN_ALL_NEW subproof_tac const_names simps ctxt) fun mk_eqvt_goal pi const arg = -let - val lhs = mk_perm pi (const $ arg) - val rhs = const $ (mk_perm pi arg) -in - HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -end + let + val lhs = mk_perm pi (const $ arg) + val rhs = const $ (mk_perm pi arg) + in + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + end fun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Fri Sep 10 09:17:40 2010 +0800 +++ b/Nominal/nominal_dt_rawperm.ML Sat Sep 11 05:56:49 2010 +0800 @@ -21,109 +21,109 @@ (** proves the two pt-type class properties **) fun prove_permute_zero induct perm_defs perm_fns lthy = -let - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types + let + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types - fun single_goal ((perm_fn, T), x) = - HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) + fun single_goal ((perm_fn, T), x) = + HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy perm_indnames [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 + in + Goal.prove lthy perm_indnames [] goals (K tac) + |> Datatype_Aux.split_conj_thm + end fun prove_permute_plus induct perm_defs perm_fns lthy = -let - val p = Free ("p", @{typ perm}) - val q = Free ("q", @{typ perm}) - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = Datatype_Prop.make_tnames perm_types + let + val p = Free ("p", @{typ perm}) + val q = Free ("q", @{typ perm}) + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = Datatype_Prop.make_tnames perm_types - fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq + fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) - val goals = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) + val goals = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) - val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 -in - Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) - |> Datatype_Aux.split_conj_thm -end + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 + in + Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + |> Datatype_Aux.split_conj_thm + end fun mk_perm_eq ty_perm_assoc cnstr = -let - fun lookup_perm p (ty, arg) = - case (AList.lookup (op=) ty_perm_assoc ty) of - SOME perm => perm $ p $ arg - | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg + let + fun lookup_perm p (ty, arg) = + case (AList.lookup (op=) ty_perm_assoc ty) of + SOME perm => perm $ p $ arg + | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg - val p = Free ("p", @{typ perm}) - val (arg_tys, ty) = - fastype_of cnstr - |> strip_type + val p = Free ("p", @{typ perm}) + val (arg_tys, ty) = + fastype_of cnstr + |> strip_type - val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) - val args = map Free (arg_names ~~ arg_tys) + val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val args = map Free (arg_names ~~ arg_tys) - val lhs = lookup_perm p (ty, list_comb (cnstr, args)) - val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) + val lhs = lookup_perm p (ty, list_comb (cnstr, args)) + val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) -in - (Attrib.empty_binding, eq) -end + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + in + (Attrib.empty_binding, eq) + end fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = -let - val perm_fn_names = full_ty_names - |> map Long_Name.base_name - |> map (prefix "permute_") + let + val perm_fn_names = full_ty_names + |> map Long_Name.base_name + |> map (prefix "permute_") - val perm_fn_types = map perm_ty tys - val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) - val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names + val perm_fn_types = map perm_ty tys + val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) + val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names - val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs + val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs - fun tac _ (_, _, simps) = - Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) + fun tac _ (_, _, simps) = + Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) - fun morphism phi (fvs, dfs, simps) = - (map (Morphism.term phi) fvs, - map (Morphism.thm phi) dfs, - map (Morphism.thm phi) simps); + fun morphism phi (fvs, dfs, simps) = + (map (Morphism.term phi) fvs, + map (Morphism.thm phi) dfs, + map (Morphism.thm phi) simps); - val ((perm_funs, perm_eq_thms), lthy') = - lthy - |> Local_Theory.exit_global - |> Class.instantiation (full_ty_names, tvs, @{sort pt}) - |> Primrec.add_primrec perm_fn_binds perm_eqs + val ((perm_funs, perm_eq_thms), lthy') = + lthy + |> Local_Theory.exit_global + |> Class.instantiation (full_ty_names, tvs, @{sort pt}) + |> Primrec.add_primrec perm_fn_binds perm_eqs - val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' - val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' -in - lthy' - |> Class.prove_instantiation_exit_result morphism tac - (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) - ||> Named_Target.theory_init -end + val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' + val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' + in + lthy' + |> Class.prove_instantiation_exit_result morphism tac + (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) + ||> Named_Target.theory_init + end end (* structure *)