# HG changeset patch # User Christian Urban # Date 1305010026 -3600 # Node ID 542ff50555f515228851328b0d133c0bb2dde6f8 # Parent 2c6851248b3f8b9346d411700a4f4f1c80e4ad66 updated to new Isabelle (> 9 May) diff -r 2c6851248b3f -r 542ff50555f5 Nominal/Atoms.thy --- a/Nominal/Atoms.thy Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/Atoms.thy Tue May 10 07:47:06 2011 +0100 @@ -225,10 +225,12 @@ declare [[coercion "atom::var2\atom"]] +(* lemma fixes a::"var1" and b::"var2" shows "a \ t \ b \ t" oops +*) (* does not yet work: it needs image as coercion map *) diff -r 2c6851248b3f -r 542ff50555f5 Nominal/Ex/Datatypes.thy --- a/Nominal/Ex/Datatypes.thy Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/Ex/Datatypes.thy Tue May 10 07:47:06 2011 +0100 @@ -91,6 +91,8 @@ thm set_ty.size_eqvt thm set_ty.supp + + end diff -r 2c6851248b3f -r 542ff50555f5 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/Nominal2.thy Tue May 10 07:47:06 2011 +0100 @@ -323,19 +323,19 @@ val _ = trace_msg (K "Defining the quotient constants...") val qconstrs_descrs = - (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs + (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) (get_cnstrs dts) raw_constrs val qbns_descr = - map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns + map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx)) bn_funs raw_bns val qfvs_descr = map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs val qfv_bns_descr = - map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns + map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns val qalpha_bns_descr = - map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs alpha_bn_trms + map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs alpha_bn_trms val qperm_descr = map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs @@ -344,7 +344,7 @@ map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms val qperm_bn_descr = - map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns + map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_perm_bns val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8) = diff -r 2c6851248b3f -r 542ff50555f5 Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/Nominal2_Base.thy Tue May 10 07:47:06 2011 +0100 @@ -743,7 +743,6 @@ text {* provides perm_simp methods *} use "nominal_permeq.ML" -setup Nominal_Permeq.setup method_setup perm_simp = {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/nominal_function_core.ML Tue May 10 07:47:06 2011 +0100 @@ -540,10 +540,10 @@ fun requantify orig_intro thm = let val (qs, t) = dest_all_all orig_intro - val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T) - val vars = Term.add_vars (prop_of thm) [] |> rev + val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) + val vars = Term.add_vars (prop_of thm) [] val varmap = AList.lookup (op =) (frees ~~ map fst vars) - #> the_default ("",0) + #> the_default ("",0) in fold_rev (fn Free (n, T) => forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/nominal_induct.ML Tue May 10 07:47:06 2011 +0100 @@ -95,7 +95,7 @@ val finish_rule = split_all_tuples #> rename_params_rule true - (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding); + (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/nominal_mutual.ML Tue May 10 07:47:06 2011 +0100 @@ -118,10 +118,11 @@ fun convert_eqs (f, qs, gs, args, rhs) = let val MutualPart {i, i', ...} = get_part f parts + val rhs' = rhs + |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) in (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), - SumTree.mk_inj RST n' i' (replace_frees rews rhs) - |> Envir.beta_norm) + Envir.beta_norm (SumTree.mk_inj RST n' i' rhs')) end val qglrs = map convert_eqs fqgars diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_permeq.ML --- a/Nominal/nominal_permeq.ML Mon May 09 04:49:58 2011 +0100 +++ b/Nominal/nominal_permeq.ML Tue May 10 07:47:06 2011 +0100 @@ -26,7 +26,6 @@ val args_parser: (thm list * string list) context_parser val trace_eqvt: bool Config.T - val setup: theory -> theory end; (* @@ -95,7 +94,7 @@ (* tracing infrastructure *) -val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); +val trace_eqvt = Attrib.setup_config_bool @{binding "trace_eqvt"} (K false); fun trace_enabled ctxt = Config.get ctxt trace_eqvt @@ -211,10 +210,6 @@ fun eqvt_tac ctxt config = CONVERSION (eqvt_conv ctxt config) -(* setup of the configuration value *) -val setup = - trace_eqvt_setup - (** methods **) fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan