# HG changeset patch # User Christian Urban # Date 1307304863 -3600 # Node ID 4bd584ff4fab57d34df7acf5224c438b6ec4f148 # Parent 8fe80e9f796dbfe7ba89159296197b755b236c06 added an option for an invariant (at the moment only a stub) diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun Jun 05 16:58:18 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Sun Jun 05 21:14:23 2011 +0100 @@ -35,6 +35,7 @@ and "sort_of (atom x) = sort_of (atom y)" shows "f x T = f y S" using assms apply - +thm Abs1_eq_iff' apply (subst (asm) Abs1_eq_iff') apply simp_all apply (elim conjE disjE) @@ -62,7 +63,7 @@ and fcb: "\x t r. atom x \ f3 x t r" begin -nominal_primrec +nominal_primrec f :: "lam \ ('a::pt)" where "f (Var x) = f1 x" @@ -92,7 +93,9 @@ end + thm test.f.simps +thm test.f.simps[simplified test_def] thm test_def diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Jun 05 16:58:18 2011 +0100 +++ b/Nominal/Nominal2.thy Sun Jun 05 21:14:23 2011 +0100 @@ -5,7 +5,8 @@ ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") ("nominal_induct.ML") - ("nominal_inductive.ML") + ("nominal_inductive.ML") + ("nominal_function_common.ML") ("nominal_function_core.ML") ("nominal_mutual.ML") ("nominal_function.ML") @@ -35,6 +36,7 @@ (***************************************) (* forked code of the function package *) (* for defining nominal functions *) +use "nominal_function_common.ML" use "nominal_function_core.ML" use "nominal_mutual.ML" use "nominal_function.ML" diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Sun Jun 05 16:58:18 2011 +0100 +++ b/Nominal/nominal_function.ML Sun Jun 05 21:14:23 2011 +0100 @@ -12,19 +12,19 @@ include FUNCTION_DATA val add_nominal_function: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> Function_Common.function_config -> + (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> local_theory -> info * local_theory val add_nominal_function_cmd: (binding * string option * mixfix) list -> - (Attrib.binding * string) list -> Function_Common.function_config -> + (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> (Proof.context -> tactic) -> local_theory -> info * local_theory val nominal_function: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> Function_Common.function_config -> + (Attrib.binding * term) list -> Nominal_Function_Common.nominal_function_config -> local_theory -> Proof.state val nominal_function_cmd: (binding * string option * mixfix) list -> - (Attrib.binding * string) list -> Function_Common.function_config -> + (Attrib.binding * string) list -> Nominal_Function_Common.nominal_function_config -> local_theory -> Proof.state val setup : theory -> theory @@ -38,8 +38,7 @@ struct open Function_Lib -open Function_Common - +open Nominal_Function_Common (* Check for all sorts of errors in the input - nominal needs a different checking function *) @@ -144,7 +143,7 @@ empty_preproc nominal_check_defs config ctxt' fixes spec (* nominal *) val defname = mk_defname fixes - val FunctionConfig {partials, default, ...} = config + val NominalFunctionConfig {partials, default, ...} = config val _ = if is_some default then Output.legacy_feature "'function (default)'. Use 'partial_function'." @@ -257,11 +256,28 @@ (* outer syntax *) +local + val option_parser = Parse.group "option" + ((Parse.reserved "sequential" >> K Sequential) + || ((Parse.reserved "default" |-- Parse.term) >> Default) + || (Parse.reserved "domintros" >> K DomIntros) + || (Parse.reserved "no_partials" >> K No_Partials) + || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) + + fun config_parser default = + (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) + >> (fn opts => fold apply_opt opts default) +in + fun nominal_function_parser default_cfg = + config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs +end + + (* nominal *) val _ = Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions" Keyword.thy_goal - (function_parser default_config + (nominal_function_parser nominal_default_config >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config)) diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/nominal_function_common.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_function_common.ML Sun Jun 05 21:14:23 2011 +0100 @@ -0,0 +1,361 @@ +(* Nominal Function Common + Author: Christian Urban + +Common definitions and other infrastructure for the function package. +*) + +signature FUNCTION_DATA = +sig + +type info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + simps : thm list option, + inducts : thm list option, + termination: thm} + +end + +structure Function_Data : FUNCTION_DATA = +struct + +type info = + {is_partial : bool, + defname : string, + (* contains no logical entities: invariant under morphisms: *) + add_simps : (binding -> binding) -> string -> (binding -> binding) -> + Attrib.src list -> thm list -> local_theory -> thm list * local_theory, + case_names : string list, + fs : term list, + R : term, + psimps: thm list, + pinducts: thm list, + simps : thm list option, + inducts : thm list option, + termination: thm} + +end + +structure Nominal_Function_Common = +struct + +open Function_Data + +local open Function_Lib in + +(* Profiling *) +val profile = Unsynchronized.ref false; + +fun PROFILE msg = if !profile then timeap_msg msg else I + + +val acc_const_name = @{const_name accp} +fun mk_acc domT R = + Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R + +val function_name = suffix "C" +val graph_name = suffix "_graph" +val rel_name = suffix "_rel" +val dom_name = suffix "_dom" + +(* Termination rules *) + +structure TerminationRule = Generic_Data +( + type T = thm list + val empty = [] + val extend = I + val merge = Thm.merge_thms +); + +val get_termination_rules = TerminationRule.get +val store_termination_rule = TerminationRule.map o cons +val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof + + +(* Function definition result data *) + +datatype function_result = FunctionResult of + {fs: term list, + G: term, + R: term, + psimps : thm list, + simple_pinducts : thm list, + cases : thm, + termination : thm, + domintros : thm list option} + +fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts, + simps, inducts, termination, defname, is_partial} : info) phi = + let + val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi + val name = Binding.name_of o Morphism.binding phi o Binding.name + in + { add_simps = add_simps, case_names = case_names, + fs = map term fs, R = term R, psimps = fact psimps, + pinducts = fact pinducts, simps = Option.map fact simps, + inducts = Option.map fact inducts, termination = thm termination, + defname = name defname, is_partial=is_partial } + end + +structure FunctionData = Generic_Data +( + type T = (term * info) Item_Net.T; + val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); + val extend = I; + fun merge tabs : T = Item_Net.merge tabs; +) + +val get_function = FunctionData.get o Context.Proof; + + +fun lift_morphism thy f = + let + val term = Drule.term_rule thy f + in + Morphism.thm_morphism f $> Morphism.term_morphism term + $> Morphism.typ_morphism (Logic.type_map term) + end + +fun import_function_data t ctxt = + let + val thy = Proof_Context.theory_of ctxt + val ct = cterm_of thy t + val inst_morph = lift_morphism thy o Thm.instantiate + + fun match (trm, data) = + SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) + handle Pattern.MATCH => NONE + in + get_first match (Item_Net.retrieve (get_function ctxt) t) + end + +fun import_last_function ctxt = + case Item_Net.content (get_function ctxt) of + [] => NONE + | (t, data) :: _ => + let + val ([t'], ctxt') = Variable.import_terms true [t] ctxt + in + import_function_data t' ctxt' + end + +val all_function_data = Item_Net.content o get_function + +fun add_function_data (data : info as {fs, termination, ...}) = + FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) + #> store_termination_rule termination + + +(* Simp rules for termination proofs *) + +structure Termination_Simps = Named_Thms +( + val name = "termination_simp" + val description = "simplification rules for termination proofs" +) + + +(* Default Termination Prover *) + +structure TerminationProver = Generic_Data +( + type T = Proof.context -> tactic + val empty = (fn _ => error "Termination prover not configured") + val extend = I + fun merge (a, _) = a +) + +val set_termination_prover = TerminationProver.put +val get_termination_prover = TerminationProver.get o Context.Proof + + +(* Configuration management *) +datatype nominal_function_opt + = Sequential + | Default of string + | DomIntros + | No_Partials + | Invariant of string + +datatype nominal_function_config = NominalFunctionConfig of + {sequential: bool, + default: string option, + domintros: bool, + partials: bool, + inv: string option} + +fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) = + NominalFunctionConfig + {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv} + | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) = + NominalFunctionConfig + {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv} + | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) = + NominalFunctionConfig + {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv} + | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) = + NominalFunctionConfig + {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv} + | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) = + NominalFunctionConfig + {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s} + +val nominal_default_config = + NominalFunctionConfig { sequential=false, default=NONE, + domintros=false, partials=true, inv=NONE} + + +(* Analyzing function equations *) + +fun split_def ctxt check_head geq = + let + fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] + val qs = Term.strip_qnt_vars "all" geq + val imp = Term.strip_qnt_body "all" geq + val (gs, eq) = Logic.strip_horn imp + + val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) + handle TERM _ => error (input_error "Not an equation") + + val (head, args) = strip_comb f_args + + val fname = fst (dest_Free head) handle TERM _ => "" + val _ = check_head fname + in + (fname, qs, gs, args, rhs) + end + +(* Check for all sorts of errors in the input *) +fun check_defs ctxt fixes eqs = + let + val fnames = map (fst o fst) fixes + + fun check geq = + let + fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) + + fun check_head fname = + member (op =) fnames fname orelse + input_error ("Illegal equation head. Expected " ^ commas_quote fnames) + + val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq + + val _ = length args > 0 orelse input_error "Function has no arguments:" + + fun add_bvs t is = add_loose_bnos (t, 0, is) + val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) + |> map (fst o nth (rev qs)) + + val _ = null rvs orelse input_error + ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ + " occur" ^ plural "s" "" rvs ^ " on right hand side only:") + + val _ = forall (not o Term.exists_subterm + (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) + orelse input_error "Defined function may not occur in premises or arguments" + + val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args + val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs + val _ = null funvars orelse (warning (cat_lines + ["Bound variable" ^ plural " " "s " funvars ^ + commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ + " in function position.", "Misspelled constructor???"]); true) + in + (fname, length args) + end + + val grouped_args = AList.group (op =) (map check eqs) + val _ = grouped_args + |> map (fn (fname, ars) => + length (distinct (op =) ars) = 1 + orelse error ("Function " ^ quote fname ^ + " has different numbers of arguments in different equations")) + + val not_defined = subtract (op =) (map fst grouped_args) fnames + val _ = null not_defined + orelse error ("No defining equations for function" ^ + plural " " "s " not_defined ^ commas_quote not_defined) + + fun check_sorts ((fname, fT), _) = + Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS) + orelse error (cat_lines + ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", + Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) + + val _ = map check_sorts fixes + in + () + end + +(* Preprocessors *) + +type fixes = ((string * typ) * mixfix) list +type 'a spec = (Attrib.binding * 'a list) list +type preproc = nominal_function_config -> Proof.context -> fixes -> term spec -> + (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) + +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o + HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all + +fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k + | mk_case_names _ n 0 = [] + | mk_case_names _ n 1 = [n] + | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) + +fun empty_preproc check _ ctxt fixes spec = + let + val (bnds, tss) = split_list spec + val ts = flat tss + val _ = check ctxt fixes ts + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts + + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) + (indices ~~ xs) |> map (map snd) + + (* using theorem names for case name currently disabled *) + val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat + in + (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) + end + +structure Preprocessor = Generic_Data +( + type T = preproc + val empty : T = empty_preproc check_defs + val extend = I + fun merge (a, _) = a +) + +val get_preproc = Preprocessor.get o Context.Proof +val set_preproc = Preprocessor.map o K + + + +local + val option_parser = Parse.group "option" + ((Parse.reserved "sequential" >> K Sequential) + || ((Parse.reserved "default" |-- Parse.term) >> Default) + || (Parse.reserved "domintros" >> K DomIntros) + || (Parse.reserved "no_partials" >> K No_Partials)) + + fun config_parser default = + (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) + >> (fn opts => fold apply_opt opts default) +in + fun function_parser default_cfg = + config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs +end + + +end +end diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Sun Jun 05 16:58:18 2011 +0100 +++ b/Nominal/nominal_function_core.ML Sun Jun 05 21:14:23 2011 +0100 @@ -11,14 +11,14 @@ sig val trace: bool Unsynchronized.ref - val prepare_nominal_function : Function_Common.function_config + val prepare_nominal_function : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((bstring * typ) * mixfix) list (* defined symbol *) -> ((bstring * typ) list * term list * term * term) list (* specification *) -> local_theory -> (term (* f *) * thm (* goalstate *) - * (thm -> Function_Common.function_result) (* continuation *) + * (thm -> Nominal_Function_Common.function_result) (* continuation *) ) * local_theory end @@ -33,7 +33,7 @@ val mk_eq = HOLogic.mk_eq open Function_Lib -open Function_Common +open Nominal_Function_Common datatype globals = Globals of {fvar: term, @@ -905,7 +905,7 @@ (* nominal *) fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = let - val FunctionConfig {domintros, default=default_opt, ...} = config + val NominalFunctionConfig {domintros, default=default_opt, ...} = config val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) val fvar = Free (fname, fT) diff -r 8fe80e9f796d -r 4bd584ff4fab Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Sun Jun 05 16:58:18 2011 +0100 +++ b/Nominal/nominal_mutual.ML Sun Jun 05 21:14:23 2011 +0100 @@ -11,13 +11,13 @@ signature NOMINAL_FUNCTION_MUTUAL = sig - val prepare_nominal_function_mutual : Function_Common.function_config + val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((string * typ) * mixfix) list -> term list -> local_theory -> ((thm (* goalstate *) - * (thm -> Function_Common.function_result) (* proof continuation *) + * (thm -> Nominal_Function_Common.function_result) (* proof continuation *) ) * local_theory) end @@ -27,7 +27,7 @@ struct open Function_Lib -open Function_Common +open Nominal_Function_Common type qgar = string * (string * typ) list * term list * term list * term