# HG changeset patch # User Christian Urban # Date 1278491640 -3600 # Node ID 4c58814559238e76a573f6f37ca31e6f96212090 # Parent a908ea36054fc11addbf213cc1028ae2bd4dc48a more on the paper diff -r a908ea36054f -r 4c5881455923 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri Jul 02 15:34:46 2010 +0100 +++ b/Nominal/NewParser.thy Wed Jul 07 09:34:00 2010 +0100 @@ -336,7 +336,7 @@ val _ = warning "Definition of raw fv-functions"; val lthy3 = Theory_Target.init NONE thy; - val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = + val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = if get_STEPS lthy3 > 2 then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 else raise TEST lthy3 @@ -370,7 +370,7 @@ val _ = warning "Proving equivariance"; val bn_eqvt = if get_STEPS lthy > 6 - then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 + then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 else raise TEST lthy4 (* noting the bn_eqvt lemmas in a temprorary theory *) @@ -437,25 +437,38 @@ val qtys = map #qtyp qty_infos (* defining of quotient term-constructors, binding functions, free vars functions *) - val qconstr_descr = + val _ = warning "Defining the quotient constnats" + val qconstrs_descr = flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs val qbns_descr = - map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs + map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns val qfvs_descr = - map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs + map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs + val qfv_bns_descr = + map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns - val (qs, lthy8) = + (* TODO: probably also needs alpha_bn *) + val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = if get_STEPS lthy > 15 - then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7 + then + lthy7 + |> qconst_defs qtys qconstrs_descr + ||>> qconst_defs qtys qbns_descr + ||>> qconst_defs qtys qfvs_descr + ||>> qconst_defs qtys qfv_bns_descr else raise TEST lthy7 - val _ = tracing ("raw fvs " ^ commas (map @{make_string} raw_fvs)) - val _ = tracing ("raw fv_bns " ^ commas (map @{make_string} raw_fv_bns)) + val qconstrs = map #qconst qconstrs_info + val qbns = map #qconst qbns_info + val qfvs = map #qconst qfvs_info + val qfv_bns = map #qconst qfv_bns_info + (* respectfulness proofs *) + (* HERE *) val _ = @@ -464,18 +477,10 @@ (* old stuff *) - val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); - val raw_consts = - flat (map (fn (i, (_, _, l)) => - map (fn (cname, dts) => - Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> - Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); - val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts - val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7; val _ = warning "Proving respects"; val bn_nos = map (fn (_, i, _) => i) raw_bn_info; - val bns = raw_bn_funs ~~ bn_nos; + val bns = raw_bns ~~ bn_nos; val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; val (bns_rsp_pre, lthy9) = fold_map ( @@ -504,27 +509,36 @@ let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] - const_rsp_tac) raw_consts lthy11a + const_rsp_tac) all_raw_constrs lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; + val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12; + val qfv_ts = map #qconst qfv_info + val qfv_defs = map #def qfv_info val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs - val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs - val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a; + val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns + val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a; + val qbn_ts = map #qconst qbn_info + val qbn_defs = map #def qbn_info val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms - val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b; + val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b; + val qalpha_bn_trms = map #qconst qalpha_info + val qalphabn_defs = map #def qalpha_info + val _ = warning "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs - val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy; + (* use Local_Theory.theory_result *) + val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; + val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; - val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; + val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); @@ -556,7 +570,7 @@ val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports"; - val supports = map (prove_supports lthy20 q_perm) consts; + val supports = map (prove_supports lthy20 q_perm) qconstrs; val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); val thy3 = Local_Theory.exit_global lthy20; val _ = warning "Instantiating FS"; diff -r a908ea36054f -r 4c5881455923 Nominal/Perm.thy --- a/Nominal/Perm.thy Fri Jul 02 15:34:46 2010 +0100 +++ b/Nominal/Perm.thy Wed Jul 07 09:34:00 2010 +0100 @@ -24,38 +24,4 @@ ML {* open Nominal_Dt_Quot *} -(* permutations for quotient types *) - -ML {* -fun quotient_lift_consts_export qtys spec ctxt = -let - val (result, ctxt') = fold_map (Quotient_Def.lift_raw_const qtys) spec ctxt; - val (ts_loc, defs_loc) = split_list (map (fn info => (#qconst info, #def info)) result); - val morphism = ProofContext.export_morphism ctxt' ctxt; - val ts = map (Morphism.term morphism) ts_loc - val defs = Morphism.fact morphism defs_loc -in - (ts, defs, ctxt') end -*} - - - -ML {* -fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = -let - val lthy = - Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; - val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy; - val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; - fun tac _ = - Class.intro_classes_tac [] THEN - (ALLGOALS (resolve_tac lifted_thms)) - val lthy'' = Class.prove_instantiation_instance tac lthy' -in - Local_Theory.exit_global lthy'' -end -*} - - -end diff -r a908ea36054f -r 4c5881455923 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Fri Jul 02 15:34:46 2010 +0100 +++ b/Nominal/nominal_dt_quot.ML Wed Jul 07 09:34:00 2010 +0100 @@ -12,6 +12,9 @@ val qconst_defs: typ list -> (string * term * mixfix) list -> local_theory -> Quotient_Info.qconsts_info list * local_theory + + val qperm_defs: typ list -> string list -> (string * term * mixfix) list -> + thm list -> theory -> theory end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -38,6 +41,21 @@ end +(* defines the quotient permutations *) +fun qperm_defs qtys full_tnames name_term_pairs thms thy = +let + val lthy = + Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; + val (_, lthy') = qconst_defs qtys name_term_pairs lthy; + val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; + fun tac _ = + Class.intro_classes_tac [] THEN + (ALLGOALS (resolve_tac lifted_thms)) + val lthy'' = Class.prove_instantiation_instance tac lthy' +in + Local_Theory.exit_global lthy'' +end + end (* structure *) diff -r a908ea36054f -r 4c5881455923 Paper/Paper.thy --- a/Paper/Paper.thy Fri Jul 02 15:34:46 2010 +0100 +++ b/Paper/Paper.thy Wed Jul 07 09:34:00 2010 +0100 @@ -90,7 +90,7 @@ we would like to regard the following two type-schemes as $\alpha$-equivalent % \begin{equation}\label{ex1} - @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. y \ x"} + @{text "\{x, y}. x \ y \\<^isub>\ \{y, x}. x \ y"} \end{equation} \noindent @@ -214,8 +214,8 @@ The scope of the binding is indicated by labels given to the types, for example @{text "s::trm"}, and a binding clause, in this case \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding - clause states to bind in @{text s} all the names the function @{text - "bn(as)"} returns. This style of specifying terms and bindings is heavily + clause states that all the names the function @{text + "bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. However, we will not be able to cope with all specifications that are @@ -358,7 +358,7 @@ about them in a theorem prover would be a major pain. \medskip \noindent - {\bf Contributions:} We provide novel definitions for when terms + {\bf Contributions:} We provide novel three definitions for when terms involving general binders are $\alpha$-equivalent. These definitions are inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic proofs, we establish a reasoning infrastructure for $\alpha$-equated @@ -366,7 +366,7 @@ conditions for $\alpha$-equated terms. We are also able to derive strong induction principles that have the variable convention already built in. The method behind our specification of general binders is taken - from the Ott-tool, but we introduce crucial restrictions, and also one extension, so + from the Ott-tool, but we introduce crucial restrictions, and also extensions, so that our specifications make sense for reasoning about $\alpha$-equated terms. @@ -1026,7 +1026,7 @@ \noindent In this specification the function @{text "bn"} determines which atoms of - @{text p} are bound in the argument @{text "t"}. Note that in the + the pattern @{text p} are bound in the argument @{text "t"}. Note that in the second-last @{text bn}-clause the function @{text "atom"} coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows us to treat binders of different atom type uniformly. @@ -1067,11 +1067,11 @@ \noindent The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms - inside the assignment. This difference has consequences for the free-variable - function and $\alpha$-equivalence relation. + inside the assignment. This difference has consequences for the associated + notions of free-variables and $\alpha$-equivalence. To make sure that variables bound by deep binders cannot be free at the - same time, we cannot have more than one binding function for one deep binder. + same time, we cannot have more than one binding function for a deep binder. Consequently we exclude specifications such as \begin{center} @@ -1090,9 +1090,9 @@ We also need to restrict the form of the binding functions in order to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated - terms. As a result we cannot return an atom in a binding function that is also - bound in the corresponding term-constructor. That means in the example - \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may + terms. The main restriction is that we cannot return an atom in a binding function that is also + bound in the corresponding term-constructor. That means in \eqref{letpat} + that the term-constructors @{text PVar} and @{text PTup} may not have a binding clause (all arguments are used to define @{text "bn"}). In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} may have a binding clause involving the argument @{text t} (the only one that @@ -1143,12 +1143,12 @@ term-constructors so that binders and their bodies are next to each other will result in inadequate representations in cases like @{text "Let x\<^isub>1=t\<^isub>1\x\<^isub>n=t\<^isub>n in s"}. Therefore we will first - extract datatype definitions from the specification and then define + extract ``raw'' datatype definitions from the specification and then define explicitly an $\alpha$-equivalence relation over them. We subsequently quotient the datatypes according to our $\alpha$-equivalence. - The datatype definition can be obtained by stripping off the + The ``raw'' datatype definition can be obtained by stripping off the binding clauses and the labels from the types. We also have to invent new names for the types @{text "ty\<^sup>\"} and term-constructors @{text "C\<^sup>\"} given by the user. In our implementation we just use the affix ``@{text "_raw"}''. @@ -1179,15 +1179,14 @@ The first non-trivial step we have to perform is the generation of free-variable functions from the specifications. For the - \emph{raw} types @{text "ty"}$_{1..n}$ extracted from a specification, - we define the free-variable functions + \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-variable functions % \begin{equation}\label{fvars} @{text "fv_ty\<^isub>1, \, fv_ty\<^isub>n"} \end{equation} \noindent - by recursion over the types @{text "ty"}$_{1..n}$. + by mutual recursion. We define these functions together with auxiliary free-variable functions for the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ we define @@ -1204,11 +1203,11 @@ While the idea behind these free-variable functions is clear (they just collect all atoms that are not bound), because of our rather complicated binding mechanisms their definitions are somewhat involved. Given - the term-constructor @{text "C"} of type @{text ty} and some associated + a term-constructor @{text "C"} of type @{text ty} and some associated binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text "fv_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text "fv(bc\<^isub>1) \ \ \ fv(bc\<^isub>k)"} where we define below what @{text "fv"} of a binding - clause with mode \isacommand{bin\_set} means (similarly for the other modes). + clause means. We only show the mode \isacommand{bind\_set} (the other modes are similar). Suppose the binding clause @{text bc\<^isub>i} is of the form % \begin{equation} @@ -1239,7 +1238,7 @@ \noindent whereby the functions @{text "fv_ty\<^isub>i"} are the ones we are defining by recursion (see \eqref{fvars}) provided the @{text "d\<^isub>i"} refers to one of the raw types - @{text "ty"}$_{1..n}$ from a specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. + @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}. In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions for atom types to which shallow binders have to refer %