# HG changeset patch # User wenzelm # Date 1436185623 -7200 # Node ID 143ac4d9504af0dd348751127387f2b32da9f61b # Parent 03a25d3e759e5e0d92158d8d907378df74ce0365# Parent deaf10a6bdad51a98edef378cbb9c468e9226c3e merged diff -r 03a25d3e759e -r 143ac4d9504a NEWS --- a/NEWS Fri Jul 03 10:17:29 2015 +0200 +++ b/NEWS Mon Jul 06 14:27:03 2015 +0200 @@ -234,6 +234,12 @@ command. Minor INCOMPATIBILITY, use 'function' instead. +** ML ** + +* Thm.instantiate (and derivatives) no longer require the LHS of the +instantiation to be certified: plain variables are given directly. + + New in Isabelle2015 (May 2015) ------------------------------ diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Mon Jul 06 14:27:03 2015 +0200 @@ -656,7 +656,8 @@ @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ - @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ + @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + -> thm -> thm"} \\ @{index_ML Thm.add_axiom: "Proof.context -> binding * term -> theory -> (string * thm) * theory"} \\ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Doc/Implementation/Proof.thy Mon Jul 06 14:27:03 2015 +0200 @@ -108,7 +108,7 @@ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> - (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\ + ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\ @{index_ML Variable.focus: "term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context"} \\ \end{mldecls} diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jul 06 14:27:03 2015 +0200 @@ -1,8 +1,14 @@ theory HOL_Specific -imports Base "~~/src/HOL/Library/Old_Datatype" "~~/src/HOL/Library/Old_Recdef" - "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/FSet" +imports + Base + "~~/src/HOL/Library/Old_Datatype" + "~~/src/HOL/Library/Old_Recdef" + "~~/src/Tools/Adhoc_Overloading" + "~~/src/HOL/Library/Dlist" + "~~/src/HOL/Library/FSet" begin + chapter \Higher-Order Logic\ text \Isabelle/HOL is based on Higher-Order Logic, a polymorphic @@ -52,9 +58,7 @@ nicely, but they also mean that HOL requires some sophistication from the user. In particular, an understanding of Hindley-Milner type-inference with type-classes, which are both used extensively in - the standard libraries and applications. Beginners can set - @{attribute show_types} or even @{attribute show_sorts} to get more - explicit information about the result of type-inference.\ + the standard libraries and applications.\ chapter \Derived specification elements\ @@ -171,12 +175,10 @@ \end{description} - When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are - defined simultaneously, the list of introduction rules is called - @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the case analysis rules are - called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the list - of mutual induction rules is called @{text - "R\<^sub>1_\_R\<^sub>n.inducts"}. + When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are defined simultaneously, + the list of introduction rules is called @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the + case analysis rules are called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the + list of mutual induction rules is called @{text "R\<^sub>1_\_R\<^sub>n.inducts"}. \ @@ -236,8 +238,8 @@ (*<*)end(*>*) text \Common logical connectives can be easily characterized as -non-recursive inductive definitions with parameters, but without -arguments.\ + non-recursive inductive definitions with parameters, but without + arguments.\ (*<*)experiment begin(*>*) inductive AND for A B :: bool @@ -251,12 +253,12 @@ where "B a \ EXISTS B" (*<*)end(*>*) -text \Here the @{text "cases"} or @{text "induct"} rules produced by - the @{command inductive} package coincide with the expected - elimination rules for Natural Deduction. Already in the original - article by Gerhard Gentzen @{cite "Gentzen:1935"} there is a hint that - each connective can be characterized by its introductions, and the - elimination can be constructed systematically.\ +text \Here the @{text "cases"} or @{text "induct"} rules produced by the + @{command inductive} package coincide with the expected elimination rules + for Natural Deduction. Already in the original article by Gerhard Gentzen + @{cite "Gentzen:1935"} there is a hint that each connective can be + characterized by its introductions, and the elimination can be constructed + systematically.\ section \Recursive functions \label{sec:recursion}\ @@ -288,101 +290,98 @@ \begin{description} - \item @{command (HOL) "primrec"} defines primitive recursive - functions over datatypes (see also @{command_ref (HOL) datatype}). - The given @{text equations} specify reduction rules that are produced - by instantiating the generic combinator for primitive recursion that - is available for each datatype. + \item @{command (HOL) "primrec"} defines primitive recursive functions + over datatypes (see also @{command_ref (HOL) datatype}). The given @{text + equations} specify reduction rules that are produced by instantiating the + generic combinator for primitive recursion that is available for each + datatype. Each equation needs to be of the form: @{text [display] "f x\<^sub>1 \ x\<^sub>m (C y\<^sub>1 \ y\<^sub>k) z\<^sub>1 \ z\<^sub>n = rhs"} - such that @{text C} is a datatype constructor, @{text rhs} contains - only the free variables on the left-hand side (or from the context), - and all recursive occurrences of @{text "f"} in @{text "rhs"} are of - the form @{text "f \ y\<^sub>i \"} for some @{text i}. At most one - reduction rule for each constructor can be given. The order does - not matter. For missing constructors, the function is defined to - return a default value, but this equation is made difficult to - access for users. - - The reduction rules are declared as @{attribute simp} by default, - which enables standard proof methods like @{method simp} and - @{method auto} to normalize expressions of @{text "f"} applied to - datatype constructions, by simulating symbolic computation via - rewriting. - - \item @{command (HOL) "function"} defines functions by general - wellfounded recursion. A detailed description with examples can be - found in @{cite "isabelle-function"}. The function is specified by a - set of (possibly conditional) recursive equations with arbitrary - pattern matching. The command generates proof obligations for the - completeness and the compatibility of patterns. + such that @{text C} is a datatype constructor, @{text rhs} contains only + the free variables on the left-hand side (or from the context), and all + recursive occurrences of @{text "f"} in @{text "rhs"} are of the form + @{text "f \ y\<^sub>i \"} for some @{text i}. At most one reduction rule for + each constructor can be given. The order does not matter. For missing + constructors, the function is defined to return a default value, but this + equation is made difficult to access for users. + + The reduction rules are declared as @{attribute simp} by default, which + enables standard proof methods like @{method simp} and @{method auto} to + normalize expressions of @{text "f"} applied to datatype constructions, by + simulating symbolic computation via rewriting. + + \item @{command (HOL) "function"} defines functions by general wellfounded + recursion. A detailed description with examples can be found in @{cite + "isabelle-function"}. The function is specified by a set of (possibly + conditional) recursive equations with arbitrary pattern matching. The + command generates proof obligations for the completeness and the + compatibility of patterns. The defined function is considered partial, and the resulting - simplification rules (named @{text "f.psimps"}) and induction rule - (named @{text "f.pinduct"}) are guarded by a generated domain - predicate @{text "f_dom"}. The @{command (HOL) "termination"} - command can then be used to establish that the function is total. - - \item @{command (HOL) "fun"} is a shorthand notation for ``@{command - (HOL) "function"}~@{text "(sequential)"}'', followed by automated - proof attempts regarding pattern matching and termination. See - @{cite "isabelle-function"} for further details. - - \item @{command (HOL) "termination"}~@{text f} commences a - termination proof for the previously defined function @{text f}. If - this is omitted, the command refers to the most recent function - definition. After the proof is closed, the recursive equations and - the induction principle is established. - - \item @{command (HOL) "fun_cases"} generates specialized elimination - rules for function equations. It expects one or more function equations - and produces rules that eliminate the given equalities, following the cases + simplification rules (named @{text "f.psimps"}) and induction rule (named + @{text "f.pinduct"}) are guarded by a generated domain predicate @{text + "f_dom"}. The @{command (HOL) "termination"} command can then be used to + establish that the function is total. + + \item @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL) + "function"}~@{text "(sequential)"}'', followed by automated proof attempts + regarding pattern matching and termination. See @{cite + "isabelle-function"} for further details. + + \item @{command (HOL) "termination"}~@{text f} commences a termination + proof for the previously defined function @{text f}. If this is omitted, + the command refers to the most recent function definition. After the proof + is closed, the recursive equations and the induction principle is + established. + + \item @{command (HOL) "fun_cases"} generates specialized elimination rules + for function equations. It expects one or more function equations and + produces rules that eliminate the given equalities, following the cases given in the function definition. + \end{description} Recursive definitions introduced by the @{command (HOL) "function"} - command accommodate reasoning by induction (cf.\ @{method induct}): - rule @{text "f.induct"} refers to a specific induction rule, with - parameters named according to the user-specified equations. Cases - are numbered starting from 1. For @{command (HOL) "primrec"}, the - induction principle coincides with structural recursion on the - datatype where the recursion is carried out. - - The equations provided by these packages may be referred later as - theorem list @{text "f.simps"}, where @{text f} is the (collective) - name of the functions defined. Individual equations may be named - explicitly as well. - - The @{command (HOL) "function"} command accepts the following - options. + command accommodate reasoning by induction (cf.\ @{method induct}): rule + @{text "f.induct"} refers to a specific induction rule, with parameters + named according to the user-specified equations. Cases are numbered + starting from 1. For @{command (HOL) "primrec"}, the induction principle + coincides with structural recursion on the datatype where the recursion is + carried out. + + The equations provided by these packages may be referred later as theorem + list @{text "f.simps"}, where @{text f} is the (collective) name of the + functions defined. Individual equations may be named explicitly as well. + + The @{command (HOL) "function"} command accepts the following options. \begin{description} \item @{text sequential} enables a preprocessor which disambiguates - overlapping patterns by making them mutually disjoint. Earlier - equations take precedence over later ones. This allows to give the - specification in a format very similar to functional programming. - Note that the resulting simplification and induction rules - correspond to the transformed specification, not the one given - originally. This usually means that each equation given by the user - may result in several theorems. Also note that this automatic - transformation only works for ML-style datatype patterns. - - \item @{text domintros} enables the automated generation of - introduction rules for the domain predicate. While mostly not - needed, they can be helpful in some proofs about partial functions. + overlapping patterns by making them mutually disjoint. Earlier equations + take precedence over later ones. This allows to give the specification in + a format very similar to functional programming. Note that the resulting + simplification and induction rules correspond to the transformed + specification, not the one given originally. This usually means that each + equation given by the user may result in several theorems. Also note that + this automatic transformation only works for ML-style datatype patterns. + + \item @{text domintros} enables the automated generation of introduction + rules for the domain predicate. While mostly not needed, they can be + helpful in some proofs about partial functions. \end{description} \ + subsubsection \Example: evaluation of expressions\ -text \Subsequently, we define mutual datatypes for arithmetic and - boolean expressions, and use @{command primrec} for evaluation - functions that follow the same recursive structure.\ +text \Subsequently, we define mutual datatypes for arithmetic and boolean + expressions, and use @{command primrec} for evaluation functions that + follow the same recursive structure.\ (*<*)experiment begin(*>*) datatype 'a aexp = @@ -413,13 +412,13 @@ text \Since the value of an expression depends on the value of its variables, the functions @{const evala} and @{const evalb} take an - additional parameter, an \emph{environment} that maps variables to - their values. - - \medskip Substitution on expressions can be defined similarly. The - mapping @{text f} of type @{typ "'a \ 'a aexp"} given as a - parameter is lifted canonically on the types @{typ "'a aexp"} and - @{typ "'a bexp"}, respectively. + additional parameter, an \emph{environment} that maps variables to their + values. + + \medskip Substitution on expressions can be defined similarly. The mapping + @{text f} of type @{typ "'a \ 'a aexp"} given as a parameter is lifted + canonically on the types @{typ "'a aexp"} and @{typ "'a bexp"}, + respectively. \ primrec substa :: "('a \ 'b aexp) \ 'a aexp \ 'b aexp" @@ -434,10 +433,10 @@ | "substb f (And b1 b2) = And (substb f b1) (substb f b2)" | "substb f (Neg b) = Neg (substb f b)" -text \In textbooks about semantics one often finds substitution - theorems, which express the relationship between substitution and - evaluation. For @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove - such a theorem by mutual induction, followed by simplification. +text \In textbooks about semantics one often finds substitution theorems, + which express the relationship between substitution and evaluation. For + @{typ "'a aexp"} and @{typ "'a bexp"}, we can prove such a theorem by + mutual induction, followed by simplification. \ lemma subst_one: @@ -487,9 +486,8 @@ subsubsection \Example: a map function for infinitely branching trees\ -text \Defining functions on infinitely branching datatypes by - primitive recursion is just as easy. -\ +text \Defining functions on infinitely branching datatypes by primitive + recursion is just as easy.\ (*<*)experiment begin(*>*) datatype 'a tree = Atom 'a | Branch "nat \ 'a tree" @@ -499,11 +497,12 @@ "map_tree f (Atom a) = Atom (f a)" | "map_tree f (Branch ts) = Branch (\x. map_tree f (ts x))" -text \Note that all occurrences of functions such as @{text ts} - above must be applied to an argument. In particular, @{term - "map_tree f \ ts"} is not allowed here.\ - -text \Here is a simple composition lemma for @{term map_tree}:\ +text \Note that all occurrences of functions such as @{text ts} above must + be applied to an argument. In particular, @{term "map_tree f \ ts"} is not + allowed here. + + \medskip Here is a simple composition lemma for @{term map_tree}: +\ lemma "map_tree g (map_tree f t) = map_tree (g \ f) t" by (induct t) simp_all @@ -645,7 +644,6 @@ definitions. \end{description} - \ @@ -701,6 +699,80 @@ \ +section \Adhoc overloading of constants\ + +text \ + \begin{tabular}{rcll} + @{command_def "adhoc_overloading"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \ local_theory"} \\ + @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text false} \\ + \end{tabular} + + \medskip + + Adhoc overloading allows to overload a constant depending on + its type. Typically this involves the introduction of an + uninterpreted constant (used for input and output) and the addition + of some variants (used internally). For examples see + @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and + @{file "~~/src/HOL/Library/Monad_Syntax.thy"}. + + @{rail \ + (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) + (@{syntax nameref} (@{syntax term} + ) + @'and') + \} + + \begin{description} + + \item @{command "adhoc_overloading"}~@{text "c v\<^sub>1 ... v\<^sub>n"} + associates variants with an existing constant. + + \item @{command "no_adhoc_overloading"} is similar to + @{command "adhoc_overloading"}, but removes the specified variants + from the present context. + + \item @{attribute "show_variants"} controls printing of variants + of overloaded constants. If enabled, the internally used variants + are printed instead of their respective overloaded constants. This + is occasionally useful to check whether the system agrees with a + user's expectations about derived variants. + + \end{description} +\ + + +section \Definition by specification \label{sec:hol-specification}\ + +text \ + \begin{matharray}{rcl} + @{command_def (HOL) "specification"} & : & @{text "theory \ proof(prove)"} \\ + \end{matharray} + + @{rail \ + @@{command (HOL) specification} '(' (decl +) ')' \ + (@{syntax thmdecl}? @{syntax prop} +) + ; + decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')? + \} + + \begin{description} + + \item @{command (HOL) "specification"}~@{text "decls \"} sets up a + goal stating the existence of terms with the properties specified to + hold for the constants given in @{text decls}. After finishing the + proof, the theory will be augmented with definitions for the given + constants, as well as with theorems stating the properties for these + constants. + + @{text decl} declares a constant to be defined by the + specification given. The definition for the constant @{text c} is + bound to the name @{text c_def} unless a theorem name is given in + the declaration. Overloaded constants should be declared as such. + + \end{description} +\ + + section \Old-style datatypes \label{sec:hol-datatype}\ text \ @@ -745,9 +817,8 @@ subsubsection \Examples\ -text \We define a type of finite sequences, with slightly different - names than the existing @{typ "'a list"} that is already in @{theory - Main}:\ +text \We define a type of finite sequences, with slightly different names + than the existing @{typ "'a list"} that is already in @{theory Main}:\ (*<*)experiment begin(*>*) datatype 'a seq = Empty | Seq 'a "'a seq" @@ -902,33 +973,30 @@ subsection \Record operations\ -text \ - Any record definition of the form presented above produces certain - standard operations. Selectors and updates are provided for any - field, including the improper one ``@{text more}''. There are also - cumulative record constructor functions. To simplify the - presentation below, we assume for now that @{text "(\\<^sub>1, \, - \\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: - \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. - - \medskip \textbf{Selectors} and \textbf{updates} are available for - any field (including ``@{text more}''): +text \Any record definition of the form presented above produces certain + standard operations. Selectors and updates are provided for any field, + including the improper one ``@{text more}''. There are also cumulative + record constructor functions. To simplify the presentation below, we + assume for now that @{text "(\\<^sub>1, \, \\<^sub>m) t"} is a root record with fields + @{text "c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. + + \medskip \textbf{Selectors} and \textbf{updates} are available for any + field (including ``@{text more}''): \begin{matharray}{lll} @{text "c\<^sub>i"} & @{text "::"} & @{text "\\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^sub>i"} \\ @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ \\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^vec>c :: \<^vec>\, \ :: \\"} \\ \end{matharray} - There is special syntax for application of updates: @{text "r\x := - a\"} abbreviates term @{text "x_update a r"}. Further notation for - repeated updates is also available: @{text "r\x := a\\y := b\\z := - c\"} may be written @{text "r\x := a, y := b, z := c\"}. Note that - because of postfix notation the order of fields shown here is - reverse than in the actual term. Since repeated updates are just - function applications, fields may be freely permuted in @{text "\x - := a, y := b, z := c\"}, as far as logical equality is concerned. - Thus commutativity of independent updates can be proven within the - logic for any two fields, but not as a general theorem. + There is special syntax for application of updates: @{text "r\x := a\"} + abbreviates term @{text "x_update a r"}. Further notation for repeated + updates is also available: @{text "r\x := a\\y := b\\z := c\"} may be + written @{text "r\x := a, y := b, z := c\"}. Note that because of postfix + notation the order of fields shown here is reverse than in the actual + term. Since repeated updates are just function applications, fields may be + freely permuted in @{text "\x := a, y := b, z := c\"}, as far as logical + equality is concerned. Thus commutativity of independent updates can be + proven within the logic for any two fields, but not as a general theorem. \medskip The \textbf{make} operation provides a cumulative record constructor function: @@ -937,15 +1005,14 @@ @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ \end{matharray} - \medskip We now reconsider the case of non-root records, which are - derived of some parent. In general, the latter may depend on - another parent as well, resulting in a list of \emph{ancestor - records}. Appending the lists of fields of all ancestors results in - a certain field prefix. The record package automatically takes care - of this by lifting operations over this context of ancestor fields. - Assuming that @{text "(\\<^sub>1, \, \\<^sub>m) t"} has ancestor - fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, - the above record operations will get the following types: + \medskip We now reconsider the case of non-root records, which are derived + of some parent. In general, the latter may depend on another parent as + well, resulting in a list of \emph{ancestor records}. Appending the lists + of fields of all ancestors results in a certain field prefix. The record + package automatically takes care of this by lifting operations over this + context of ancestor fields. Assuming that @{text "(\\<^sub>1, \, \\<^sub>m) t"} has + ancestor fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, the above record + operations will get the following types: \medskip \begin{tabular}{lll} @@ -959,11 +1026,11 @@ \medskip \noindent Some further operations address the extension aspect of a - derived record scheme specifically: @{text "t.fields"} produces a - record fragment consisting of exactly the new fields introduced here - (the result may serve as a more part elsewhere); @{text "t.extend"} - takes a fixed record and adds a given more part; @{text - "t.truncate"} restricts a record scheme to a fixed record. + derived record scheme specifically: @{text "t.fields"} produces a record + fragment consisting of exactly the new fields introduced here (the result + may serve as a more part elsewhere); @{text "t.extend"} takes a fixed + record and adds a given more part; @{text "t.truncate"} restricts a record + scheme to a fixed record. \medskip \begin{tabular}{lll} @@ -974,8 +1041,8 @@ \end{tabular} \medskip - \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide - for root records. + \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide for + root records. \ @@ -989,41 +1056,40 @@ \begin{enumerate} - \item Standard conversions for selectors or updates applied to - record constructor terms are made part of the default Simplifier - context; thus proofs by reduction of basic operations merely require - the @{method simp} method without further arguments. These rules - are available as @{text "t.simps"}, too. - - \item Selectors applied to updated records are automatically reduced - by an internal simplification procedure, which is also part of the - standard Simplifier setup. - - \item Inject equations of a form analogous to @{prop "(x, y) = (x', - y') \ x = x' \ y = y'"} are declared to the Simplifier and Classical - Reasoner as @{attribute iff} rules. These rules are available as - @{text "t.iffs"}. - - \item The introduction rule for record equality analogous to @{text - "x r = x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, - and as the basic rule context as ``@{attribute intro}@{text "?"}''. - The rule is called @{text "t.equality"}. + \item Standard conversions for selectors or updates applied to record + constructor terms are made part of the default Simplifier context; thus + proofs by reduction of basic operations merely require the @{method simp} + method without further arguments. These rules are available as @{text + "t.simps"}, too. + + \item Selectors applied to updated records are automatically reduced by an + internal simplification procedure, which is also part of the standard + Simplifier setup. + + \item Inject equations of a form analogous to @{prop "(x, y) = (x', y') \ + x = x' \ y = y'"} are declared to the Simplifier and Classical Reasoner as + @{attribute iff} rules. These rules are available as @{text "t.iffs"}. + + \item The introduction rule for record equality analogous to @{text "x r = + x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, and as the + basic rule context as ``@{attribute intro}@{text "?"}''. The rule is + called @{text "t.equality"}. \item Representations of arbitrary record expressions as canonical constructor terms are provided both in @{method cases} and @{method induct} format (cf.\ the generic proof methods of the same name, - \secref{sec:cases-induct}). Several variations are available, for - fixed records, record schemes, more parts etc. - - The generic proof methods are sufficiently smart to pick the most - sensible rule according to the type of the indicated record - expression: users just need to apply something like ``@{text "(cases - r)"}'' to a certain proof problem. - - \item The derived record operations @{text "t.make"}, @{text - "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} - treated automatically, but usually need to be expanded by hand, - using the collective fact @{text "t.defs"}. + \secref{sec:cases-induct}). Several variations are available, for fixed + records, record schemes, more parts etc. + + The generic proof methods are sufficiently smart to pick the most sensible + rule according to the type of the indicated record expression: users just + need to apply something like ``@{text "(cases r)"}'' to a certain proof + problem. + + \item The derived record operations @{text "t.make"}, @{text "t.fields"}, + @{text "t.extend"}, @{text "t.truncate"} are \emph{not} treated + automatically, but usually need to be expanded by hand, using the + collective fact @{text "t.defs"}. \end{enumerate} \ @@ -1033,6 +1099,7 @@ text \See @{file "~~/src/HOL/ex/Records.thy"}, for example.\ + section \Typedef axiomatization \label{sec:hol-typedef}\ text \ @@ -1187,30 +1254,28 @@ \begin{description} - \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to - prove and register properties about the functorial structure of type - constructors. These properties then can be used by other packages - to deal with those type constructors in certain type constructions. - Characteristic theorems are noted in the current local theory. By - default, they are prefixed with the base name of the type - constructor, an explicit prefix can be given alternatively. + \item @{command (HOL) "functor"}~@{text "prefix: m"} allows to prove and + register properties about the functorial structure of type constructors. + These properties then can be used by other packages to deal with those + type constructors in certain type constructions. Characteristic theorems + are noted in the current local theory. By default, they are prefixed with + the base name of the type constructor, an explicit prefix can be given + alternatively. The given term @{text "m"} is considered as \emph{mapper} for the - corresponding type constructor and must conform to the following - type pattern: + corresponding type constructor and must conform to the following type + pattern: \begin{matharray}{lll} @{text "m"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>k \ (\<^vec>\\<^sub>n) t \ (\<^vec>\\<^sub>n) t"} \\ \end{matharray} - \noindent where @{text t} is the type constructor, @{text - "\<^vec>\\<^sub>n"} and @{text "\<^vec>\\<^sub>n"} are distinct - type variables free in the local theory and @{text "\\<^sub>1"}, - \ldots, @{text "\\<^sub>k"} is a subsequence of @{text "\\<^sub>1 \ - \\<^sub>1"}, @{text "\\<^sub>1 \ \\<^sub>1"}, \ldots, - @{text "\\<^sub>n \ \\<^sub>n"}, @{text "\\<^sub>n \ - \\<^sub>n"}. + \noindent where @{text t} is the type constructor, @{text "\<^vec>\\<^sub>n"} + and @{text "\<^vec>\\<^sub>n"} are distinct type variables free in the local + theory and @{text "\\<^sub>1"}, \ldots, @{text "\\<^sub>k"} is a subsequence of @{text + "\\<^sub>1 \ \\<^sub>1"}, @{text "\\<^sub>1 \ \\<^sub>1"}, \ldots, @{text "\\<^sub>n \ \\<^sub>n"}, @{text + "\\<^sub>n \ \\<^sub>n"}. \end{description} \ @@ -1240,29 +1305,28 @@ @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\ \end{matharray} - The quotient package defines a new quotient type given a raw type - and a partial equivalence relation. The package also historically - includes automation for transporting definitions and theorems. - But most of this automation was superseded by the Lifting and Transfer - packages. The user should consider using these two new packages for - lifting definitions and transporting theorems. + The quotient package defines a new quotient type given a raw type and a + partial equivalence relation. The package also historically includes + automation for transporting definitions and theorems. But most of this + automation was superseded by the Lifting (\secref{sec:lifting}) and + Transfer (\secref{sec:transfer}) packages. The user should consider using + these two new packages for lifting definitions and transporting theorems. @{rail \ - @@{command (HOL) quotient_type} (spec) + @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '=' + quot_type \ quot_morphisms? quot_parametric? + ; + quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term} ; - spec: @{syntax typespec} @{syntax mixfix}? '=' \ - @{syntax type} '/' ('partial' ':')? @{syntax term} \ - (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})? - \} - - @{rail \ + quot_morphisms: @'morphisms' @{syntax name} @{syntax name} + ; + quot_parametric: @'parametric' @{syntax thmref} + ; @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \ @{syntax term} 'is' @{syntax term} ; constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? - \} - - @{rail \ + ; @@{method (HOL) lifting} @{syntax thmrefs}? ; @@{method (HOL) lifting_setup} @{syntax thmrefs}? @@ -1270,175 +1334,92 @@ \begin{description} - \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \}. The - injection from a quotient type to a raw type is called @{text + \item @{command (HOL) "quotient_type"} defines a new quotient type @{text + \}. The injection from a quotient type to a raw type is called @{text rep_\}, its inverse @{text abs_\} unless explicit @{keyword (HOL) - "morphisms"} specification provides alternative names. @{command - (HOL) "quotient_type"} requires the user to prove that the relation - is an equivalence relation (predicate @{text equivp}), unless the - user specifies explicitly @{text partial} in which case the - obligation is @{text part_equivp}. A quotient defined with @{text - partial} is weaker in the sense that less things can be proved - automatically. + "morphisms"} specification provides alternative names. @{command (HOL) + "quotient_type"} requires the user to prove that the relation is an + equivalence relation (predicate @{text equivp}), unless the user specifies + explicitly @{text partial} in which case the obligation is @{text + part_equivp}. A quotient defined with @{text partial} is weaker in the + sense that less things can be proved automatically. The command internally proves a Quotient theorem and sets up the Lifting - package by the command @{command (HOL) setup_lifting}. Thus the Lifting + package by the command @{command (HOL) setup_lifting}. Thus the Lifting and Transfer packages can be used also with quotient types defined by - @{command (HOL) "quotient_type"} without any extra set-up. The parametricity - theorem for the equivalence relation R can be provided as an extra argument - of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}. - This theorem allows the Lifting package to generate a stronger transfer rule for equality. - + @{command (HOL) "quotient_type"} without any extra set-up. The + parametricity theorem for the equivalence relation R can be provided as an + extra argument of the command and is passed to the corresponding internal + call of @{command (HOL) setup_lifting}. This theorem allows the Lifting + package to generate a stronger transfer rule for equality. + \end{description} - The most of the rest of the package was superseded by the Lifting and Transfer - packages. The user should consider using these two new packages for - lifting definitions and transporting theorems. - - \begin{description} - - \item @{command (HOL) "quotient_definition"} defines a constant on - the quotient type. - - \item @{command (HOL) "print_quotmapsQ3"} prints quotient map - functions. + Most of the rest of the package was superseded by the Lifting + (\secref{sec:lifting}) and Transfer (\secref{sec:transfer}) packages. + + \begin{description} + + \item @{command (HOL) "quotient_definition"} defines a constant on the + quotient type. + + \item @{command (HOL) "print_quotmapsQ3"} prints quotient map functions. \item @{command (HOL) "print_quotientsQ3"} prints quotients. \item @{command (HOL) "print_quotconsts"} prints quotient constants. \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} - methods match the current goal with the given raw theorem to be - lifted producing three new subgoals: regularization, injection and - cleaning subgoals. @{method (HOL) "lifting"} tries to apply the - heuristics for automatically solving these three subgoals and - leaves only the subgoals unsolved by the heuristics to the user as - opposed to @{method (HOL) "lifting_setup"} which leaves the three - subgoals unsolved. - - \item @{method (HOL) "descending"} and @{method (HOL) - "descending_setup"} try to guess a raw statement that would lift - to the current subgoal. Such statement is assumed as a new subgoal - and @{method (HOL) "descending"} continues in the same way as - @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries - to solve the arising regularization, injection and cleaning - subgoals with the analogous method @{method (HOL) - "descending_setup"} which leaves the four unsolved subgoals. + methods match the current goal with the given raw theorem to be lifted + producing three new subgoals: regularization, injection and cleaning + subgoals. @{method (HOL) "lifting"} tries to apply the heuristics for + automatically solving these three subgoals and leaves only the subgoals + unsolved by the heuristics to the user as opposed to @{method (HOL) + "lifting_setup"} which leaves the three subgoals unsolved. + + \item @{method (HOL) "descending"} and @{method (HOL) "descending_setup"} + try to guess a raw statement that would lift to the current subgoal. Such + statement is assumed as a new subgoal and @{method (HOL) "descending"} + continues in the same way as @{method (HOL) "lifting"} does. @{method + (HOL) "descending"} tries to solve the arising regularization, injection + and cleaning subgoals with the analogous method @{method (HOL) + "descending_setup"} which leaves the four unsolved subgoals. \item @{method (HOL) "partiality_descending"} finds the regularized - theorem that would lift to the current subgoal, lifts it and - leaves as a subgoal. This method can be used with partial - equivalence quotients where the non regularized statements would - not be true. @{method (HOL) "partiality_descending_setup"} leaves - the injection and cleaning subgoals unchanged. - - \item @{method (HOL) "regularize"} applies the regularization - heuristics to the current subgoal. - - \item @{method (HOL) "injection"} applies the injection heuristics - to the current goal using the stored quotient respectfulness - theorems. - - \item @{method (HOL) "cleaning"} applies the injection cleaning - heuristics to the current subgoal using the stored quotient - preservation theorems. - - \item @{attribute (HOL) quot_lifted} attribute tries to - automatically transport the theorem to the quotient type. - The attribute uses all the defined quotients types and quotient - constants often producing undesired results or theorems that - cannot be lifted. - - \item @{attribute (HOL) quot_respect} and @{attribute (HOL) - quot_preserve} attributes declare a theorem as a respectfulness - and preservation theorem respectively. These are stored in the - local theory store and used by the @{method (HOL) "injection"} - and @{method (HOL) "cleaning"} methods respectively. - - \item @{attribute (HOL) quot_thm} declares that a certain theorem - is a quotient extension theorem. Quotient extension theorems - allow for quotienting inside container types. Given a polymorphic - type that serves as a container, a map function defined for this - container using @{command (HOL) "functor"} and a relation - map defined for for the container type, the quotient extension - theorem should be @{term "Quotient3 R Abs Rep \ Quotient3 - (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems - are stored in a database and are used all the steps of lifting - theorems. - - \end{description} -\ - - -section \Definition by specification \label{sec:hol-specification}\ - -text \ - \begin{matharray}{rcl} - @{command_def (HOL) "specification"} & : & @{text "theory \ proof(prove)"} \\ - \end{matharray} - - @{rail \ - @@{command (HOL) specification} '(' (decl +) ')' \ - (@{syntax thmdecl}? @{syntax prop} +) - ; - decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')? - \} - - \begin{description} - - \item @{command (HOL) "specification"}~@{text "decls \"} sets up a - goal stating the existence of terms with the properties specified to - hold for the constants given in @{text decls}. After finishing the - proof, the theory will be augmented with definitions for the given - constants, as well as with theorems stating the properties for these - constants. - - @{text decl} declares a constant to be defined by the - specification given. The definition for the constant @{text c} is - bound to the name @{text c_def} unless a theorem name is given in - the declaration. Overloaded constants should be declared as such. - - \end{description} -\ - - -section \Adhoc overloading of constants\ - -text \ - \begin{tabular}{rcll} - @{command_def "adhoc_overloading"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "no_adhoc_overloading"} & : & @{text "local_theory \ local_theory"} \\ - @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text false} \\ - \end{tabular} - - \medskip - - Adhoc overloading allows to overload a constant depending on - its type. Typically this involves the introduction of an - uninterpreted constant (used for input and output) and the addition - of some variants (used internally). For examples see - @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and - @{file "~~/src/HOL/Library/Monad_Syntax.thy"}. - - @{rail \ - (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) - (@{syntax nameref} (@{syntax term} + ) + @'and') - \} - - \begin{description} - - \item @{command "adhoc_overloading"}~@{text "c v\<^sub>1 ... v\<^sub>n"} - associates variants with an existing constant. - - \item @{command "no_adhoc_overloading"} is similar to - @{command "adhoc_overloading"}, but removes the specified variants - from the present context. - - \item @{attribute "show_variants"} controls printing of variants - of overloaded constants. If enabled, the internally used variants - are printed instead of their respective overloaded constants. This - is occasionally useful to check whether the system agrees with a - user's expectations about derived variants. + theorem that would lift to the current subgoal, lifts it and leaves as a + subgoal. This method can be used with partial equivalence quotients where + the non regularized statements would not be true. @{method (HOL) + "partiality_descending_setup"} leaves the injection and cleaning subgoals + unchanged. + + \item @{method (HOL) "regularize"} applies the regularization heuristics + to the current subgoal. + + \item @{method (HOL) "injection"} applies the injection heuristics to the + current goal using the stored quotient respectfulness theorems. + + \item @{method (HOL) "cleaning"} applies the injection cleaning heuristics + to the current subgoal using the stored quotient preservation theorems. + + \item @{attribute (HOL) quot_lifted} attribute tries to automatically + transport the theorem to the quotient type. The attribute uses all the + defined quotients types and quotient constants often producing undesired + results or theorems that cannot be lifted. + + \item @{attribute (HOL) quot_respect} and @{attribute (HOL) quot_preserve} + attributes declare a theorem as a respectfulness and preservation theorem + respectively. These are stored in the local theory store and used by the + @{method (HOL) "injection"} and @{method (HOL) "cleaning"} methods + respectively. + + \item @{attribute (HOL) quot_thm} declares that a certain theorem is a + quotient extension theorem. Quotient extension theorems allow for + quotienting inside container types. Given a polymorphic type that serves + as a container, a map function defined for this container using @{command + (HOL) "functor"} and a relation map defined for for the container type, + the quotient extension theorem should be @{term "Quotient3 R Abs Rep \ + Quotient3 (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems + are stored in a database and are used all the steps of lifting theorems. \end{description} \ @@ -1446,31 +1427,244 @@ chapter \Proof tools\ -section \Adhoc tuples\ + +section \Lifting package \label{sec:lifting}\ text \ \begin{matharray}{rcl} - @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\ + @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \ local_theory"}\\ + @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \ proof(prove)"}\\ + @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \ local_theory"}\\ + @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \ local_theory"}\\ + @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ + @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ + @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\ + @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\ + @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\ + @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\ \end{matharray} + The Lifting package allows users to lift terms of the raw type to the + abstract type, which is a necessary step in building a library for an + abstract type. Lifting defines a new constant by combining coercion + functions (@{term Abs} and @{term Rep}) with the raw term. It also proves + an appropriate transfer rule for the Transfer (\secref{sec:transfer}) + package and, if possible, an equation for the code generator. + + The Lifting package provides two main commands: @{command (HOL) + "setup_lifting"} for initializing the package to work with a new type, and + @{command (HOL) "lift_definition"} for lifting constants. The Lifting + package works with all four kinds of type abstraction: type copies, + subtypes, total quotients and partial quotients. + + Theoretical background can be found in @{cite + "Huffman-Kuncar:2013:lifting_transfer"}. + @{rail \ - @@{attribute (HOL) split_format} ('(' 'complete' ')')? + @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \ + (@'parametric' @{syntax thmref})? + ; + @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \ + @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \ + (@'parametric' (@{syntax thmref}+))? + ; + @@{command (HOL) lifting_forget} @{syntax nameref} + ; + @@{command (HOL) lifting_update} @{syntax nameref} + ; + @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})? \} \begin{description} - \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes - arguments in function applications to be represented canonically - according to their tuple type structure. - - Note that this operation tends to invent funny names for new local - parameters introduced. + \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work + with a user-defined type. The command supports two modes. The first one is + a low-level mode when the user must provide as a first argument of + @{command (HOL) "setup_lifting"} a quotient theorem @{term "Quotient R Abs + Rep T"}. The package configures a transfer rule for equality, a domain + transfer rules and sets up the @{command_def (HOL) "lift_definition"} + command to work with the abstract type. An optional theorem @{term "reflp + R"}, which certifies that the equivalence relation R is total, can be + provided as a second argument. This allows the package to generate + stronger transfer rules. And finally, the parametricity theorem for R can + be provided as a third argument. This allows the package to generate a + stronger transfer rule for equality. + + Users generally will not prove the @{text Quotient} theorem manually for + new types, as special commands exist to automate the process. + + When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) + "lift_definition"} can be used in its second mode, where only the + type_definition theorem @{text "type_definition Rep Abs A"} is used as an + argument of the command. The command internally proves the corresponding + Quotient theorem and registers it with @{command (HOL) setup_lifting} + using its first mode. + + For quotients, the command @{command (HOL) quotient_type} can be used. The + command defines a new quotient type and similarly to the previous case, + the corresponding Quotient theorem is proved and registered by @{command + (HOL) setup_lifting}. + + The command @{command (HOL) "setup_lifting"} also sets up the code + generator for the new type. Later on, when a new constant is defined by + @{command (HOL) "lift_definition"}, the Lifting package proves and + registers a code equation (if there is one) for the new constant. + + \item @{command (HOL) "lift_definition"} @{text "f :: \"} @{keyword (HOL) + "is"} @{text t} Defines a new function @{text f} with an abstract type + @{text \} in terms of a corresponding operation @{text t} on a + representation type. More formally, if @{text "t :: \"}, then the command + builds a term @{text "F"} as a corresponding combination of abstraction + and representation functions such that @{text "F :: \ \ \" } and defines + @{text f} is as @{text "f \ F t"}. The term @{text t} does not have to be + necessarily a constant but it can be any term. + + The command opens a proof environment and the user must discharge a + respectfulness proof obligation. For a type copy, i.e., a typedef with + @{text UNIV}, the obligation is discharged automatically. The proof goal + is presented in a user-friendly, readable form. A respectfulness theorem + in the standard format @{text f.rsp} and a transfer rule @{text + f.transfer} for the Transfer package are generated by the package. + + The user can specify a parametricity theorems for @{text t} after the + keyword @{keyword "parametric"}, which allows the command to generate + parametric transfer rules for @{text f}. + + For each constant defined through trivial quotients (type copies or + subtypes) @{text f.rep_eq} is generated. The equation is a code + certificate that defines @{text f} using the representation function. + + For each constant @{text f.abs_eq} is generated. The equation is + unconditional for total quotients. The equation defines @{text f} using + the abstraction function. + + Integration with [@{attribute code} abstract]: For subtypes (e.g., + corresponding to a datatype invariant, such as @{typ "'a dlist"}), + @{command (HOL) "lift_definition"} uses a code certificate theorem @{text + f.rep_eq} as a code equation. Because of the limitation of the code + generator, @{text f.rep_eq} cannot be used as a code equation if the + subtype occurs inside the result type rather than at the top level (e.g., + function returning @{typ "'a dlist option"} vs. @{typ "'a dlist"}). In + this case, an extension of @{command (HOL) "lift_definition"} can be + invoked by specifying the flag @{text "code_dt"}. This extension enables + code execution through series of internal type and lifting definitions if + the return type @{text "\"} meets the following inductive conditions: + \begin{description} \item @{text "\"} is a type variable \item @{text "\ = + \\<^sub>1 \ \\<^sub>n \"}, where @{text "\"} is an abstract type constructor and + @{text "\\<^sub>1 \ \\<^sub>n"} do not contain abstract types (i.e., @{typ "int + dlist"} is allowed whereas @{typ "int dlist dlist"} not) \item @{text "\ = + \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that was defined as a + (co)datatype whose constructor argument types do not contain either + non-free datatypes or the function type. \end{description} + + Integration with [@{attribute code} equation]: For total quotients, + @{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code + equation. + + \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} + These two commands serve for storing and deleting the set-up of the + Lifting package and corresponding transfer rules defined by this package. + This is useful for hiding of type construction details of an abstract type + when the construction is finished but it still allows additions to this + construction when this is later necessary. + + Whenever the Lifting package is set up with a new abstract type @{text + "\"} by @{command_def (HOL) "lift_definition"}, the package defines a new + bundle that is called @{text "\.lifting"}. This bundle already includes + set-up for the Lifting package. The new transfer rules introduced by + @{command (HOL) "lift_definition"} can be stored in the bundle by the + command @{command (HOL) "lifting_update"} @{text "\.lifting"}. + + The command @{command (HOL) "lifting_forget"} @{text "\.lifting"} deletes + set-up of the Lifting package for @{text \} and deletes all the transfer + rules that were introduced by @{command (HOL) "lift_definition"} using + @{text \} as an abstract type. + + The stored set-up in a bundle can be reintroduced by the Isar commands for + including a bundle (@{command "include"}, @{keyword "includes"} and + @{command "including"}). + + \item @{command (HOL) "print_quot_maps"} prints stored quotient map + theorems. + + \item @{command (HOL) "print_quotients"} prints stored quotient theorems. + + \item @{attribute (HOL) quot_map} registers a quotient map theorem, a + theorem showing how to "lift" quotients over type constructors. E.g., + @{term "Quotient R Abs Rep T \ Quotient (rel_set R) (image Abs) (image + Rep) (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} + or @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically + if the involved type is BNF without dead variables. + + \item @{attribute (HOL) relator_eq_onp} registers a theorem that shows + that a relator applied to an equality restricted by a predicate @{term P} + (i.e., @{term "eq_onp P"}) is equal to a predicator applied to the @{term + P}. The combinator @{const eq_onp} is used for internal encoding of proper + subtypes. Such theorems allows the package to hide @{text eq_onp} from a + user in a user-readable form of a respectfulness theorem. For examples see + @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. + This property is proved automatically if the involved type is BNF without + dead variables. + + \item @{attribute (HOL) "relator_mono"} registers a property describing a + monotonicity of a relator. E.g., @{term "A \ B \ rel_set A \ rel_set B"}. + This property is needed for proving a stronger transfer rule in + @{command_def (HOL) "lift_definition"} when a parametricity theorem for + the raw term is specified and also for the reflexivity prover. For + examples see @{file "~~/src/HOL/Lifting_Set.thy"} or @{file + "~~/src/HOL/Lifting.thy"}. This property is proved automatically if the + involved type is BNF without dead variables. + + \item @{attribute (HOL) "relator_distr"} registers a property describing a + distributivity of the relation composition and a relator. E.g., @{text + "rel_set R \\ rel_set S = rel_set (R \\ S)"}. This property is needed for + proving a stronger transfer rule in @{command_def (HOL) "lift_definition"} + when a parametricity theorem for the raw term is specified. When this + equality does not hold unconditionally (e.g., for the function type), the + user can specified each direction separately and also register multiple + theorems with different set of assumptions. This attribute can be used + only after the monotonicity property was already registered by @{attribute + (HOL) "relator_mono"}. For examples see @{file + "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This + property is proved automatically if the involved type is BNF without dead + variables. + + \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem + from the Lifting infrastructure and thus de-register the corresponding + quotient. This effectively causes that @{command (HOL) lift_definition} + will not do any lifting for the corresponding type. This attribute is + rather used for low-level manipulation with set-up of the Lifting package + because @{command (HOL) lifting_forget} is preferred for normal usage. + + \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def + pcr_cr_eq_thm"} registers the Quotient theorem @{text Quotient_thm} in the + Lifting infrastructure and thus sets up lifting for an abstract type + @{text \} (that is defined by @{text Quotient_thm}). Optional theorems + @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register the + parametrized correspondence relation for @{text \}. E.g., for @{typ "'a + dlist"}, @{text pcr_def} is @{text "pcr_dlist A \ list_all2 A \\ + cr_dlist"} and @{text pcr_cr_eq_thm} is @{text "pcr_dlist op= = op="}. + This attribute is rather used for low-level manipulation with set-up of + the Lifting package because using of the bundle @{text \.lifting} together + with the commands @{command (HOL) lifting_forget} and @{command (HOL) + lifting_update} is preferred for normal usage. + + \item Integration with the BNF package @{cite "isabelle-datatypes"}: As + already mentioned, the theorems that are registered by the following + attributes are proved and registered automatically if the involved type is + BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) + relator_eq_onp}, @{attribute (HOL) "relator_mono"}, @{attribute (HOL) + "relator_distr"}. Also the definition of a relator and predicator is + provided automatically. Moreover, if the BNF represents a datatype, + simplification rules for a predicator are again proved automatically. \end{description} \ -section \Transfer package\ +section \Transfer package \label{sec:transfer}\ text \ \begin{matharray}{rcl} @@ -1487,318 +1681,81 @@ \begin{description} - \item @{method (HOL) "transfer"} method replaces the current subgoal - with a logically equivalent one that uses different types and - constants. The replacement of types and constants is guided by the - database of transfer rules. Goals are generalized over all free - variables by default; this is necessary for variables whose types - change, but can be overridden for specific variables with e.g. - @{text "transfer fixing: x y z"}. - - \item @{method (HOL) "transfer'"} is a variant of @{method (HOL) - transfer} that allows replacing a subgoal with one that is - logically stronger (rather than equivalent). For example, a - subgoal involving equality on a quotient type could be replaced - with a subgoal involving equality (instead of the corresponding - equivalence relation) on the underlying raw type. - - \item @{method (HOL) "transfer_prover"} method assists with proving - a transfer rule for a new constant, provided the constant is - defined in terms of other constants that already have transfer - rules. It should be applied after unfolding the constant - definitions. - - \item @{attribute (HOL) "untransferred"} proves the same equivalent theorem - as @{method (HOL) "transfer"} internally does. + \item @{method (HOL) "transfer"} method replaces the current subgoal with + a logically equivalent one that uses different types and constants. The + replacement of types and constants is guided by the database of transfer + rules. Goals are generalized over all free variables by default; this is + necessary for variables whose types change, but can be overridden for + specific variables with e.g. @{text "transfer fixing: x y z"}. + + \item @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer} + that allows replacing a subgoal with one that is logically stronger + (rather than equivalent). For example, a subgoal involving equality on a + quotient type could be replaced with a subgoal involving equality (instead + of the corresponding equivalence relation) on the underlying raw type. + + \item @{method (HOL) "transfer_prover"} method assists with proving a + transfer rule for a new constant, provided the constant is defined in + terms of other constants that already have transfer rules. It should be + applied after unfolding the constant definitions. + + \item @{attribute (HOL) "untransferred"} proves the same equivalent + theorem as @{method (HOL) "transfer"} internally does. \item @{attribute (HOL) Transfer.transferred} works in the opposite - direction than @{method (HOL) "transfer'"}. E.g., given the transfer - relation @{text "ZN x n \ (x = int n)"}, corresponding transfer rules and the theorem - @{text "\x::int \ {0..}. x < x + 1"}, the attribute would prove - @{text "\n::nat. n < n + 1"}. The attribute is still in experimental - phase of development. - - \item @{attribute (HOL) "transfer_rule"} attribute maintains a - collection of transfer rules, which relate constants at two - different types. Typical transfer rules may relate different type - instances of the same polymorphic constant, or they may relate an - operation on a raw type to a corresponding operation on an - abstract type (quotient or subtype). For example: - - @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"}\\ + direction than @{method (HOL) "transfer'"}. E.g., given the transfer + relation @{text "ZN x n \ (x = int n)"}, corresponding transfer rules and + the theorem @{text "\x::int \ {0..}. x < x + 1"}, the attribute would + prove @{text "\n::nat. n < n + 1"}. The attribute is still in experimental + phase of development. + + \item @{attribute (HOL) "transfer_rule"} attribute maintains a collection + of transfer rules, which relate constants at two different types. Typical + transfer rules may relate different type instances of the same polymorphic + constant, or they may relate an operation on a raw type to a corresponding + operation on an abstract type (quotient or subtype). For example: + + @{text "((A ===> B) ===> list_all2 A ===> list_all2 B) map map"} \\ @{text "(cr_int ===> cr_int ===> cr_int) (\(x,y) (u,v). (x+u, y+v)) plus"} - Lemmas involving predicates on relations can also be registered - using the same attribute. For example: - - @{text "bi_unique A \ (list_all2 A ===> op =) distinct distinct"}\\ + Lemmas involving predicates on relations can also be registered using the + same attribute. For example: + + @{text "bi_unique A \ (list_all2 A ===> op =) distinct distinct"} \\ @{text "\bi_unique A; bi_unique B\ \ bi_unique (rel_prod A B)"} - Preservation of predicates on relations (@{text "bi_unique, bi_total, - right_unique, right_total, left_unique, left_total"}) with the respect to a relator - is proved automatically if the involved type is BNF - @{cite "isabelle-datatypes"} without dead variables. - - \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection - of rules, which specify a domain of a transfer relation by a predicate. - E.g., given the transfer relation @{text "ZN x n \ (x = int n)"}, - one can register the following transfer domain rule: - @{text "Domainp ZN = (\x. x \ 0)"}. The rules allow the package to produce - more readable transferred goals, e.g., when quantifiers are transferred. - - \item @{attribute (HOL) relator_eq} attribute collects identity laws - for relators of various type constructors, e.g. @{term "rel_set - (op =) = (op =)"}. The @{method (HOL) transfer} method uses these - lemmas to infer transfer rules for non-polymorphic constants on - the fly. For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. - - \item @{attribute_def (HOL) "relator_domain"} attribute collects rules - describing domains of relators by predicators. E.g., - @{term "Domainp (rel_set T) = (\A. Ball A (Domainp T))"}. This allows the package - to lift transfer domain rules through type constructors. For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. + Preservation of predicates on relations (@{text "bi_unique, bi_total, + right_unique, right_total, left_unique, left_total"}) with the respect to + a relator is proved automatically if the involved type is BNF @{cite + "isabelle-datatypes"} without dead variables. + + \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a + collection of rules, which specify a domain of a transfer relation by a + predicate. E.g., given the transfer relation @{text "ZN x n \ (x = int + n)"}, one can register the following transfer domain rule: @{text "Domainp + ZN = (\x. x \ 0)"}. The rules allow the package to produce more readable + transferred goals, e.g., when quantifiers are transferred. + + \item @{attribute (HOL) relator_eq} attribute collects identity laws for + relators of various type constructors, e.g. @{term "rel_set (op =) = (op + =)"}. The @{method (HOL) transfer} method uses these lemmas to infer + transfer rules for non-polymorphic constants on the fly. For examples see + @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. + This property is proved automatically if the involved type is BNF without + dead variables. + + \item @{attribute_def (HOL) "relator_domain"} attribute collects rules + describing domains of relators by predicators. E.g., @{term "Domainp + (rel_set T) = (\A. Ball A (Domainp T))"}. This allows the package to lift + transfer domain rules through type constructors. For examples see @{file + "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This + property is proved automatically if the involved type is BNF without dead + variables. \end{description} - Theoretical background can be found in @{cite "Huffman-Kuncar:2013:lifting_transfer"}. -\ - - -section \Lifting package\ - -text \ - The Lifting package allows users to lift terms of the raw type to the abstract type, which is - a necessary step in building a library for an abstract type. Lifting defines a new constant - by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate - transfer rule for the Transfer package and, if possible, an equation for the code generator. - - The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing - the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants. - The Lifting package works with all four kinds of type abstraction: type copies, subtypes, - total quotients and partial quotients. - - Theoretical background can be found in @{cite "Huffman-Kuncar:2013:lifting_transfer"}. - - \begin{matharray}{rcl} - @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \ local_theory"}\\ - @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \ proof(prove)"}\\ - @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \ local_theory"}\\ - @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \ local_theory"}\\ - @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ - @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ - @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\ - @{attribute_def (HOL) "relator_eq_onp"} & : & @{text attribute} \\ - @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\ - @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\ - @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\ - @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\ - \end{matharray} - - @{rail \ - @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \ - (@'parametric' @{syntax thmref})? - \} - - @{rail \ - @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? @{syntax name} '::' @{syntax type} \ - @{syntax mixfix}? 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))? - \} - - @{rail \ - @@{command (HOL) lifting_forget} @{syntax nameref} - \} - - @{rail \ - @@{command (HOL) lifting_update} @{syntax nameref} - \} - - @{rail \ - @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})? - \} - - \begin{description} - - \item @{command (HOL) "setup_lifting"} Sets up the Lifting package - to work with a user-defined type. - The command supports two modes. The first one is a low-level mode when - the user must provide as a first - argument of @{command (HOL) "setup_lifting"} a - quotient theorem @{term "Quotient R Abs Rep T"}. The - package configures a transfer rule for equality, a domain transfer - rules and sets up the @{command_def (HOL) "lift_definition"} - command to work with the abstract type. An optional theorem @{term "reflp R"}, which certifies that - the equivalence relation R is total, - can be provided as a second argument. This allows the package to generate stronger transfer - rules. And finally, the parametricity theorem for R can be provided as a third argument. - This allows the package to generate a stronger transfer rule for equality. - - Users generally will not prove the @{text Quotient} theorem manually for - new types, as special commands exist to automate the process. - - When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"} - can be used in its - second mode, where only the type_definition theorem @{text "type_definition Rep Abs A"} - is used as an argument of the command. The command internally proves the corresponding - Quotient theorem and registers it with @{command (HOL) setup_lifting} using its first mode. - - For quotients, the command @{command (HOL) quotient_type} can be used. The command defines - a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved - and registered by @{command (HOL) setup_lifting}. - - The command @{command (HOL) "setup_lifting"} also sets up the code generator - for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"}, - the Lifting package proves and registers a code equation (if there is one) for the new constant. - - \item @{command (HOL) "lift_definition"} @{text "f :: \"} @{keyword (HOL) "is"} @{text t} - Defines a new function @{text f} with an abstract type @{text \} - in terms of a corresponding operation @{text t} on a - representation type. More formally, if @{text "t :: \"}, then - the command builds a term @{text "F"} as a corresponding combination of abstraction - and representation functions such that @{text "F :: \ \ \" } and - defines @{text f} is as @{text "f \ F t"}. - The term @{text t} does not have to be necessarily a constant but it can be any term. - - The command opens a proof environment and the user must discharge - a respectfulness proof obligation. For a type copy, i.e., a typedef with @{text - UNIV}, the obligation is discharged automatically. The proof goal is - presented in a user-friendly, readable form. A respectfulness - theorem in the standard format @{text f.rsp} and a transfer rule - @{text f.transfer} for the Transfer package are generated by the - package. - - The user can specify a parametricity theorems for @{text t} after the keyword - @{keyword "parametric"}, which allows the command - to generate parametric transfer rules for @{text f}. - - For each constant defined through trivial quotients (type copies or - subtypes) @{text f.rep_eq} is generated. The equation is a code certificate - that defines @{text f} using the representation function. - - For each constant @{text f.abs_eq} is generated. The equation is unconditional - for total quotients. The equation defines @{text f} using - the abstraction function. - - Integration with [@{attribute code} abstract]: For subtypes (e.g., - corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command - (HOL) "lift_definition"} uses a code certificate theorem - @{text f.rep_eq} as a code equation. Because of the limitation of the code generator, - @{text f.rep_eq} cannot be used as a code equation if the subtype occurs inside the result - type rather than at the top level (e.g., function returning @{typ "'a dlist option"} vs. - @{typ "'a dlist"}). In this case, an extension of @{command - (HOL) "lift_definition"} can be invoked by specifying the flag @{text "code_dt"}. This - extension enables code execution through series of internal type and lifting definitions - if the return type @{text "\"} meets the following inductive conditions: - \begin{description} - \item @{text "\"} is a type variable - \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, where @{text "\"} is an abstract type constructor - and @{text "\\<^sub>1 \ \\<^sub>n"} do not contain abstract types (i.e., @{typ "int dlist"} is allowed - whereas @{typ "int dlist dlist"} not) - \item @{text "\ = \\<^sub>1 \ \\<^sub>n \"}, @{text "\"} is a type constructor that was defined as a - (co)datatype whose constructor argument types do not contain either non-free datatypes - or the function type. - \end{description} - - Integration with [@{attribute code} equation]: For total quotients, @{command - (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation. - - \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} - These two commands serve for storing and deleting the set-up of - the Lifting package and corresponding transfer rules defined by this package. - This is useful for hiding of type construction details of an abstract type - when the construction is finished but it still allows additions to this construction - when this is later necessary. - - Whenever the Lifting package is set up with a new abstract type @{text "\"} by - @{command_def (HOL) "lift_definition"}, the package defines a new bundle - that is called @{text "\.lifting"}. This bundle already includes set-up for the Lifting package. - The new transfer rules - introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by - the command @{command (HOL) "lifting_update"} @{text "\.lifting"}. - - The command @{command (HOL) "lifting_forget"} @{text "\.lifting"} deletes set-up of the Lifting - package - for @{text \} and deletes all the transfer rules that were introduced - by @{command (HOL) "lift_definition"} using @{text \} as an abstract type. - - The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle - (@{command "include"}, @{keyword "includes"} and @{command "including"}). - - \item @{command (HOL) "print_quot_maps"} prints stored quotient map - theorems. - - \item @{command (HOL) "print_quotients"} prints stored quotient - theorems. - - \item @{attribute (HOL) quot_map} registers a quotient map - theorem, a theorem showing how to "lift" quotients over type constructors. - E.g., @{term "Quotient R Abs Rep T \ - Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"}. - For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. - - \item @{attribute (HOL) relator_eq_onp} registers a theorem that - shows that a relator applied to an equality restricted by a predicate @{term P} (i.e., @{term - "eq_onp P"}) is equal - to a predicator applied to the @{term P}. The combinator @{const eq_onp} is used for - internal encoding of proper subtypes. Such theorems allows the package to hide @{text - eq_onp} from a user in a user-readable form of a - respectfulness theorem. For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. - - \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator. - E.g., @{term "A \ B \ rel_set A \ rel_set B"}. - This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"} - when a parametricity theorem for the raw term is specified and also for the reflexivity prover. - For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. - - \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity - of the relation composition and a relator. E.g., - @{text "rel_set R \\ rel_set S = rel_set (R \\ S)"}. - This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"} - when a parametricity theorem for the raw term is specified. - When this equality does not hold unconditionally (e.g., for the function type), the user can specified - each direction separately and also register multiple theorems with different set of assumptions. - This attribute can be used only after the monotonicity property was already registered by - @{attribute (HOL) "relator_mono"}. For examples see @{file - "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. - This property is proved automatically if the involved type is BNF without dead variables. - - \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem - from the Lifting infrastructure and thus de-register the corresponding quotient. - This effectively causes that @{command (HOL) lift_definition} will not - do any lifting for the corresponding type. This attribute is rather used for low-level - manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is - preferred for normal usage. - - \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"} - registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure - and thus sets up lifting for an abstract type @{text \} (that is defined by @{text Quotient_thm}). - Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register - the parametrized - correspondence relation for @{text \}. E.g., for @{typ "'a dlist"}, @{text pcr_def} is - @{text "pcr_dlist A \ list_all2 A \\ cr_dlist"} and @{text pcr_cr_eq_thm} is - @{text "pcr_dlist op= = op="}. - This attribute is rather used for low-level - manipulation with set-up of the Lifting package because using of the bundle @{text \.lifting} - together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is - preferred for normal usage. - - \item Integration with the BNF package @{cite "isabelle-datatypes"}: - As already mentioned, the theorems that are registered - by the following attributes are proved and registered automatically if the involved type - is BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp}, - @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also the definition of a - relator and predicator is provided automatically. Moreover, if the BNF represents a datatype, - simplification rules for a predicator are again proved automatically. - - \end{description} + Theoretical background can be found in @{cite + "Huffman-Kuncar:2013:lifting_transfer"}. \ @@ -2264,10 +2221,10 @@ them back into Isabelle terms for displaying counterexamples. \begin{description} \item[@{text exhaustive}] The parameters of the type classes @{class exhaustive} - and @{class full_exhaustive} implement the testing. They take a + and @{class full_exhaustive} implement the testing. They take a testing function as a parameter, which takes a value of type @{typ "'a"} and optionally produces a counterexample, and a size parameter for the test values. - In @{class full_exhaustive}, the testing function parameter additionally + In @{class full_exhaustive}, the testing function parameter additionally expects a lazy term reconstruction in the type @{typ Code_Evaluation.term} of the tested value. @@ -2280,7 +2237,7 @@ value of the given size and a lazy term reconstruction of the value in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator is defined in theory @{theory Random}. - + \item[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"} using the type classes @{class narrowing} and @{class partial_term_of}. Variables in the current goal are initially represented as symbolic variables. @@ -2402,6 +2359,31 @@ \ + +section \Adhoc tuples\ + +text \ + \begin{matharray}{rcl} + @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\ + \end{matharray} + + @{rail \ + @@{attribute (HOL) split_format} ('(' 'complete' ')')? + \} + + \begin{description} + + \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes + arguments in function applications to be represented canonically + according to their tuple type structure. + + Note that this operation tends to invent funny names for new local + parameters introduced. + + \end{description} +\ + + chapter \Executable code\ text \For validation purposes, it is often useful to \emph{execute} @@ -2614,7 +2596,7 @@ if needed these are implemented by program abort (exception) instead. Usually packages introducing code equations provide a reasonable - default setup for selection. + default setup for selection. \item @{command (HOL) "code_datatype"} specifies a constructor set for a logical type. diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/Isar_Ref/ML_Tactic.thy --- a/src/Doc/Isar_Ref/ML_Tactic.thy Fri Jul 03 10:17:29 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,177 +0,0 @@ -theory ML_Tactic -imports Base Main -begin - -chapter \ML tactic expressions\ - -text \ - Isar Proof methods closely resemble traditional tactics, when used - in unstructured sequences of @{command "apply"} commands. - Isabelle/Isar provides emulations for all major ML tactics of - classic Isabelle --- mostly for the sake of easy porting of existing - developments, as actual Isar proof texts would demand much less - diversity of proof methods. - - Unlike tactic expressions in ML, Isar proof methods provide proper - concrete syntax for additional arguments, options, modifiers etc. - Thus a typical method text is usually more concise than the - corresponding ML tactic. Furthermore, the Isar versions of classic - Isabelle tactics often cover several variant forms by a single - method with separate options to tune the behavior. For example, - method @{method simp} replaces all of @{ML simp_tac}~/ @{ML - asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there - is also concrete syntax for augmenting the Simplifier context (the - current ``simpset'') in a convenient way. -\ - - -section \Resolution tactics\ - -text \ - Classic Isabelle provides several variant forms of tactics for - single-step rule applications (based on higher-order resolution). - The space of resolution tactics has the following main dimensions. - - \begin{enumerate} - - \item The ``mode'' of resolution: intro, elim, destruct, or forward - (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, - @{ML forward_tac}). - - \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ - @{ML Rule_Insts.res_inst_tac}). - - \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} - vs.\ @{ML rtac}). - - \end{enumerate} - - Basically, the set of Isar tactic emulations @{method rule_tac}, - @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see - \secref{sec:tactics}) would be sufficient to cover the four modes, - either with or without instantiation, and either with single or - multiple arguments. Although it is more convenient in most cases to - use the plain @{method_ref (Pure) rule} method, or any of its - ``improper'' variants @{method erule}, @{method drule}, @{method - frule}. Note that explicit goal addressing is only supported by the - actual @{method rule_tac} version. - - With this in mind, plain resolution tactics correspond to Isar - methods as follows. - - \medskip - \begin{tabular}{lll} - @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ - @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ - @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a 1"} & & - @{text "rule_tac x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\[0.5ex] - @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ - @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ - @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a i"} & & - @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\ - \end{tabular} - \medskip - - Note that explicit goal addressing may be usually avoided by - changing the order of subgoals with @{command "defer"} or @{command - "prefer"} (see \secref{sec:tactic-commands}). -\ - - -section \Simplifier tactics\ - -text \The main Simplifier tactics @{ML simp_tac} and variants are - all covered by the @{method simp} and @{method simp_all} methods - (see \secref{sec:simplifier}). Note that there is no individual - goal addressing available, simplification acts either on the first - goal (@{method simp}) or all goals (@{method simp_all}). - - \medskip - \begin{tabular}{lll} - @{ML asm_full_simp_tac}~@{text "@{context} 1"} & & @{method simp} \\ - @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex] - @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\ - @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\ - @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\ - @{ML asm_lr_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(asm_lr)"} \\ - \end{tabular} - \medskip -\ - - -section \Classical Reasoner tactics\ - -text \The Classical Reasoner provides a rather large number of - variations of automated tactics, such as @{ML blast_tac}, @{ML - fast_tac}, @{ML clarify_tac} etc. The corresponding Isar methods - usually share the same base name, such as @{method blast}, @{method - fast}, @{method clarify} etc.\ (see \secref{sec:classical}).\ - - -section \Miscellaneous tactics\ - -text \ - There are a few additional tactics defined in various theories of - Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. - The most common ones of these may be ported to Isar as follows. - - \medskip - \begin{tabular}{lll} - @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\ - @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\ - @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\ - & @{text "\"} & @{text "simp only: split_tupled_all"} \\ - & @{text "\"} & @{text "clarify"} \\ - \end{tabular} -\ - - -section \Tacticals\ - -text \ - Classic Isabelle provides a huge amount of tacticals for combination - and modification of existing tactics. This has been greatly reduced - in Isar, providing the bare minimum of combinators only: ``@{text - ","}'' (sequential composition), ``@{text "|"}'' (alternative - choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least - once). These are usually sufficient in practice; if all fails, - arbitrary ML tactic code may be invoked via the @{method tactic} - method (see \secref{sec:tactics}). - - \medskip Common ML tacticals may be expressed directly in Isar as - follows: - - \medskip - \begin{tabular}{lll} - @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\ - @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\ - @{ML TRY}~@{text tac} & & @{text "meth?"} \\ - @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\ - @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\ - @{ML EVERY}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1, \"} \\ - @{ML FIRST}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1 | \"} \\ - \end{tabular} - \medskip - - \medskip @{ML CHANGED} (see @{cite "isabelle-implementation"}) is - usually not required in Isar, since most basic proof methods already - fail unless there is an actual change in the goal state. - Nevertheless, ``@{text "?"}'' (try) may be used to accept - \emph{unchanged} results as well. - - \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see - @{cite "isabelle-implementation"}) are not available in Isar, since - there is no direct goal addressing. Nevertheless, some basic - methods address all goals internally, notably @{method simp_all} - (see \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be - often replaced by ``@{text "+"}'' (repeat at least once), although - this usually has a different operational behavior: subgoals are - solved in a different order. - - \medskip Iterated resolution, such as - @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better - expressed using the @{method intro} and @{method elim} methods of - Isar (see \secref{sec:classical}). -\ - -end diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/Isar_Ref/document/root.tex --- a/src/Doc/Isar_Ref/document/root.tex Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Doc/Isar_Ref/document/root.tex Mon Jul 06 14:27:03 2015 +0200 @@ -86,7 +86,6 @@ \input{Quick_Reference.tex} \let\int\intorig \input{Symbols.tex} -\input{ML_Tactic.tex} \begingroup \tocentry{\bibname} diff -r 03a25d3e759e -r 143ac4d9504a src/Doc/ROOT --- a/src/Doc/ROOT Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Doc/ROOT Mon Jul 06 14:27:03 2015 +0200 @@ -171,7 +171,6 @@ HOL_Specific Quick_Reference Symbols - ML_Tactic document_files (in "..") "prepare_document" "pdfsetup.sty" diff -r 03a25d3e759e -r 143ac4d9504a src/FOLP/ex/Nat.thy --- a/src/FOLP/ex/Nat.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/FOLP/ex/Nat.thy Mon Jul 06 14:27:03 2015 +0200 @@ -82,24 +82,26 @@ lemmas nat_congs = Suc_cong Plus_cong ML {* - val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}] + val add_ss = + FOLP_ss addcongs @{thms nat_congs} + |> fold (addrew @{context}) @{thms add_0 add_Suc} *} schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)" apply (rule_tac n = k in induct) -apply (tactic {* SIMP_TAC add_ss 1 *}) -apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) +apply (tactic {* SIMP_TAC @{context} add_ss 1 *}) +apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *}) done schematic_lemma add_0_right: "?p : m+0 = m" apply (rule_tac n = m in induct) -apply (tactic {* SIMP_TAC add_ss 1 *}) -apply (tactic {* ASM_SIMP_TAC add_ss 1 *}) +apply (tactic {* SIMP_TAC @{context} add_ss 1 *}) +apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *}) done schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" apply (rule_tac n = m in induct) -apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *}) +apply (tactic {* ALLGOALS (ASM_SIMP_TAC @{context} add_ss) *}) done (*mk_typed_congs appears not to work with FOLP's version of subst*) diff -r 03a25d3e759e -r 143ac4d9504a src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/FOLP/simp.ML Mon Jul 06 14:27:03 2015 +0200 @@ -24,26 +24,26 @@ end; -infix 4 addrews addcongs delrews delcongs setauto; +infix 4 addcongs delrews delcongs setauto; signature SIMP = sig type simpset val empty_ss : simpset val addcongs : simpset * thm list -> simpset - val addrews : simpset * thm list -> simpset + val addrew : Proof.context -> thm -> simpset -> simpset val delcongs : simpset * thm list -> simpset val delrews : simpset * thm list -> simpset val dest_ss : simpset -> thm list * thm list - val print_ss : simpset -> unit + val print_ss : Proof.context -> simpset -> unit val setauto : simpset * (int -> tactic) -> simpset - val ASM_SIMP_CASE_TAC : simpset -> int -> tactic - val ASM_SIMP_TAC : simpset -> int -> tactic + val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic + val ASM_SIMP_TAC : Proof.context -> simpset -> int -> tactic val CASE_TAC : simpset -> int -> tactic - val SIMP_CASE2_TAC : simpset -> int -> tactic - val SIMP_THM : simpset -> thm -> thm - val SIMP_TAC : simpset -> int -> tactic - val SIMP_CASE_TAC : simpset -> int -> tactic + val SIMP_CASE2_TAC : Proof.context -> simpset -> int -> tactic + val SIMP_THM : Proof.context -> simpset -> thm -> thm + val SIMP_TAC : Proof.context -> simpset -> int -> tactic + val SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic val mk_congs : theory -> string list -> thm list val mk_typed_congs : theory -> (string * string) list -> thm list (* temporarily disabled: @@ -220,15 +220,13 @@ in add_norms(congs,ccs,new_asms) end; fun normed_rews congs = - let val add_norms = add_norm_tags congs in - fn thm => + let + val add_norms = add_norm_tags congs + fun normed ctxt thm = let - val ctxt = - Thm.theory_of_thm thm - |> Proof_Context.init_global - |> Variable.declare_thm thm; + val ctxt' = Variable.declare_thm thm ctxt; in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end - end; + in normed end; fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; @@ -241,7 +239,7 @@ SS of {auto_tac: int -> tactic, congs: thm list, cong_net: thm Net.net, - mk_simps: thm -> thm list, + mk_simps: Proof.context -> thm -> thm list, simps: (thm * thm list) list, simp_net: thm Net.net} @@ -251,22 +249,18 @@ (** Insertion of congruences and rewrites **) (*insert a thm in a thm net*) -fun insert_thm_warn th net = +fun insert_thm th net = Net.insert_term Thm.eq_thm_prop (Thm.concl_of th, th) net - handle Net.INSERT => - (writeln ("Duplicate rewrite or congruence rule:\n" ^ - Display.string_of_thm_without_context th); net); + handle Net.INSERT => net; -val insert_thms = fold_rev insert_thm_warn; +val insert_thms = fold_rev insert_thm; -fun addrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = -let val thms = mk_simps thm +fun addrew ctxt thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = +let val thms = mk_simps ctxt thm in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net} end; -fun ss addrews thms = fold addrew thms ss; - fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = thms @ congs; in SS{auto_tac=auto_tac, congs= congs', @@ -277,13 +271,11 @@ (** Deletion of congruences and rewrites **) (*delete a thm from a thm net*) -fun delete_thm_warn th net = +fun delete_thm th net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net - handle Net.DELETE => - (writeln ("No such rewrite or congruence rule:\n" ^ - Display.string_of_thm_without_context th); net); + handle Net.DELETE => net; -val delete_thms = fold_rev delete_thm_warn; +val delete_thms = fold_rev delete_thm; fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) = let val congs' = fold (remove Thm.eq_thm_prop) thms congs @@ -295,9 +287,7 @@ fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) = let fun find((p as (th,ths))::ps',ps) = if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps) - | find([],simps') = - (writeln ("No such rewrite or congruence rule:\n" ^ - Display.string_of_thm_without_context thm); ([], simps')) + | find([],simps') = ([], simps') val (thms,simps') = find(simps,[]) in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps, simps = simps', simp_net = delete_thms thms simp_net } @@ -315,10 +305,10 @@ fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps); -fun print_ss(SS{congs,simps,...}) = +fun print_ss ctxt (SS{congs,simps,...}) = writeln (cat_lines - (["Congruences:"] @ map Display.string_of_thm_without_context congs @ - ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps)); + (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @ + ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps)); (* Rewriting with conditionals *) @@ -385,26 +375,25 @@ in variants_abs (params, Logic.strip_assums_concl subgi) end; (*print lhs of conclusion of subgoal i*) -fun pr_goal_lhs i st = - writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) - (lhs_of (prepare_goal i st))); +fun pr_goal_lhs ctxt i st = + writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st))); (*print conclusion of subgoal i*) -fun pr_goal_concl i st = - writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) +fun pr_goal_concl ctxt i st = + writeln (Syntax.string_of_term ctxt (prepare_goal i st)) (*print subgoals i to j (inclusive)*) -fun pr_goals (i,j) st = +fun pr_goals ctxt (i,j) st = if i>j then () - else (pr_goal_concl i st; pr_goals (i+1,j) st); + else (pr_goal_concl ctxt i st; pr_goals ctxt (i+1,j) st); (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals, thm=old state, thm'=new state *) -fun pr_rew (i,n,thm,thm',not_asms) = +fun pr_rew ctxt (i,n,thm,thm',not_asms) = if !tracing then (if not_asms then () else writeln"Assumption used in"; - pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm'; - if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm') + pr_goal_lhs ctxt i thm; writeln"->"; pr_goal_lhs ctxt (i+n) thm'; + if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n-1) thm') else (); writeln"" ) else (); @@ -417,7 +406,8 @@ strip_varify(t,n,Var(("?",length vs),T)::vs) | strip_varify _ = []; -fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let +fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) = +let fun simp_lhs(thm,ss,anet,ats,cs) = if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else @@ -436,21 +426,16 @@ are represented by rules, generalized over their parameters*) fun add_asms(ss,thm,a,anet,ats,cs) = let val As = strip_varify(nth_subgoal i thm, a, []); - val thms = map (Thm.trivial o Thm.global_cterm_of(Thm.theory_of_thm thm)) As; + val thms = map (Thm.trivial o Thm.cterm_of ctxt) As; val new_rws = maps mk_rew_rules thms; val rwrls = map mk_trans (maps mk_rew_rules thms); val anet' = fold_rev lhs_insert_thm rwrls anet; - in if !tracing andalso not(null new_rws) - then writeln (cat_lines - ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws)) - else (); - (ss,thm,anet',anet::ats,cs) - end; + in (ss,thm,anet',anet::ats,cs) end; fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of SOME(thm',seq') => let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm) - in pr_rew(i,n,thm,thm',more); + in pr_rew ctxt (i,n,thm,thm',more); if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) @@ -466,7 +451,7 @@ | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs in if !tracing then (writeln"*** Failed to prove precondition. Normal form:"; - pr_goal_concl i thm; writeln"") + pr_goal_concl ctxt i thm; writeln"") else (); rew(seq,thm0,ss0,anet0,ats0,cs0,more) end; @@ -495,30 +480,30 @@ in exec(ss, thm, Net.empty, [], []) end; -fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = +fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = let val cong_tac = net_tac cong_net in fn i => (fn thm => if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty - else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm))) + else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm))) THEN TRY(auto_tac i) end; -val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false); -val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); +fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false); +fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false); -val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); -val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); +fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false); +fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false); -val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); +fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true); -fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = +fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) = let val cong_tac = net_tac cong_net in fn thm => let val state = thm RSN (2,red1) - in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end + in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end end; -val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); +fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false); (* Compute Congruence rules for individual constants using the substition diff -r 03a25d3e759e -r 143ac4d9504a src/FOLP/simpdata.ML --- a/src/FOLP/simpdata.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/FOLP/simpdata.ML Mon Jul 06 14:27:03 2015 +0200 @@ -78,9 +78,9 @@ val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; -val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews; +val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews; val FOLP_rews = IFOLP_rews @ @{thms cla_rews}; -val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews; +val FOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) FOLP_rews; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Decision_Procs/approximation.ML Mon Jul 06 14:27:03 2015 +0200 @@ -78,9 +78,9 @@ |> HOLogic.mk_list @{typ nat} |> Thm.cterm_of ctxt in - (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), - (@{cpat "?prec::nat"}, p), - (@{cpat "?ss::nat list"}, s)]) + (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n), + ((("prec", 0), @{typ nat}), p), + ((("ss", 0), @{typ "nat list"}), s)]) @{thm "approx_form"}) i THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st end @@ -95,9 +95,9 @@ val s = vs |> map lookup_splitting |> hd |> Thm.cterm_of ctxt in - rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), - (@{cpat "?t::nat"}, t), - (@{cpat "?prec::nat"}, p)]) + rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s), + ((("t", 0), @{typ nat}), t), + ((("prec", 0), @{typ nat}), p)]) @{thm "approx_tse_form"}) i st end end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Jul 06 14:27:03 2015 +0200 @@ -58,6 +58,7 @@ funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) (funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf))) |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun) + |> apply2 (apply2 (dest_Var o Thm.term_of)) fun myfwd (th1, th2, th3, th4, th5) p1 p2 [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = @@ -73,7 +74,7 @@ in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') end - val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (Thm.cprop_of qe) + val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) fun main vs p = let val ((xn,ce),(x,fm)) = (case Thm.term_of p of diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Jul 06 14:27:03 2015 +0200 @@ -9,14 +9,13 @@ Drule.cterm_instantiate. *) -structure Eisbach_Rule_Insts : sig end = +structure Eisbach_Rule_Insts: sig end = struct fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm)); -fun add_thm_insts thm = +fun add_thm_insts ctxt thm = let - val thy = Thm.theory_of_thm thm; val tyvars = Thm.fold_terms Term.add_tvars thm []; val tyvars' = tyvars |> map (Logic.mk_term o Logic.mk_type o TVar); @@ -24,7 +23,7 @@ val tvars' = tvars |> map (Logic.mk_term o Var); val conj = - Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.global_cterm_of thy |> Drule.mk_term; + Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.cterm_of ctxt |> Drule.mk_term; in ((tyvars, tvars), Conjunction.intr thm conj) end; @@ -48,19 +47,17 @@ (thm', insts') end; -fun instantiate_xis insts thm = +fun instantiate_xis ctxt insts thm = let val tyvars = Thm.fold_terms Term.add_tvars thm []; val tvars = Thm.fold_terms Term.add_vars thm []; - val cert = Thm.global_cterm_of (Thm.theory_of_thm thm); - val certT = Thm.global_ctyp_of (Thm.theory_of_thm thm); fun add_inst (xi, t) (Ts, ts) = (case AList.lookup (op =) tyvars xi of - SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts) + SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts) | NONE => (case AList.lookup (op =) tvars xi of - SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts) + SOME T => (Ts, (Thm.cterm_of ctxt (Var (xi, T)), Thm.cterm_of ctxt t) :: ts) | NONE => error "indexname not found in thm")); val (cTinsts, cinsts) = fold add_inst insts ([], []); @@ -187,7 +184,7 @@ let val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts; - val (thm_insts, thm') = add_thm_insts thm + val (thm_insts, thm') = add_thm_insts ctxt thm; val (thm'', thm_insts') = Rule_Insts.where_rule ctxt insts' fixes thm' |> get_thm_insts; @@ -215,8 +212,9 @@ val (ts', ctxt'') = Variable.import_terms false ts ctxt'; val ts'' = Variable.export_terms ctxt'' ctxt ts'; val insts' = ListPair.zip (xis, ts''); - in instantiate_xis insts' thm end - | read_instantiate_closed _ (Term_Insts insts) thm = instantiate_xis insts thm; + in instantiate_xis ctxt insts' thm end + | read_instantiate_closed ctxt (Term_Insts insts) thm = + instantiate_xis ctxt insts thm; val _ = Theory.setup diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Mon Jul 06 14:27:03 2015 +0200 @@ -440,10 +440,9 @@ val focus_schematics = #2 o Focus_Data.get; -fun add_focus_schematics cterms = +fun add_focus_schematics schematics = (Focus_Data.map o @{apply 3(2)}) - (fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t))) - (map (apply2 Thm.term_of) cterms)); + (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics); (* focus params *) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Import/import_rule.ML Mon Jul 06 14:27:03 2015 +0200 @@ -157,15 +157,12 @@ meta_mp i th4 end -fun freezeT thm = +fun freezeT thy thm = let val tvars = Term.add_tvars (Thm.prop_of thm) [] val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars - val tvars = map TVar tvars - val thy = Thm.theory_of_thm thm - fun inst ty = Thm.global_ctyp_of thy ty in - Thm.instantiate ((map inst tvars ~~ map inst tfrees), []) thm + Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm end fun def' constname rhs thy = @@ -177,7 +174,7 @@ val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs) val (thms, thy2) = Global_Theory.add_defs false [((Binding.suffix_name "_hldef" constbinding, eq), [])] thy1 - val def_thm = freezeT (hd thms) + val def_thm = freezeT thy1 (hd thms) in (meta_eq_to_obj_eq def_thm, thy2) end @@ -225,7 +222,7 @@ Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c (SOME (Binding.name rep_name, Binding.name abs_name)) (fn _ => rtac th2 1) thy val aty = #abs_type (#1 typedef_info) - val th = freezeT (#type_definition (#2 typedef_info)) + val th = freezeT thy' (#type_definition (#2 typedef_info)) val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) val (th_s, abst) = Thm.dest_comb th_s val rept = Thm.dest_arg th_s @@ -264,11 +261,12 @@ val tys_before = Term.add_tfrees (Thm.prop_of th) [] val th1 = Thm.varifyT_global th val tys_after = Term.add_tvars (Thm.prop_of th1) [] - val tyinst = map2 (fn bef => fn iS => - (case try (assoc (TFree bef)) lambda of - SOME cty => (Thm.global_ctyp_of thy (TVar iS), cty) - | NONE => (Thm.global_ctyp_of thy (TVar iS), Thm.global_ctyp_of thy (TFree bef)) - )) tys_before tys_after + val tyinst = + map2 (fn bef => fn iS => + (case try (assoc (TFree bef)) lambda of + SOME cty => (iS, cty) + | NONE => (iS, Thm.global_ctyp_of thy (TFree bef)))) + tys_before tys_after in Thm.instantiate (tyinst,[]) th1 end @@ -334,9 +332,7 @@ val tns = map (fn (_, _) => "'") tvs val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt)) val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs)) - val cvs = map (Thm.ctyp_of ctxt) vs - val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs) - val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm + val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm in snd (Global_Theory.add_thm ((binding, thm'), []) thy) end @@ -372,7 +368,7 @@ | process (thy, state) (#"M", [s]) = let val ctxt = Variable.set_body false (Proof_Context.init_global thy) - val thm = freezeT (Global_Theory.get_thm thy s) + val thm = freezeT thy (Global_Theory.get_thm thy s) val ((_, [th']), _) = Variable.import true [thm] ctxt in setth th' (thy, state) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Mon Jul 06 14:27:03 2015 +0200 @@ -34,7 +34,7 @@ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(cv, ct)]) thm end + in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end in fun instantiate_elim thm = @@ -215,7 +215,7 @@ fun insert_trigger_conv [] ct = Conv.all_conv ct | insert_trigger_conv ctss ct = let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct - in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end + in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = let @@ -298,7 +298,8 @@ fun mk_weight_eq w = let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) in - Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq + Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)]) + weight_eq end fun add_weight_conv NONE _ = Conv.all_conv diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_smt_utils.ML --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Mon Jul 06 14:27:03 2015 +0200 @@ -152,7 +152,7 @@ val destT1 = hd o Thm.dest_ctyp val destT2 = hd o tl o Thm.dest_ctyp -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_z3_proof_literals.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Mon Jul 06 14:27:03 2015 +0200 @@ -195,7 +195,9 @@ fun on_cprop f thm = f (Thm.cprop_of thm) fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm) fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 = - Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule + Thm.instantiate ([], + [(dest_Var (Thm.term_of cv1), on_cprop f thm1), + (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule |> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2 fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct) @@ -303,7 +305,7 @@ |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) end - val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})) + val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})))) fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE} in fun contradict conj ct = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_z3_proof_parser.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Mon Jul 06 14:27:03 2015 +0200 @@ -109,7 +109,7 @@ val max = fold (Integer.max o fst) vars 0 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) fun mk (i, v) = - (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) + (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) in map mk vars end fun close ctxt (ct, vars) = @@ -161,7 +161,10 @@ if null vars then ([], vars) else fold part vars ([], []) - in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end + in + (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct, + (maxidx', vars' @ all_vars)) + end in fun mk_fun f ts = let val (cts, (_, vars)) = fold_map prep ts (0, []) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Mon Jul 06 14:27:03 2015 +0200 @@ -625,7 +625,10 @@ val vs = frees_of ctxt (Thm.term_of ct) val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt val vars_of = get_vars Term.add_vars Var (K true) ctxt' - in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end + in + (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm, + ctxt') + end val sk_rules = @{lemma "c = (SOME x. P x) ==> (EX x. P x) = P c" diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/Old_SMT/old_z3_proof_tools.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Mon Jul 06 14:27:03 2015 +0200 @@ -27,7 +27,7 @@ (Proof.context -> cterm -> thm) -> cterm -> thm (*a faster COMP*) - type compose_data + type compose_data = cterm list * (cterm -> cterm list) * thm val precompose: (cterm -> cterm list) -> thm -> compose_data val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data val compose: compose_data -> thm -> thm @@ -257,11 +257,11 @@ fun list2 (x, y) = [x, y] -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) -fun precompose2 f rule = precompose (list2 o f) rule +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule) +fun precompose2 f rule : compose_data = precompose (list2 o f) rule fun compose (cvs, f, rule) thm = - discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) + discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/cconv.ML Mon Jul 06 14:27:03 2015 +0200 @@ -182,7 +182,7 @@ ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct | _ => cv ct) -fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong +fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong (*rewrite B in A1 \ ... \ An \ B*) fun concl_cconv 0 cv ct = cv ct @@ -202,10 +202,10 @@ NONE => (As, B) | SOME (A,B) => strip_prems (i - 1) (A::As) B val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] - val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp} + val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp} val th1 = cv prem RS rewr_imp_concl val nprems = Thm.nprems_of th1 - fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl + fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl fun f p th = (th RS inst_cut_rl p) |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq})) in fold f prems th1 end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Mon Jul 06 14:27:03 2015 +0200 @@ -304,15 +304,15 @@ (Pv, Dv, Sign.typ_match thy (Dty, ty) Vartab.empty) | _ => error "not a valid case thm"; - val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) + val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest type_insts); - val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv); - val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv); + val Pv = dest_Var (Envir.subst_term_types type_insts Pv); + val Dv = dest_Var (Envir.subst_term_types type_insts Dv); in Conv.fconv_rule Drule.beta_eta_conversion (case_thm |> Thm.instantiate (type_cinsts, []) - |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])) + |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)])) end; @@ -1124,11 +1124,11 @@ local (* this is fragile *) val prop = Thm.prop_of spec val x = hd (tl (Misc_Legacy.term_vars prop)) - val cTV = Thm.ctyp_of @{context} (type_of x) + val TV = dest_TVar (type_of x) val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec in fun SPEC tm thm = - let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec + let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec in thm RS (Thm.forall_elim tm gspec') end end; @@ -1141,11 +1141,11 @@ local val prop = Thm.prop_of allI val [P] = Misc_Legacy.add_term_vars (prop, []) - fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty)) + fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty)) fun ctm_theta ctxt = map (fn (i, (_, tm2)) => let val ctm2 = Thm.cterm_of ctxt tm2 - in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end) + in ((i, Thm.typ_of_cterm ctm2), ctm2) end) fun certify ctxt (ty_theta,tm_theta) = (cty_theta ctxt (Vartab.dest ty_theta), ctm_theta ctxt (Vartab.dest tm_theta)) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Mon Jul 06 14:27:03 2015 +0200 @@ -483,7 +483,7 @@ fun real_not_eq_conv ct = let val (l,r) = dest_eq (Thm.dest_arg ct) - val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th + val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th))) val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x @@ -729,9 +729,9 @@ val pth_max = instantiate' [SOME @{ctyp real}] [] max_split val pth_min = instantiate' [SOME @{ctyp real}] [] min_split val abs_tm = @{cterm "abs :: real => _"} - val p_tm = @{cpat "?P :: real => bool"} - val x_tm = @{cpat "?x :: real"} - val y_tm = @{cpat "?y::real"} + val p_v = (("P", 0), @{typ "real \ bool"}) + val x_v = (("x", 0), @{typ real}) + val y_v = (("y", 0), @{typ real}) val is_max = is_binop @{cterm "max :: real => _"} val is_min = is_binop @{cterm "min :: real => _"} fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm @@ -746,16 +746,16 @@ val elim_abs = eliminate_construct is_abs (fn p => fn ax => - Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs) + Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs) val elim_max = eliminate_construct is_max (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) + in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_max end) val elim_min = eliminate_construct is_min (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) + in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_min end) in first_conv [elim_abs, elim_max, elim_min, all_conv] end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Mon Jul 06 14:27:03 2015 +0200 @@ -265,15 +265,13 @@ let fun instantiate_normalize_env ctxt env thm = let - fun certs f = map (apply2 (f ctxt)) val prop = Thm.prop_of thm val norm_type = Envir.norm_type o Envir.type_env val insts = Term.add_vars prop [] - |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x))) - |> certs Thm.cterm_of + |> map (fn x as (s, T) => + ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) val tyinsts = Term.add_tvars prop [] - |> map (fn x => (TVar x, norm_type env (TVar x))) - |> certs Thm.ctyp_of + |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) in Drule.instantiate_normalize (tyinsts, insts) thm end fun unify_with_rhs context to env thm = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Mon Jul 06 14:27:03 2015 +0200 @@ -315,8 +315,8 @@ end fun conv_subst thy (subst : Type.tyenv) = - map (fn (iname, (sort, ty)) => (Thm.global_ctyp_of thy (TVar (iname, sort)), Thm.global_ctyp_of thy ty)) - (Vartab.dest subst) + map (fn (iname, (sort, ty)) => ((iname, sort), Thm.global_ctyp_of thy ty)) + (Vartab.dest subst) fun add_monos thy monocs pats ths = let diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Mon Jul 06 14:27:03 2015 +0200 @@ -258,8 +258,9 @@ local val pth_zero = @{thm norm_zero} - val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) - pth_zero + val tv_n = + (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) + pth_zero val concl = Thm.dest_arg o Thm.cprop_of fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = let @@ -356,7 +357,7 @@ val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1)) val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1]) val cps = map (swap o Thm.dest_equals) (cprems_of th11) - val th12 = Drule.instantiate_normalize ([], cps) th11 + val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11 val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12; in hd (Variable.export ctxt' ctxt [th13]) end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Jul 06 14:27:03 2015 +0200 @@ -332,7 +332,7 @@ fun thms_of all thy = filter - (fn th => (all orelse Context.theory_name (Thm.theory_of_thm th) = Context.theory_name thy) + (fn th => (all orelse Thm.theory_name_of_thm th = Context.theory_name thy) (* andalso is_executable_thm thy th *)) (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false))) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Jul 06 14:27:03 2015 +0200 @@ -153,7 +153,7 @@ fun theorems_of thy = filter (fn (name, th) => not (is_forbidden_theorem name) andalso - (Thm.theory_of_thm th, thy) |> apply2 Context.theory_name |> op =) + Thm.theory_name_of_thm th = Context.theory_name thy) (Global_Theory.all_thms_of thy true) fun check_formulas tsp = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Jul 06 14:27:03 2015 +0200 @@ -1390,13 +1390,13 @@ end); val induct_aux' = Thm.instantiate ([], - map (fn (s, v as Var (_, T)) => - (Thm.global_cterm_of thy9 v, Thm.global_cterm_of thy9 (Free (s, T)))) + map (fn (s, Var (v as (_, T))) => + (v, Thm.global_cterm_of thy9 (Free (s, T)))) (pnames ~~ map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @ map (fn (_, f) => let val f' = Logic.varify_global f - in (Thm.global_cterm_of thy9 f', + in (dest_Var f', Thm.global_cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f'))) end) fresh_fs) induct_aux; @@ -1562,7 +1562,7 @@ (augment_sort thy1 pt_cp_sort (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) (fn {context = ctxt, ...} => dtac (Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), permT)), + [((("pi", 0), permT), Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) in (ths, ths') end) dt_atomTs); @@ -1653,7 +1653,7 @@ SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY [cut_facts_tac [rec_prem] 1, rtac (Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), mk_permT aT)), + [((("pi", 0), mk_permT aT), Thm.global_cterm_of thy11 (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1, asm_simp_tac (put_simpset HOL_ss context addsimps @@ -1872,8 +1872,7 @@ val l = find_index (equal T) dt_atomTs; val th = nth (nth rec_equiv_thms' l) k; val th' = Thm.instantiate ([], - [(Thm.global_cterm_of thy11 (Var (("pi", 0), U)), - Thm.global_cterm_of thy11 p)]) th; + [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th; in rtac th' 1 end; val th' = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jul 06 14:27:03 2015 +0200 @@ -31,7 +31,10 @@ (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun res_inst_tac_term ctxt = - gen_res_inst_tac_term ctxt (curry Thm.instantiate); + gen_res_inst_tac_term ctxt (fn instT => fn inst => + Thm.instantiate + (map (apfst (dest_TVar o Thm.typ_of)) instT, + map (apfst (dest_Var o Thm.term_of)) inst)); fun res_inst_tac_term' ctxt = gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) []; @@ -146,10 +149,10 @@ fun inst_fresh vars params i st = let val vars' = Misc_Legacy.term_vars (Thm.prop_of st); in case subtract (op =) vars vars' of - [x] => + [Var v] => Seq.single (Thm.instantiate ([], - [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st) + [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st) | _ => error "fresh_fun_simp: Too many variables, please report." end in diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Jul 06 14:27:03 2015 +0200 @@ -338,7 +338,8 @@ val pis'' = fold (concat_perm #> map) pis' pis; val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp) (Vartab.empty, Vartab.empty); - val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy)) + val ihyp' = Thm.instantiate ([], + map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t)) (map (Envir.subst_term env) vs ~~ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Jul 06 14:27:03 2015 +0200 @@ -146,9 +146,7 @@ fun inst_params thy (vs, p) th cts = let val env = Pattern.first_order_match thy (p, Thm.prop_of th) (Vartab.empty, Vartab.empty) - in Thm.instantiate ([], - map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th - end; + in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end; fun prove_strong_ind s alt_name avoids ctxt = let diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Jul 06 14:27:03 2015 +0200 @@ -18,7 +18,7 @@ val subtractProver : Proof.context -> term -> cterm -> thm -> thm val distinct_simproc : string list -> simproc - val discharge : thm list -> thm -> thm + val discharge : Proof.context -> thm list -> thm -> thm end; structure DistinctTreeProver : DISTINCT_TREE_PROVER = @@ -95,7 +95,11 @@ fun mapT_and_recertify ct = (Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))); val insts' = map (apfst mapT_and_recertify) insts; - in Thm.instantiate (instTs, insts') end; + in + Thm.instantiate + (map (apfst (dest_TVar o Thm.typ_of)) instTs, + map (apfst (dest_Var o Thm.term_of)) insts') + end; fun tvar_clash ixn S S' = raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []); @@ -140,18 +144,14 @@ in mtch env (t, ct) end; -fun discharge prems rule = +fun discharge ctxt prems rule = let - val thy = Thm.theory_of_thm (hd prems); val (tyinsts,insts) = fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []); - val tyinsts' = - map (fn (v, (S, U)) => - (Thm.global_ctyp_of thy (TVar (v, S)), Thm.global_ctyp_of thy U)) tyinsts; + map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts; val insts' = - map (fn (idxn, ct) => - (Thm.global_cterm_of thy (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts; + map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts; val rule' = Thm.instantiate (tyinsts', insts') rule; in fold Thm.elim_implies prems rule' end; @@ -203,7 +203,7 @@ let val rule = (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}) - in dist_subtree ps (discharge [thm] rule) end; + in dist_subtree ps (discharge ctxt [thm] rule) end; val (ps, x_rest, y_rest) = split_common_prefix x_path y_path; val dist_subtree_thm = dist_subtree ps dist_thm; @@ -227,7 +227,7 @@ instantiate ctxt [(Thm.ctyp_of_cterm x_in_set_left, xT)] [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left}; - in discharge [in_set_l] in_set_left' end + in discharge ctxt [in_set_l] in_set_left' end | Right :: ps' => let val in_set_r = in_set ps' r; @@ -235,15 +235,17 @@ instantiate ctxt [(Thm.ctyp_of_cterm x_in_set_right, xT)] [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right}; - in discharge [in_set_r] in_set_right' end) + in discharge ctxt [in_set_r] in_set_right' end) end; fun in_set' [] = raise TERM ("distinctTreeProver", []) | in_set' (Left :: ps) = in_set ps l | in_set' (Right :: ps) = in_set ps r; - fun distinct_lr node_in_set Left = discharge [dist_subtree_thm, node_in_set] @{thm distinct_left} - | distinct_lr node_in_set Right = discharge [dist_subtree_thm, node_in_set] @{thm distinct_right} + fun distinct_lr node_in_set Left = + discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_left} + | distinct_lr node_in_set Right = + discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_right} val (swap, neq) = (case x_rest of @@ -262,22 +264,24 @@ in (case xr of Left => - (false, discharge [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right}) + (false, + discharge ctxt [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right}) | Right => - (true, discharge [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right})) + (true, + discharge ctxt [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right})) end)); - in if swap then discharge [neq] @{thm swap_neq} else neq end; + in if swap then discharge ctxt [neq] @{thm swap_neq} else neq end; -fun deleteProver dist_thm [] = @{thm delete_root} OF [dist_thm] - | deleteProver dist_thm (p::ps) = +fun deleteProver _ dist_thm [] = @{thm delete_root} OF [dist_thm] + | deleteProver ctxt dist_thm (p::ps) = let val dist_rule = (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}); - val dist_thm' = discharge [dist_thm] dist_rule; + val dist_thm' = discharge ctxt [dist_thm] dist_rule; val del_rule = (case p of Left => @{thm delete_left} | Right => @{thm delete_right}); - val del = deleteProver dist_thm' ps; - in discharge [dist_thm, del] del_rule end; + val del = deleteProver ctxt dist_thm' ps; + in discharge ctxt [dist_thm, del] del_rule end; local val (alpha, v) = @@ -286,7 +290,7 @@ @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp; - in (alpha, #1 (dest_Var (Thm.term_of ct))) end; + in (dest_TVar (Thm.typ_of alpha), #1 (dest_Var (Thm.term_of ct))) end; in fun subtractProver ctxt (Const (@{const_name Tip}, T)) ct dist_thm = @@ -296,20 +300,20 @@ in Thm.instantiate ([(alpha, Thm.ctyp_of ctxt alphaI)], - [(Thm.cterm_of ctxt (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip} + [((v, treeT alphaI), ct')]) @{thm subtract_Tip} end | subtractProver ctxt (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm = let val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val (_, [cl, _, _, cr]) = Drule.strip_comb ct; val ps = the (find_tree x (Thm.term_of ct')); - val del_tree = deleteProver dist_thm ps; - val dist_thm' = discharge [del_tree, dist_thm] @{thm delete_Some_all_distinct}; + val del_tree = deleteProver ctxt dist_thm ps; + val dist_thm' = discharge ctxt [del_tree, dist_thm] @{thm delete_Some_all_distinct}; val sub_l = subtractProver ctxt (Thm.term_of cl) cl (dist_thm'); val sub_r = subtractProver ctxt (Thm.term_of cr) cr - (discharge [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res}); - in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end; + (discharge ctxt [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res}); + in discharge ctxt [del_tree, sub_l, sub_r] @{thm subtract_Node} end; end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Jul 06 14:27:03 2015 +0200 @@ -1029,12 +1029,14 @@ val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name +(* FIXME !???! fun rtac_wrap thm_f i = fn st => let val thy = Thm.theory_of_thm st in rtac (thm_f thy) i st end +*) (*Some nodes don't have an inference name, such as the conjecture, definitions and axioms. Such nodes shouldn't appear in the @@ -1063,14 +1065,7 @@ let fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string) val reconstructed_inference = thm ctxt' - val rec_inf_tac = fn st => - let - val ctxt = - Thm.theory_of_thm st - |> Proof_Context.init_global - in - HEADGOAL (rtac (thm ctxt)) st - end + fun rec_inf_tac st = HEADGOAL (rtac (thm ctxt')) st in (reconstructed_inference, rec_inf_tac) end) @@ -1157,14 +1152,16 @@ else let val maybe_thm = ignore_interpretation_exn try_make_step ctxt +(* FIXME !???! val ctxt' = if is_some maybe_thm then the maybe_thm |> #1 |> Thm.theory_of_thm |> Proof_Context.init_global else ctxt +*) in - (maybe_thm, ctxt') + (maybe_thm, ctxt) end in (thm, (node, thm) :: memo, ctxt') end | SOME maybe_thm => (maybe_thm, memo, ctxt) @@ -1183,8 +1180,7 @@ (hd skel, Thm.prop_of (def_thm thy) |> SOME, - SOME (def_thm thy, - HEADGOAL (rtac_wrap def_thm))) :: rest memo ctxt + SOME (def_thm thy, HEADGOAL (rtac (def_thm thy)))) :: rest memo ctxt end | Axiom n => let diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Mon Jul 06 14:27:03 2015 +0200 @@ -570,14 +570,14 @@ diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t) (*valuation of type variables*) - val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing + val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing val typeval_env = map (apfst dest_TVar) type_pairing (*valuation of term variables*) val termval = - map (apfst (type_devar typeval_env)) term_pairing - |> map (apply2 (Thm.cterm_of ctxt)) + map (apfst (dest_Var o type_devar typeval_env)) term_pairing + |> map (apsnd (Thm.cterm_of ctxt)) in Thm.instantiate (typeval, termval) scheme_thm end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Jul 06 14:27:03 2015 +0200 @@ -950,8 +950,8 @@ val tactic = if is_none var_opt then no_tac else - fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac - + fold (curry (op APPEND)) + (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac in tactic st end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Mon Jul 06 14:27:03 2015 +0200 @@ -329,10 +329,8 @@ *} ML {* -(*given a thm, show us the axioms in its thy*) -val axms_of_thy_of_thm = - Thm.theory_of_thm - #> ` Theory.axioms_of +val axms_of_thy = + `Theory.axioms_of #> apsnd cterm_of #> swap #> apsnd (map snd) @@ -351,14 +349,8 @@ *} ML {* -fun leo2_tac_wrap prob_name step i = fn st => - let - val ctxt = - Thm.theory_of_thm st - |> Proof_Context.init_global - in - rtac (interpret_leo2_inference ctxt prob_name step) i st - end +fun leo2_tac_wrap ctxt prob_name step i st = + rtac (interpret_leo2_inference ctxt prob_name step) i st *} (*FIXME move these examples elsewhere*) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Mon Jul 06 14:27:03 2015 +0200 @@ -7,7 +7,7 @@ - Makes use of the PolyML structure. *) -theory TPTP_Proof_Reconstruction_Test +theory TPTP_Proof_Reconstruction_Test_Units imports TPTP_Test TPTP_Proof_Reconstruction begin @@ -482,16 +482,7 @@ (\ SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) = False" (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*) -by (tactic {*fn thm => - let - val ctxt = - theory_of_thm thm - |> Context.Theory - |> Context.proof_of - in nonfull_extcnf_combined_tac ctxt [Extuni_Func, Existential_Var] thm - end*}) -(*by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*})*) -oops +by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*}) consts SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind" diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 06 14:27:03 2015 +0200 @@ -166,7 +166,7 @@ val facts = Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false Keyword.empty_keywords [] [] css_table - |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd) + |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd) val problem = facts |> map (fn ((_, loc), th) => diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Mon Jul 06 14:27:03 2015 +0200 @@ -54,7 +54,7 @@ val css = clasimpset_rule_table_of ctxt val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css - val name_tabs = build_name_tables nickname_of_thm facts + val name_tabs = build_name_tables (nickname_of_thm ctxt) facts fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_str (j, s) = s ^ "@" ^ string_of_int j @@ -90,12 +90,12 @@ [name] => name | names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ ".")) val th = - case find_first (fn (_, th) => nickname_of_thm th = name) facts of + case find_first (fn (_, th) => nickname_of_thm ctxt th = name) facts of SOME (_, th) => th | NONE => error ("No fact called \"" ^ name ^ "\".") val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt - val isar_deps = these (isar_dependencies_of name_tabs th) + val isar_deps = these (isar_dependencies_of ctxt name_tabs th) val suggss = isar_deps :: suggss0 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) @@ -116,7 +116,7 @@ else let fun nickify ((_, stature), th) = - ((K (encode_str (nickname_of_thm th)), stature), th) + ((K (encode_str (nickname_of_thm ctxt th)), stature), th) val facts = suggs diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/TPTP/mash_export.ML Mon Jul 06 14:27:03 2015 +0200 @@ -58,14 +58,14 @@ | _ => ("", [])) fun has_thm_thy th thy = - Context.theory_name thy = Context.theory_name (Thm.theory_of_thm th) + Context.theory_name thy = Thm.theory_name_of_thm th fun has_thys thys th = exists (has_thm_thy th) thys fun all_facts ctxt = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css - |> sort (crude_thm_ord o apply2 snd) + |> sort (crude_thm_ord ctxt o apply2 snd) end fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) @@ -82,8 +82,8 @@ val facts = all_facts ctxt |> filter_out (has_thys thys o snd) - |> attach_parents_to_facts [] - |> map (apsnd (nickname_of_thm o snd)) + |> attach_parents_to_facts ctxt [] + |> map (apsnd (nickname_of_thm ctxt o snd)) in File.write path ""; List.app do_fact facts @@ -97,8 +97,8 @@ fun do_fact ((_, stature), th) = let - val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th] + val name = nickname_of_thm ctxt th + val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s @@ -124,7 +124,7 @@ let val deps = (case isar_deps_opt of - NONE => isar_dependencies_of name_tabs th + NONE => isar_dependencies_of ctxt name_tabs th | deps => deps) in (case deps of @@ -142,12 +142,12 @@ let val path = Path.explode file_name val facts = filter_out (has_thys thys o snd) (all_facts ctxt) - val name_tabs = build_name_tables nickname_of_thm facts + val name_tabs = build_name_tables (nickname_of_thm ctxt) facts fun do_fact (j, (_, th)) = if in_range range j then let - val name = nickname_of_thm th + val name = nickname_of_thm ctxt th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val access_facts = filter_accessible_from th facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE @@ -180,22 +180,22 @@ val path = Path.explode file_name val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) - val name_tabs = build_name_tables nickname_of_thm facts + val name_tabs = build_name_tables (nickname_of_thm ctxt) facts fun do_fact (j, (name, (parents, ((_, stature), th)))) = if in_range range j then let val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) - val isar_deps = isar_dependencies_of name_tabs th + val isar_deps = isar_dependencies_of ctxt name_tabs th val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps) - val goal_feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th] + val goal_feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_of_thm th) stature + |> features_of ctxt (Thm.theory_name_of_thm th) stature |> map (rpair (weight * extra_feature_factor)) val query = @@ -224,7 +224,9 @@ "" val new_facts = - new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd)) + new_facts + |> attach_parents_to_facts ctxt old_facts + |> map (`(nickname_of_thm ctxt o snd o snd)) val lines = map do_fact (tag_list 1 new_facts) in File.write_list path lines @@ -243,16 +245,16 @@ val path = Path.explode file_name val facts = all_facts ctxt val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) - val name_tabs = build_name_tables nickname_of_thm facts + val name_tabs = build_name_tables (nickname_of_thm ctxt) facts fun do_fact (j, ((_, th), old_facts)) = if in_range range j then let - val name = nickname_of_thm th + val name = nickname_of_thm ctxt th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt - val isar_deps = isar_dependencies_of name_tabs th + val isar_deps = isar_dependencies_of ctxt name_tabs th in if is_bad_query ctxt ho_atp step j th isar_deps then "" @@ -261,9 +263,9 @@ val suggs = old_facts |> filter_accessible_from th - |> mepo_or_mash_suggested_facts ctxt (Thm.theory_of_thm th) params max_suggs hyp_ts - concl_t - |> map (nickname_of_thm o snd) + |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name_of_thm th) + params max_suggs hyp_ts concl_t + |> map (nickname_of_thm ctxt o snd) in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end @@ -288,11 +290,11 @@ (Options.put_default @{system_option MaSh} algorithm; Sledgehammer_MaSh.mash_unlearn (); generate_mepo_or_mash_suggestions - (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts => - fn concl_t => + (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} => + fn max_suggs => fn hyp_ts => fn concl_t => tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false Sledgehammer_Util.one_year) - #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t + #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t #> fst)) fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jul 06 14:27:03 2015 +0200 @@ -607,9 +607,9 @@ let val n = Thm.nprems_of coind; val m = Thm.nprems_of (hd rel_monos) - n; - fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi))))) - |> apply2 (Thm.cterm_of ctxt); - val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var); + fun mk_inst phi = + (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi)))))) + val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst; fun mk_unfold rel_eq rel_mono = let val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl]; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jul 06 14:27:03 2015 +0200 @@ -685,7 +685,9 @@ let val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; - val rho_As = map (apply2 (Thm.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As); + val rho_As = + map (fn (T, U) => (dest_TVar T, Thm.ctyp_of lthy U)) + (map Logic.varifyT_global As ~~ As); fun inst_thm t thm = Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)] diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Function/function.ML Mon Jul 06 14:27:03 2015 +0200 @@ -98,7 +98,7 @@ fun afterqed [[proof]] lthy = let - val result = cont (Thm.close_derivation proof) + val result = cont lthy (Thm.close_derivation proof) val FunctionResult {fs, R, dom, psimps, simple_pinducts, termination, domintros, cases, ...} = result diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Mon Jul 06 14:27:03 2015 +0200 @@ -15,7 +15,7 @@ -> local_theory -> (term (* f *) * thm (* goalstate *) - * (thm -> Function_Common.function_result) (* continuation *) + * (Proof.context -> thm -> Function_Common.function_result) (* continuation *) ) * local_theory end @@ -893,11 +893,8 @@ (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm - fun mk_partial_rules provedgoal = + fun mk_partial_rules newctxt provedgoal = let - val newthy = Thm.theory_of_thm provedgoal (*FIXME*) - val newctxt = Proof_Context.init_global newthy (*FIXME*) - val (graph_is_function, complete_thm) = provedgoal |> Conjunction.elim diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Mon Jul 06 14:27:03 2015 +0200 @@ -12,7 +12,7 @@ -> term list -> local_theory -> ((thm (* goalstate *) - * (thm -> Function_Common.function_result) (* proof continuation *) + * (Proof.context -> thm -> Function_Common.function_result) (* proof continuation *) ) * local_theory) end @@ -310,7 +310,7 @@ val (mutual', lthy'') = define_projections fixes mutual fsum lthy' - val cont' = mk_partial_rules_mutual lthy'' cont mutual' + fun cont' ctxt = mk_partial_rules_mutual lthy'' (cont ctxt) mutual' in ((goalstate, cont'), lthy'') end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Mon Jul 06 14:27:03 2015 +0200 @@ -200,7 +200,8 @@ val (P_var, x_var) = Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> strip_comb |> apsnd hd - val P_rangeT = range_type (snd (Term.dest_Var P_var)) + |> apply2 dest_Var + val P_rangeT = range_type (snd P_var) val PT = map (snd o dest_Free) args ---> P_rangeT val x_inst = cert (foldl1 HOLogic.mk_prod args) val P_inst = cert (uncurry_n (length args) (Free (P, PT))) @@ -211,7 +212,7 @@ THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 THEN CONVERSION (split_params_conv ctxt then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) - |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) + |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)]) |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |> singleton (Variable.export ctxt' ctxt) in diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Function/relation.ML Mon Jul 06 14:27:03 2015 +0200 @@ -18,8 +18,7 @@ fun inst_state_tac ctxt inst = SUBGOAL (fn (goal, _) => (case Term.add_vars goal [] of - [v as (_, T)] => - PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) + [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))])) | _ => no_tac)); fun relation_tac ctxt rel i = @@ -39,9 +38,7 @@ |> map_types Type_Infer.paramify_vars |> Type.constraint T |> Syntax.check_term ctxt; - in - PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')])) - end + in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end | _ => no_tac)); fun relation_infer_tac ctxt rel i = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Mon Jul 06 14:27:03 2015 +0200 @@ -23,7 +23,7 @@ fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars - val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars UNIVs + val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |> (fn thm => thm RS sym) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Jul 06 14:27:03 2015 +0200 @@ -310,7 +310,7 @@ val thy = Proof_Context.theory_of ctxt val (_, qty_schematic) = quot_thm_rty_qty quot_thm val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty - fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty) + fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty) val ty_inst = Vartab.fold (cons o prep_ty) match_env [] in Thm.instantiate (ty_inst, []) quot_thm diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Jul 06 14:27:03 2015 +0200 @@ -145,7 +145,7 @@ fun instT_thm ctxt env = let val cinst = env |> Vartab.dest - |> map (fn (x, (S, T)) => (Thm.ctyp_of ctxt (TVar (x, S)), Thm.ctyp_of ctxt T)); + |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)); in Thm.instantiate (cinst, []) end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Mon Jul 06 14:27:03 2015 +0200 @@ -346,16 +346,17 @@ (*Replaces universally quantified variables by FREE variables -- because assumptions may not contain scheme variables. Later, generalize using Variable.export. *) local - val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); - val spec_varT = Thm.typ_of_cterm spec_var; - fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu; + val spec_var = + Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))) + |> Thm.term_of |> dest_Var; + fun name_of (Const (@{const_name All}, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu; in fun freeze_spec th ctxt = let val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt; val spec' = spec - |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]); + |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]); in (th RS spec', ctxt') end end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Jul 06 14:27:03 2015 +0200 @@ -44,10 +44,10 @@ "Sledgehammer_Util".) *) fun transform_elim_theorem th = (case Thm.concl_of th of (*conclusion variable*) - @{const Trueprop} $ (v as Var (_, @{typ bool})) => - Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th - | v as Var(_, @{typ prop}) => - Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th + @{const Trueprop} $ (Var (v as (_, @{typ bool}))) => + Thm.instantiate ([], [(v, cfalse)]) th + | Var (v as (_, @{typ prop})) => + Thm.instantiate ([], [(v, ctp_false)]) th | _ => th) @@ -375,9 +375,7 @@ th ctxt val (cnf_ths, ctxt) = clausify nnf_th fun intr_imp ct th = - Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt)) - [(Var (("i", 0), @{typ nat}), - HOLogic.mk_nat ax_no)]) + Thm.instantiate ([], [((("i", 0), @{typ nat}), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))]) (zero_var_indexes @{thm skolem_COMBK_D}) RS Thm.implies_intr ct th in diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jul 06 14:27:03 2015 +0200 @@ -174,7 +174,7 @@ fun incr_type_indexes ctxt inc th = let val tvs = Term.add_tvars (Thm.full_prop_of th) [] - fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s)) + fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s))) in Thm.instantiate (map inc_tvar tvs, []) th end @@ -211,7 +211,7 @@ |> rpair (Envir.empty ~1) |-> fold (Pattern.unify (Context.Proof ctxt)) |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)) + |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)) in (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as @@ -400,8 +400,8 @@ val thy = Proof_Context.theory_of ctxt val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T) - fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t) + fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T) + fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t) val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] @@ -570,11 +570,11 @@ Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, tenv = Vartab.empty, tyenv = tyenv} val ty_inst = - Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))) + Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T))) tyenv [] val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')] in - Drule.instantiate_normalize (ty_inst, t_inst) th + Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th end | _ => raise Fail "expected a single non-zapped, non-Metis Var") in diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Jul 06 14:27:03 2015 +0200 @@ -232,10 +232,10 @@ fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) = let - fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t) + fun inst_pair_of (ix, (ty, t)) = ((ix, ty), t) fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) - |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of) + |> snd |> Vartab.dest |> map (apsnd (Thm.cterm_of ctxt2) o inst_pair_of) val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems) val case_th = rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Jul 06 14:27:03 2015 +0200 @@ -150,10 +150,10 @@ val get_pmi = get_pmi_term o Thm.cprop_of; -val p_v' = @{cpat "?P' :: int => bool"}; -val q_v' = @{cpat "?Q' :: int => bool"}; -val p_v = @{cpat "?P:: int => bool"}; -val q_v = @{cpat "?Q:: int => bool"}; +val p_v' = (("P'", 0), @{typ "int \ bool"}); +val q_v' = (("Q'", 0), @{typ "int \ bool"}); +val p_v = (("P", 0), @{typ "int \ bool"}); +val q_v = (("Q", 0), @{typ "int \ bool"}); fun myfwd (th1, th2, th3) p q [(th_1,th_2,th_3), (th_1',th_2',th_3')] = @@ -430,11 +430,13 @@ val insert_tm = @{cterm "insert :: int => _"}; fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; -val [A_tm,B_tm] = map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg - |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg) - [asetP,bsetP]; +val [A_v,B_v] = + map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg + |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg + |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg + |> Thm.term_of |> dest_Var) [asetP, bsetP]; -val D_tm = @{cpat "?D::int"}; +val D_v = (("D", 0), @{typ int}); fun cooperex_conv ctxt vs q = let @@ -501,16 +503,16 @@ if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) then (bl,b0,decomp_minf, - fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) + fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp) [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ - (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) + (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)])) [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, bsetdisj,infDconj, infDdisj]), cpmi) else (al,a0,decomp_pinf,fn A => - (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) + (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp) [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ - (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) + (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)])) [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, asetdisj,infDconj, infDdisj]),cppi) val cpth = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Quickcheck/find_unused_assms.ML --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Mon Jul 06 14:27:03 2015 +0200 @@ -13,8 +13,9 @@ structure Find_Unused_Assms : FIND_UNUSED_ASSMS = struct -fun thms_of thy thy_name = Global_Theory.all_thms_of thy false - |> filter (fn (_, th) => Context.theory_name (Thm.theory_of_thm th) = thy_name) +fun thms_of thy thy_name = + Global_Theory.all_thms_of thy false + |> filter (fn (_, th) => Thm.theory_name_of_thm th = thy_name) fun do_while P f s list = if P s then diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 06 14:27:03 2015 +0200 @@ -73,7 +73,9 @@ val lhs = eq |> Thm.dest_arg1; val pt_random_aux = lhs |> Thm.dest_fun; val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun; -val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1; +val a_v = + pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1 + |> Thm.typ_of |> dest_TVar; val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one}, @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}]; @@ -89,7 +91,7 @@ (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; val Type (_, [_, iT]) = T; val icT = Thm.ctyp_of lthy iT; - val inst = Thm.instantiate_cterm ([(aT, icT)], []); + val inst = Thm.instantiate_cterm ([(a_v, icT)], []); fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t); val t_rhs = lambda t_k proto_t_rhs; val eqs0 = [subst_v @{term "0::natural"} eq, @@ -98,11 +100,11 @@ val ((_, (_, eqs2)), lthy') = lthy |> BNF_LFP_Compat.primrec_simple [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1; - val cT_random_aux = inst pt_random_aux; - val cT_rhs = inst pt_rhs; + val cT_random_aux = inst pt_random_aux |> Thm.term_of |> dest_Var; + val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var; val rule = @{thm random_aux_rec} |> Drule.instantiate_normalize - ([(aT, icT)], + ([(a_v, icT)], [(cT_random_aux, Thm.cterm_of lthy' t_random_aux), (cT_rhs, Thm.cterm_of lthy' t_rhs)]); fun tac ctxt = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jul 06 14:27:03 2015 +0200 @@ -72,20 +72,16 @@ | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." -fun prep_trm thy (x, (T, t)) = - (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty) - fun get_match_inst thy pat trm = let val univ = Unify.matchers (Context.Theory thy) [(pat, trm)] val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) + fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty) + fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t) in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) + (map prep_ty tyenv, map prep_trm tenv) end (* Calculates the instantiations for the lemmas: @@ -480,7 +476,7 @@ then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) val thm4 = - Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3 + Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3 in Conv.rewr_conv thm4 ctrm end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Jul 06 14:27:03 2015 +0200 @@ -35,7 +35,7 @@ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(cv, ct)]) thm end + in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end in fun instantiate_elim thm = @@ -199,8 +199,10 @@ fun insert_trigger_conv [] ct = Conv.all_conv ct | insert_trigger_conv ctss ct = - let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct - in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end + let + val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct + val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)] + in Thm.instantiate ([], inst) trigger_eq end fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = let diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/SMT/smt_util.ML --- a/src/HOL/Tools/SMT/smt_util.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/SMT/smt_util.ML Mon Jul 06 14:27:03 2015 +0200 @@ -171,7 +171,7 @@ val destT1 = hd o Thm.dest_ctyp val destT2 = hd o tl o Thm.dest_ctyp -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/SMT/z3_replay_methods.ML --- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Mon Jul 06 14:27:03 2015 +0200 @@ -100,20 +100,20 @@ (Vartab.empty, Vartab.empty) |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t) -fun gen_certify_inst sel mk cert ctxt thm t = +fun gen_certify_inst sel cert ctxt thm t = let val inst = match ctxt (dest_thm thm) (dest_prop t) - fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b) + fun cert_inst (ix, (a, b)) = ((ix, a), cert b) in Vartab.fold (cons o cert_inst) (sel inst) [] end fun match_instantiateT ctxt t thm = if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then - Thm.instantiate (gen_certify_inst fst TVar (Thm.ctyp_of ctxt) ctxt thm t, []) thm + Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm else thm fun match_instantiate ctxt t thm = let val thm' = match_instantiateT ctxt t thm in - Thm.instantiate ([], gen_certify_inst snd Var (Thm.cterm_of ctxt) ctxt thm' t) thm' + Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm' end fun apply_rule ctxt t = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/SMT/z3_replay_util.ML --- a/src/HOL/Tools/SMT/z3_replay_util.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML Mon Jul 06 14:27:03 2015 +0200 @@ -15,7 +15,7 @@ val discharge: thm -> thm -> thm (*a faster COMP*) - type compose_data + type compose_data = cterm list * (cterm -> cterm list) * thm val precompose: (cterm -> cterm list) -> thm -> compose_data val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data val compose: compose_data -> thm -> thm @@ -71,11 +71,12 @@ fun list2 (x, y) = [x, y] -fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) -fun precompose2 f rule = precompose (list2 o f) rule +fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule) +fun precompose2 f rule : compose_data = precompose (list2 o f) rule fun compose (cvs, f, rule) thm = - discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) + discharge thm + (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) (* simpset *) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 06 14:27:03 2015 +0200 @@ -45,19 +45,20 @@ val str_of_mash_algorithm : mash_algorithm -> string val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list - val nickname_of_thm : thm -> string + val nickname_of_thm : Proof.context -> thm -> string val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list - val crude_thm_ord : thm * thm -> order + val crude_thm_ord : Proof.context -> thm * thm -> order val thm_less : thm * thm -> bool val goal_of_thm : theory -> thm -> thm val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> prover_result - val features_of : Proof.context -> theory -> stature -> term list -> string list + val features_of : Proof.context -> string -> stature -> term list -> string list val trim_dependencies : string list -> string list option - val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option + val isar_dependencies_of : Proof.context -> string Symtab.table * string Symtab.table -> + thm -> string list option val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> string Symtab.table * string Symtab.table -> thm -> bool * string list - val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> + val attach_parents_to_facts : Proof.context -> ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list val num_extra_feature_facts : int val extra_feature_factor : real @@ -65,7 +66,7 @@ val weight_facts_steeply : 'a list -> ('a * real) list val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list - val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term -> + val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list val mash_unlearn : unit -> unit @@ -737,25 +738,24 @@ (*** Isabelle helpers ***) -fun elided_backquote_thm threshold th = - elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th) +fun elided_backquote_thm ctxt threshold th = + elide_string threshold (backquote_thm ctxt th) -val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm - -fun nickname_of_thm th = +fun nickname_of_thm ctxt th = if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of - SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th] + SOME suf => + Long_Name.implode [Thm.theory_name_of_thm th, suf, elided_backquote_thm ctxt 50 th] | NONE => hint) end else - elided_backquote_thm 200 th + elided_backquote_thm ctxt 200 th fun find_suggested_facts ctxt facts = let - fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) + fun add (fact as (_, th)) = Symtab.default (nickname_of_thm ctxt th, fact) val tab = fold add facts Symtab.empty fun lookup nick = Symtab.lookup tab nick @@ -778,12 +778,12 @@ EQUAL => string_ord (apply2 Context.theory_name p) | order => order) -fun crude_thm_ord p = +fun crude_thm_ord ctxt p = (case crude_theory_ord (apply2 Thm.theory_of_thm p) of EQUAL => (* The hack below is necessary because of odd dependencies that are not reflected in the theory comparison. *) - let val q = apply2 nickname_of_thm p in + let val q = apply2 (nickname_of_thm ctxt) p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q @@ -924,12 +924,10 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of ctxt thy (scope, _) ts = - let val thy_name = Context.theory_name thy in - thy_feature_of thy_name :: - term_features_of ctxt thy_name term_max_depth type_max_depth ts - |> scope <> Global ? cons local_feature - end +fun features_of ctxt thy_name (scope, _) ts = + thy_feature_of thy_name :: + term_features_of ctxt thy_name term_max_depth type_max_depth ts + |> scope <> Global ? cons local_feature (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn from such proofs. *) @@ -938,14 +936,14 @@ val prover_default_max_facts = 25 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) -val typedef_dep = nickname_of_thm @{thm CollectI} +val typedef_dep = nickname_of_thm @{context} @{thm CollectI} (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to "someI_ex" (and to some internal constructions). *) -val class_some_dep = nickname_of_thm @{thm someI_ex} +val class_some_dep = nickname_of_thm @{context} @{thm someI_ex} val fundef_ths = @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value} - |> map nickname_of_thm + |> map (nickname_of_thm @{context}) (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) val typedef_ths = @@ -953,46 +951,46 @@ type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct type_definition.Rep_range type_definition.Abs_image} - |> map nickname_of_thm + |> map (nickname_of_thm @{context}) -fun is_size_def [dep] th = +fun is_size_def ctxt [dep] th = (case first_field ".rec" dep of SOME (pref, _) => - (case first_field ".size" (nickname_of_thm th) of + (case first_field ".size" (nickname_of_thm ctxt th) of SOME (pref', _) => pref = pref' | NONE => false) | NONE => false) - | is_size_def _ _ = false + | is_size_def _ _ _ = false fun trim_dependencies deps = if length deps > max_dependencies then NONE else SOME deps -fun isar_dependencies_of name_tabs th = +fun isar_dependencies_of ctxt name_tabs th = thms_in_proof max_dependencies (SOME name_tabs) th |> Option.map (fn deps => if deps = [typedef_dep] orelse deps = [class_some_dep] orelse exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse - is_size_def deps th then + is_size_def ctxt deps th then [] else deps) fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = - (case isar_dependencies_of name_tabs th of + (case isar_dependencies_of ctxt name_tabs th of SOME [] => (false, []) | isar_deps0 => let val isar_deps = these isar_deps0 val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th - val name = nickname_of_thm th + val name = nickname_of_thm ctxt th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val facts = facts |> filter (fn (_, th') => thm_less (th', th)) - fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) + fun nickify ((_, stature), th) = ((nickname_of_thm ctxt th, stature), th) - fun is_dep dep (_, th) = nickname_of_thm th = dep + fun is_dep dep (_, th) = nickname_of_thm ctxt th = dep fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then @@ -1036,7 +1034,7 @@ (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) -fun chunks_and_parents_for chunks th = +fun chunks_and_parents_for ctxt chunks th = let fun insert_parent new parents = let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in @@ -1060,11 +1058,11 @@ in fold_rev do_chunk chunks ([], []) |>> cons [] - ||> map nickname_of_thm + ||> map (nickname_of_thm ctxt) end -fun attach_parents_to_facts _ [] = [] - | attach_parents_to_facts old_facts (facts as (_, th) :: _) = +fun attach_parents_to_facts _ _ [] = [] + | attach_parents_to_facts ctxt old_facts (facts as (_, th) :: _) = let fun do_facts _ [] = [] | do_facts (_, parents) [fact] = [(parents, fact)] @@ -1073,16 +1071,16 @@ let val chunks = app_hd (cons th) chunks val chunks_and_parents' = - if thm_less_eq (th, th') andalso thy_name_of_thm th = thy_name_of_thm th' then - (chunks, [nickname_of_thm th]) - else - chunks_and_parents_for chunks th' + if thm_less_eq (th, th') andalso + Thm.theory_name_of_thm th = Thm.theory_name_of_thm th' + then (chunks, [nickname_of_thm ctxt th]) + else chunks_and_parents_for ctxt chunks th' in (parents, fact) :: do_facts chunks_and_parents' facts end in old_facts @ facts - |> do_facts (chunks_and_parents_for [[]] th) + |> do_facts (chunks_and_parents_for ctxt [[]] th) |> drop (length old_facts) end @@ -1114,15 +1112,15 @@ fun strict_subthy thyp = Theory.subthy thyp andalso not (Theory.subthy (swap thyp)) -fun maximal_wrt_access_graph _ [] = [] - | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) = +fun maximal_wrt_access_graph _ _ [] = [] + | maximal_wrt_access_graph ctxt access_G ((fact as (_, th)) :: facts) = let val thy = Thm.theory_of_thm th in fact :: filter_out (fn (_, th') => strict_subthy (Thm.theory_of_thm th', thy)) facts - |> map (nickname_of_thm o snd) + |> map (nickname_of_thm ctxt o snd) |> maximal_wrt_graph access_G end -fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm +fun is_fact_in_graph ctxt access_G = can (Graph.get_node access_G) o nickname_of_thm ctxt val chained_feature_factor = 0.5 (* FUDGE *) val extra_feature_factor = 0.1 (* FUDGE *) @@ -1147,29 +1145,28 @@ (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown) end -fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts = +fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts = let - val thy_name = Context.theory_name thy val algorithm = the_mash_algorithm () val facts = facts - |> rev_sort_list_prefix (crude_thm_ord o apply2 snd) + |> rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd) (Int.max (num_extra_feature_facts, max_proximity_facts)) val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts - fun fact_has_right_theory (_, th) = - thy_name = Context.theory_name (Thm.theory_of_thm th) + fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name_of_thm th fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_of_thm th) stature + |> features_of ctxt (Thm.theory_name_of_thm th) stature |> map (rpair (weight * factor)) val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} = peek_state ctxt - val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts) + val goal_feats0 = + features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) @@ -1185,7 +1182,7 @@ fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) |> debug ? sort (Real.compare o swap o apply2 snd) - val parents = maximal_wrt_access_graph access_G facts + val parents = maximal_wrt_access_graph ctxt access_G facts val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents) val suggs = @@ -1205,7 +1202,7 @@ goal_feats int_goal_feats end - val unknown = filter_out (is_fact_in_graph access_G o snd) facts + val unknown = filter_out (is_fact_in_graph ctxt access_G o snd) facts in find_mash_suggestions ctxt max_suggs suggs facts chained unknown |> apply2 (map fact_of_raw_fact) @@ -1266,16 +1263,16 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = features_of ctxt thy (Local, General) [t] - val facts = rev_sort_list_prefix (crude_thm_ord o apply2 snd) 1 facts + val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t] + val facts = rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd) 1 facts in map_state ctxt (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => let - val parents = maximal_wrt_access_graph access_G facts + val parents = maximal_wrt_access_graph ctxt access_G facts val deps = used_ths - |> filter (is_fact_in_graph access_G) - |> map nickname_of_thm + |> filter (is_fact_in_graph ctxt access_G) + |> map (nickname_of_thm ctxt) val name = learned_proof_name () val (access_G', xtabs', rev_learns) = @@ -1304,7 +1301,7 @@ fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout) val {access_G, ...} = peek_state ctxt - val is_in_access_G = is_fact_in_graph access_G o snd + val is_in_access_G = is_fact_in_graph ctxt access_G o snd val no_new_facts = forall is_in_access_G facts in if no_new_facts andalso not run_prover then @@ -1318,7 +1315,7 @@ "" else let - val name_tabs = build_name_tables nickname_of_thm facts + val name_tabs = build_name_tables (nickname_of_thm ctxt) facts fun deps_of status th = if status = Non_Rec_Def orelse status = Rec_Def then @@ -1327,7 +1324,7 @@ prover_dependencies_of ctxt params prover auto_level facts name_tabs th |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) else - isar_dependencies_of name_tabs th + isar_dependencies_of ctxt name_tabs th fun do_commit [] [] [] state = state | do_commit learns relearns flops @@ -1375,8 +1372,8 @@ | learn_new_fact (parents, ((_, stature as (_, status)), th)) (learns, (num_nontrivial, next_commit, _)) = let - val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of th] + val name = nickname_of_thm ctxt th + val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] val deps = these (deps_of status th) val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns @@ -1396,8 +1393,8 @@ else let val new_facts = facts - |> sort (crude_thm_ord o apply2 snd) - |> attach_parents_to_facts [] + |> sort (crude_thm_ord ctxt o apply2 snd) + |> attach_parents_to_facts ctxt [] |> filter_out (is_in_access_G o snd) val (learns, (num_nontrivial, _, _)) = ([], (0, next_commit_time (), false)) @@ -1410,7 +1407,7 @@ | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (num_nontrivial, next_commit, _)) = let - val name = nickname_of_thm th + val name = nickname_of_thm ctxt th val (num_nontrivial, relearns, flops) = (case deps_of status th of SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops) @@ -1434,7 +1431,7 @@ fun priority_of th = Random.random_range 0 max_isar + - (case try (Graph.get_node access_G) (nickname_of_thm th) of + (case try (Graph.get_node access_G) (nickname_of_thm ctxt th) of SOME (Isar_Proof, _, deps) => ~100 * length deps | SOME (Automatic_Proof, _, _) => 2 * max_isar | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar @@ -1468,7 +1465,7 @@ val ctxt = ctxt |> Config.put instantiate_inducts false val facts = nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True} - |> sort (crude_thm_ord o apply2 snd o swap) + |> sort (crude_thm_ord ctxt o apply2 snd o swap) val num_facts = length facts val prover = hd provers @@ -1515,7 +1512,7 @@ [("", [])] else let - val thy = Proof_Context.theory_of ctxt + val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) fun maybe_launch_thread exact min_num_facts_to_learn = if not (Async_Manager_Legacy.has_running_threads MaShN) andalso @@ -1536,7 +1533,7 @@ fun please_learn () = let val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt - val is_in_access_G = is_fact_in_graph access_G o snd + val is_in_access_G = is_fact_in_graph ctxt access_G o snd val min_num_facts_to_learn = length facts - num_facts0 in if min_num_facts_to_learn <= max_facts_to_learn_before_query then @@ -1578,8 +1575,8 @@ |> weight_facts_steeply, []) fun mash () = - mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t - facts + mash_suggested_facts ctxt thy_name params + (generous_max_suggestions max_facts) hyp_ts concl_t facts |>> weight_facts_steeply val mess = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Jul 06 14:27:03 2015 +0200 @@ -220,7 +220,7 @@ t fun theory_const_prop_of fudge th = - theory_constify fudge (Context.theory_name (Thm.theory_of_thm th)) (Thm.prop_of th) + theory_constify fudge (Thm.theory_name_of_thm th) (Thm.prop_of th) fun pair_consts_fact thy fudge fact = (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Mon Jul 06 14:27:03 2015 +0200 @@ -592,11 +592,10 @@ fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms fst ctxt' tab s t val binsts = bool_insts (if equiv then 0 else 1) (s, t) - val cbool = @{ctyp bool} - val relT = @{typ "bool => bool => bool"} val idx = Thm.maxidx_of thm + 1 - fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool) - fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t) + fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool}) + fun inst (a, t) = + ((Name.clean_index (prep a, idx), @{typ "bool \ bool \ bool"}), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (tfrees, rnames @ frees) idx @@ -616,11 +615,10 @@ fun prep a = the (AList.lookup (op =) tab a) val thm = transfer_rule_of_terms snd ctxt' tab t s val binsts = bool_insts 1 (s, t) - val cbool = @{ctyp bool} - val relT = @{typ "bool => bool => bool"} val idx = Thm.maxidx_of thm + 1 - fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool) - fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t) + fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool}) + fun inst (a, t) = + ((Name.clean_index (prep a, idx), @{typ "bool \ bool \ bool"}), Thm.cterm_of ctxt' t) in thm |> Thm.generalize (tfrees, rnames @ frees) idx diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/coinduction.ML Mon Jul 06 14:27:03 2015 +0200 @@ -61,9 +61,9 @@ |> fold Variable.declare_names vars |> fold Variable.declare_thm (raw_thm :: prems); val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; - val (rhoTs, rhots) = Thm.match (thm_concl, concl) - |>> map (apply2 Thm.typ_of) - ||> map (apply2 Thm.term_of); + val (instT, inst) = Thm.match (thm_concl, concl); + val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT; + val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst; val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |> map (subst_atomic_types rhoTs); val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; @@ -160,4 +160,3 @@ end; end; - diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/hologic.ML Mon Jul 06 14:27:03 2015 +0200 @@ -207,14 +207,14 @@ let val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ) handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); - val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); + val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; fun conj_elim ctxt thPQ = let val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ)) handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); - val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); + val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; in (thP, thQ) end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/inductive_set.ML Mon Jul 06 14:27:03 2015 +0200 @@ -205,7 +205,7 @@ val x' = map_type (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x; in - (Thm.cterm_of ctxt x, + (dest_Var x, Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts (HOLogic.Collect_const U $ HOLogic.mk_psplits ps U HOLogic.boolT @@ -367,7 +367,7 @@ val T = HOLogic.mk_ptupleT ps Us; val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x in - (Thm.cterm_of ctxt x, + (dest_Var x, Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts (HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)), list_comb (x', map Bound (l - 1 downto k + 1)))))) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/lin_arith.ML Mon Jul 06 14:27:03 2015 +0200 @@ -60,10 +60,8 @@ fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm thy t = - let - val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT)) - and ct = Thm.global_cterm_of thy t - in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end; + let val ct = Thm.global_cterm_of thy t + in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end; end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/monomorph.ML Mon Jul 06 14:27:03 2015 +0200 @@ -159,7 +159,7 @@ fun instantiate ctxt subst = let - fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T) + fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T) fun cert' subst = Vartab.fold (cons o cert) subst [] in Thm.instantiate (cert' subst, []) end diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/numeral.ML Mon Jul 06 14:27:03 2015 +0200 @@ -49,7 +49,7 @@ val uminus = @{cpat "uminus"}; val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus)); -fun instT T V = Thm.instantiate_cterm ([(V, T)], []); +fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []); in diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Mon Jul 06 14:27:03 2015 +0200 @@ -595,8 +595,8 @@ fun prove_nz ctxt T t = let - val z = Thm.instantiate_cterm ([(zT,T)],[]) zr - val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq + val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr + val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply eq t) z))) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/record.ML Mon Jul 06 14:27:03 2015 +0200 @@ -1755,7 +1755,7 @@ fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate - ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) + ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], []) |> Axclass.unoverload thy; val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq); val ensure_exhaustive_record = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/reification.ML Mon Jul 06 14:27:03 2015 +0200 @@ -169,9 +169,9 @@ val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv); val (fts, its) = (map (snd o snd) fnvs, - map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs); + map (fn ((vn, vi), (tT, t)) => (((vn, vi), tT), Thm.cterm_of ctxt t)) invs); val ctyenv = - map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty)) + map (fn ((vn, vi), (s, ty)) => (((vn, vi), s), Thm.ctyp_of ctxt ty)) (Vartab.dest tyenv); in ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt, @@ -203,7 +203,7 @@ val sbst = Envir.subst_term (tyenv, tmenv); val sbsT = Envir.subst_type tyenv; val subst_ty = - map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv) + map (fn (n, (s, t)) => ((n, s), Thm.ctyp_of ctxt'' t)) (Vartab.dest tyenv) val tml = Vartab.dest tmenv; val (subst_ns, bds) = fold_map (fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds => @@ -230,7 +230,9 @@ let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; - val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym; + val th = + (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq) + RS sym; in (hd (Variable.export ctxt'' ctxt [th]), bds) end) handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); @@ -266,10 +268,7 @@ let val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb; - val subst = - map_filter - (fn (v as Var (_, T)) => SOME (Thm.cterm_of ctxt' v, subst T) - | _ => NONE) vs; + val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs; in Thm.instantiate ([], subst) eq end; val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs; val bds = AList.make (K ([], [])) tys; @@ -285,9 +284,10 @@ | is_list_var _ = false; val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd |> strip_comb |> snd |> filter is_list_var; - val vs = map (fn v as Var (_, T) => + val vs = map (fn Var (v as (_, T)) => (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; - val th' = Drule.instantiate_normalize ([], map (apply2 (Thm.cterm_of ctxt)) vs) th; + val th' = + Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th; val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); in Thm.transitive th'' th' end; diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/sat.ML Mon Jul 06 14:27:03 2015 +0200 @@ -73,8 +73,6 @@ val resolution_thm = @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} -val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT)); - (* ------------------------------------------------------------------------- *) (* lit_ord: an order on integers that considers their absolute values only, *) (* thereby treating integers that represent the same atom (positively *) @@ -173,7 +171,7 @@ val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) in - Thm.instantiate ([], [(cP, cLit)]) resolution_thm + Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm end val _ = diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Mon Jul 06 14:27:03 2015 +0200 @@ -238,7 +238,7 @@ if is_binop ct ct' then Thm.dest_binop ct' else raise CTERM ("dest_binop: bad binop", [ct, ct']) -fun inst_thm inst = Thm.instantiate ([], inst); +fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst); val dest_number = Thm.term_of #> HOLogic.dest_number #> snd; val is_number = can dest_number; @@ -300,7 +300,7 @@ val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) val neg_tm = Thm.dest_fun neg_pat val dest_sub = dest_binop sub_tm - in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub, neg_mul |> concl |> Thm.dest_arg, + in (neg_mul, sub_add, sub_tm, neg_tm, dest_sub, neg_mul |> concl |> Thm.dest_arg, sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg) end | _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm)); @@ -760,7 +760,7 @@ fun polynomial_neg_conv ctxt tm = let val (l,r) = Thm.dest_comb tm in if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else - let val th1 = inst_thm [(cx',r)] neg_mul + let val th1 = inst_thm [(cx', r)] neg_mul val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) in Thm.transitive th2 (polynomial_monomial_mul_conv ctxt (concl th2)) end @@ -770,7 +770,7 @@ (* Subtraction. *) fun polynomial_sub_conv ctxt tm = let val (l,r) = dest_sub tm - val th1 = inst_thm [(cx',l),(cy',r)] sub_add + val th1 = inst_thm [(cx', l), (cy', r)] sub_add val (tm1,tm2) = Thm.dest_comb(concl th1) val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv ctxt tm2) in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv ctxt (concl th2))) diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/simpdata.ML Mon Jul 06 14:27:03 2015 +0200 @@ -56,7 +56,7 @@ (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) *) -fun lift_meta_eq_to_obj_eq i st = +fun lift_meta_eq_to_obj_eq ctxt i st = let fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; @@ -69,7 +69,7 @@ val mk_simp_implies = fold_rev (fn R => fn S => Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps; in - Goal.prove_global (Thm.theory_of_thm st) [] + Goal.prove_global (Proof_Context.theory_of ctxt) [] [mk_simp_implies @{prop "(x::'a) == y"}] (mk_simp_implies @{prop "(x::'a) = y"}) (fn {context = ctxt, prems} => EVERY @@ -85,7 +85,7 @@ fun mk_meta_cong ctxt rl = let val rl' = Seq.hd (TRYALL (fn i => fn st => - resolve_tac ctxt [lift_meta_eq_to_obj_eq i st] i st) rl) + resolve_tac ctxt [lift_meta_eq_to_obj_eq ctxt i st] i st) rl) in mk_meta_eq rl' handle THM _ => if can Logic.dest_equals (Thm.concl_of rl') then rl' diff -r 03a25d3e759e -r 143ac4d9504a src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/HOL/Tools/split_rule.ML Mon Jul 06 14:27:03 2015 +0200 @@ -42,7 +42,7 @@ fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl = let val T' = HOLogic.flatten_tupleT T1 ---> T2; val newt = ap_split T1 T2 (Var (v, T')); - in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end + in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end | split_rule_var' _ _ rl = rl; @@ -65,15 +65,15 @@ val ys = Name.variant_list xs (replicate (length Ts) a); in (xs @ ys, - apply2 (Thm.cterm_of ctxt) - (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T - (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts) + (dest_Var v, + Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T + (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts) end | mk_tuple _ x = x; val newt = ap_split' Us U (Var (v, T')); val (vs', insts) = fold mk_tuple ts (vs, []); in - (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs') + (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs') end | complete_split_rule_var _ _ x = x; diff -r 03a25d3e759e -r 143ac4d9504a src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Jul 06 14:27:03 2015 +0200 @@ -424,7 +424,7 @@ val T = Thm.typ_of_cterm cv in mth - |> Thm.instantiate ([], [(cv, number_of T n)]) + |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)]) |> rewrite_concl |> discharge_prem handle CTERM _ => mult_by_add n thm diff -r 03a25d3e759e -r 143ac4d9504a src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Provers/classical.ML Mon Jul 06 14:27:03 2015 +0200 @@ -282,12 +282,12 @@ fun delete x = delete_tagged_list (joinrules x); fun delete' x = delete_tagged_list (joinrules' x); -fun string_of_thm NONE = Display.string_of_thm_without_context - | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context); +fun bad_thm (SOME context) msg th = + error (msg ^ "\n" ^ Display.string_of_thm (Context.proof_of context) th) + | bad_thm NONE msg th = raise THM (msg, 0, [th]); -fun make_elim context th = - if has_fewer_prems 1 th then - error ("Ill-formed destruction rule\n" ^ string_of_thm context th) +fun make_elim opt_context th = + if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed destruction rule" th else Tactic.make_elim th; fun warn_thm (SOME (Context.Proof ctxt)) msg th = @@ -295,31 +295,31 @@ then warning (msg ^ Display.string_of_thm ctxt th) else () | warn_thm _ _ _ = (); -fun warn_rules context msg rules th = - Item_Net.member rules th andalso (warn_thm context msg th; true); +fun warn_rules opt_context msg rules th = + Item_Net.member rules th andalso (warn_thm opt_context msg th; true); -fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = - warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse - warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse - warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse - warn_rules context "Rule already declared as elimination (elim)\n" hazEs th; +fun warn_claset opt_context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = + warn_rules opt_context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse + warn_rules opt_context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse + warn_rules opt_context "Rule already declared as introduction (intro)\n" hazIs th orelse + warn_rules opt_context "Rule already declared as elimination (elim)\n" hazEs th; (*** Safe rules ***) -fun addSI w context th +fun addSI w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs + if warn_rules opt_context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs else let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) List.partition Thm.no_prems [th']; val nI = Item_Net.length safeIs + 1; val nE = Item_Net.length safeEs; - val _ = warn_claset context th cs; + val _ = warn_claset opt_context th cs; in CS {safeIs = Item_Net.update th safeIs, @@ -335,21 +335,20 @@ xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} end; -fun addSE w context th +fun addSE w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs - else if has_fewer_prems 1 th then - error ("Ill-formed elimination rule\n" ^ string_of_thm context th) + if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs + else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) List.partition (fn rl => Thm.nprems_of rl=1) [th']; val nI = Item_Net.length safeIs; val nE = Item_Net.length safeEs + 1; - val _ = warn_claset context th cs; + val _ = warn_claset opt_context th cs; in CS {safeEs = Item_Net.update th safeEs, @@ -365,22 +364,22 @@ xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} end; -fun addSD w context th = addSE w context (make_elim context th); +fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th); (*** Hazardous (unsafe) rules ***) -fun addI w context th +fun addI w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs + if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" hazIs th then cs else let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; val nI = Item_Net.length hazIs + 1; val nE = Item_Net.length hazEs; - val _ = warn_claset context th cs; + val _ = warn_claset opt_context th cs; in CS {hazIs = Item_Net.update th hazIs, @@ -396,21 +395,20 @@ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} end handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) - error ("Ill-formed introduction rule\n" ^ string_of_thm context th); + bad_thm opt_context "Ill-formed introduction rule" th; -fun addE w context th +fun addE w opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs - else if has_fewer_prems 1 th then - error ("Ill-formed elimination rule\n" ^ string_of_thm context th) + if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" hazEs th then cs + else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); val nI = Item_Net.length hazIs; val nE = Item_Net.length hazEs + 1; - val _ = warn_claset context th cs; + val _ = warn_claset opt_context th cs; in CS {hazEs = Item_Net.update th hazEs, @@ -426,7 +424,7 @@ xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} end; -fun addD w context th = addE w context (make_elim context th); +fun addD w opt_context th = addE w opt_context (make_elim opt_context th); @@ -435,12 +433,12 @@ to insert. ***) -fun delSI context th +fun delSI opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if Item_Net.member safeIs th then let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; in @@ -459,12 +457,12 @@ end else cs; -fun delSE context th +fun delSE opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if Item_Net.member safeEs th then let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th']; in @@ -483,12 +481,12 @@ end else cs; -fun delI context th +fun delI opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if Item_Net.member hazIs th then let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; in CS @@ -506,14 +504,14 @@ end else cs handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) - error ("Ill-formed introduction rule\n" ^ string_of_thm context th); + bad_thm opt_context "Ill-formed introduction rule" th; -fun delE context th +fun delE opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if Item_Net.member hazEs th then let - val ctxt = default_context context th; + val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); in CS @@ -532,17 +530,17 @@ else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) -fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = +fun delrule opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = let val th' = Tactic.make_elim th in if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse Item_Net.member safeEs th' orelse Item_Net.member hazEs th' then - delSI context th - (delSE context th - (delI context th - (delE context th (delSE context th' (delE context th' cs))))) - else (warn_thm context "Undeclared classical rule\n" th; cs) + delSI opt_context th + (delSE opt_context th + (delI opt_context th + (delE opt_context th (delSE opt_context th' (delE opt_context th' cs))))) + else (warn_thm opt_context "Undeclared classical rule\n" th; cs) end; @@ -858,7 +856,8 @@ (* attributes *) fun attrib f = - Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context); + Thm.declaration_attribute (fn th => fn opt_context => + map_cs (f (SOME opt_context) th) opt_context); val safe_elim = attrib o addSE; val safe_intro = attrib o addSI; @@ -868,8 +867,8 @@ val haz_dest = attrib o addD; val rule_del = - Thm.declaration_attribute (fn th => fn context => - context |> map_cs (delrule (SOME context) th) |> + Thm.declaration_attribute (fn th => fn opt_context => + opt_context |> map_cs (delrule (SOME opt_context) th) |> Thm.attribute_declaration Context_Rules.rule_del th); diff -r 03a25d3e759e -r 143ac4d9504a src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Provers/hypsubst.ML Mon Jul 06 14:27:03 2015 +0200 @@ -186,10 +186,10 @@ val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); in compose_tac ctxt (true, Drule.instantiate_normalize (instT, - map (apply2 (Thm.cterm_of ctxt)) - [(Var (ixn, Ts ---> U --> body_type T), u), - (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), - (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', + map (apsnd (Thm.cterm_of ctxt)) + [((ixn, Ts ---> U --> body_type T), u), + ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), + ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', Thm.nprems_of rl) i end | NONE => no_tac); diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Isar/element.ML Mon Jul 06 14:27:03 2015 +0200 @@ -201,7 +201,7 @@ SOME C => let val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); - val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th; + val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th; in (th', true) end | NONE => (th, false)); @@ -340,7 +340,7 @@ fun instantiate_tfrees thy subst th = let val idx = Thm.maxidx_of th + 1; - fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T); + fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T); fun add_inst (a, S) insts = if AList.defined (op =) insts a then insts diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Isar/generic_target.ML Mon Jul 06 14:27:03 2015 +0200 @@ -271,12 +271,13 @@ |>> map Logic.dest_type; val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); - val inst = filter (is_Var o fst) (vars ~~ frees); - val cinstT = instT - |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar); - val cinst = inst - |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT))); - val result' = Thm.instantiate (cinstT, cinst) result; + val inst = + map_filter + (fn (Var (xi, T), t) => + SOME ((xi, Term_Subst.instantiateT instT T), + Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) + | _ => NONE) (vars ~~ frees); + val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result; (*import assumes/defines*) val result'' = diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Mon Jul 06 14:27:03 2015 +0200 @@ -334,7 +334,7 @@ val instT = fold (Term.add_tvarsT o #2) params [] - |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T))); + |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v)))); val closed_rule = rule |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |> Thm.instantiate (instT, []); diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Isar/subgoal.ML Mon Jul 06 14:27:03 2015 +0200 @@ -12,8 +12,9 @@ signature SUBGOAL = sig - type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, - asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list} + type focus = + {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, + concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} val focus_params: Proof.context -> int -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> thm -> focus * thm val focus_prems: Proof.context -> int -> thm -> focus * thm @@ -36,8 +37,9 @@ (* focus *) -type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, - asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}; +type focus = + {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, + concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}; fun gen_focus (do_prems, do_concl) ctxt i raw_st = let @@ -100,7 +102,7 @@ val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); - val th'' = Thm.instantiate ([], inst1) th'; + val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; in ((inst2, th''), ctxt'') end; (* diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Proof/proof_checker.ML Mon Jul 06 14:27:03 2015 +0200 @@ -78,8 +78,8 @@ let val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; val (fmap, thm') = Thm.varifyT_global' [] thm; - val ctye = map (apply2 (Thm.global_ctyp_of thy)) - (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) + val ctye = + (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts); in Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) end; @@ -118,7 +118,7 @@ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t end - | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) = + | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) = let val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/Tools/rule_insts.ML Mon Jul 06 14:27:03 2015 +0200 @@ -149,8 +149,8 @@ in thm |> Drule.instantiate_normalize - (map (apply2 (Thm.ctyp_of ctxt') o apfst TVar) inst_tvars, - map (apply2 (Thm.cterm_of ctxt') o apfst Var) inst_vars) + (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars, + map (apsnd (Thm.cterm_of ctxt')) inst_vars) |> singleton (Variable.export ctxt' ctxt) |> Rule_Cases.save thm end; @@ -240,13 +240,13 @@ val inc = Thm.maxidx_of st + 1; val lift_type = Logic.incr_tvar inc; - fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T); + fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T); fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t); val inst_tvars' = inst_tvars - |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar); + |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))); val inst_vars' = inst_vars - |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t)); + |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))); val thm' = Thm.lift_rule cgoal thm |> Drule.instantiate_normalize (inst_tvars', inst_vars') @@ -262,10 +262,11 @@ fun make_elim_preserve ctxt rl = let val maxidx = Thm.maxidx_of rl; + fun var x = ((x, 0), propT); fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = - Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), - (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl; + Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)), + (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl; in (case Seq.list_of (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/conjunction.ML Mon Jul 06 14:27:03 2015 +0200 @@ -69,8 +69,8 @@ local -val A = read_prop "A" and vA = read_prop "?A"; -val B = read_prop "B" and vB = read_prop "?B"; +val A = read_prop "A" and vA = (("A", 0), propT); +val B = read_prop "B" and vB = (("B", 0), propT); val C = read_prop "C"; val ABC = read_prop "A ==> B ==> C"; val A_B = read_prop "A &&& B"; diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/display.ML --- a/src/Pure/display.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/display.ML Mon Jul 06 14:27:03 2015 +0200 @@ -21,10 +21,8 @@ val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T - val pretty_thm_without_context: thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string - val string_of_thm_without_context: thm -> string val pretty_full_theory: bool -> theory -> Pretty.T list end; @@ -82,11 +80,8 @@ fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; -fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; - val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; -val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context; diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/drule.ML Mon Jul 06 14:27:03 2015 +0200 @@ -20,7 +20,8 @@ val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm - val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm + val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + thm -> thm val zero_var_indexes_list: thm list -> thm list val zero_var_indexes: thm -> thm val implies_intr_hyps: thm -> thm @@ -613,11 +614,9 @@ fun mk_term ct = let - val thy = Thm.theory_of_cterm ct; - val T = Thm.typ_of_cterm ct; - val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T); - val x = Thm.global_cterm_of thy (Var (("x", 0), T)); - in Thm.instantiate ([instT], [(x, ct)]) termI end; + val cT = Thm.ctyp_of_cterm ct; + val T = Thm.typ_of cT; + in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in @@ -767,9 +766,9 @@ val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0); val instT = Vartab.fold (fn (xi, (S, T)) => - cons (apply2 (Thm.global_ctyp_of thy) (TVar (xi, S), Envir.norm_type tye T))) tye []; + cons ((xi, S), Thm.global_ctyp_of thy (Envir.norm_type tye T))) tye []; val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; - in instantiate_normalize (instT, inst) th end + in instantiate_normalize (instT, map (apfst (Thm.term_of #> dest_Var)) inst) th end handle TERM (msg, _) => raise THM (msg, 0, [th]) | TYPE (msg, _, _) => raise THM (msg, 0, [th]); end; @@ -784,27 +783,18 @@ map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); - fun inst_of (v, ct) = - (Thm.global_cterm_of (Thm.theory_of_cterm ct) (Var v), ct) - handle TYPE (msg, _, _) => err msg; - - fun tyinst_of (v, cT) = - (Thm.global_ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT) - handle TYPE (msg, _, _) => err msg; - fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; - (*instantiate types first!*) val thm' = if forall is_none cTs then thm - else Thm.instantiate - (map tyinst_of (zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; + else + Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; val thm'' = if forall is_none cts then thm' - else Thm.instantiate - ([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm'; + else + Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; in thm'' end; diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/goal.ML Mon Jul 06 14:27:03 2015 +0200 @@ -60,9 +60,7 @@ -------- (init) C ==> #C *) -val init = - let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI)) - in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; +fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI; (* A1 ==> ... ==> An ==> C @@ -134,8 +132,7 @@ val fixes = map (Thm.cterm_of ctxt) xs; val tfrees = fold Term.add_tfrees (prop :: As) []; - val instT = - map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees; + val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees; val global_prop = Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))) diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/more_thm.ML Mon Jul 06 14:27:03 2015 +0200 @@ -62,12 +62,12 @@ val forall_elim_vars: int -> thm -> thm val global_certify_inst: theory -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - (ctyp * ctyp) list * (cterm * cterm) list + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val global_certify_instantiate: theory -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm val certify_inst: Proof.context -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - (ctyp * ctyp) list * (cterm * cterm) list + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val certify_instantiate: Proof.context -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm val forall_intr_frees: thm -> thm @@ -357,15 +357,15 @@ (* certify_instantiate *) fun global_certify_inst thy (instT, inst) = - (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT, - map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst); + (map (apsnd (Thm.global_ctyp_of thy)) instT, + map (apsnd (Thm.global_cterm_of thy)) inst); fun global_certify_instantiate thy insts th = Thm.instantiate (global_certify_inst thy insts) th; fun certify_inst ctxt (instT, inst) = - (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT, - map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst); + (map (apsnd (Thm.ctyp_of ctxt)) instT, + map (apsnd (Thm.cterm_of ctxt)) inst); fun certify_instantiate ctxt insts th = Thm.instantiate (certify_inst ctxt insts) th; @@ -446,10 +446,12 @@ fun stripped_sorts thy t = let - val tfrees = rev (map TFree (Term.add_tfrees t [])); - val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees)); - val strip = tfrees ~~ tfrees'; - val recover = map (apply2 (Thm.global_ctyp_of thy o Logic.varifyT_global) o swap) strip; + val tfrees = rev (Term.add_tfrees t []); + val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length tfrees)); + val recover = + map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) + tfrees' tfrees; + val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Mon Jul 06 14:27:03 2015 +0200 @@ -1044,8 +1044,9 @@ then NONE else SOME thm2')) end; -val (cA, (cB, cC)) = - apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); +val vA = (("A", 0), propT); +val vB = (("B", 0), propT); +val vC = (("C", 0), propT); fun transitive1 NONE NONE = NONE | transitive1 (SOME thm1) NONE = SOME thm1 @@ -1177,7 +1178,7 @@ val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); val eq' = Thm.implies_elim - (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) + (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong) (Thm.implies_intr prem eq); in if not r then eq' @@ -1188,9 +1189,9 @@ in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq) end end diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/thm.ML Mon Jul 06 14:27:03 2015 +0200 @@ -47,8 +47,10 @@ val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm - val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list - val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list + val match: cterm * cterm -> + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + val first_order_match: cterm * cterm -> + ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list (*theorems*) val rep_thm: thm -> {thy: theory, @@ -70,6 +72,7 @@ val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_of_thm: thm -> theory + val theory_name_of_thm: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val hyps_of: thm -> term list @@ -119,8 +122,10 @@ val equal_elim: thm -> thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq val generalize: string list * string list -> int -> thm -> thm - val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm - val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm + val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + thm -> thm + val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> + cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val strip_shyps: thm -> thm @@ -311,12 +316,10 @@ val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = - (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts}, - Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); - fun mk_ctinst ((x, i), (T, t)) = - let val T = Envir.subst_type Tinsts T in - (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts}, - Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) + (((a, i), S), Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); + fun mk_ctinst ((x, i), (U, t)) = + let val T = Envir.subst_type Tinsts U in + (((x, i), T), Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; @@ -391,6 +394,7 @@ (* basic components *) val theory_of_thm = #thy o rep_thm; +val theory_name_of_thm = Context.theory_name o #thy o rep_thm; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val hyps_of = #hyps o rep_thm; @@ -1089,37 +1093,28 @@ fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; -fun add_inst (ct, cu) (thy, sorts) = +fun add_inst (v as (_, T), cu) (thy, sorts) = let - val Cterm {t = t, T = T, ...} = ct; - val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; - val thy' = Theory.merge (thy, merge_thys0 ct cu); + val Cterm {t = u, T = U, thy = thy2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; + val thy' = Theory.merge (thy, thy2); val sorts' = Sorts.union sorts_u sorts; in - (case t of Var v => - if T = U then ((v, (u, maxidx_u)), (thy', sorts')) - else raise TYPE (Pretty.string_of (Pretty.block + if T = U then ((v, (u, maxidx_u)), (thy', sorts')) + else + raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", - Pretty.fbrk, pretty_typing thy' t T, - Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u]) - | _ => raise TYPE (Pretty.string_of (Pretty.block - [Pretty.str "instantiate: not a variable", - Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t])) + Pretty.fbrk, pretty_typing thy' (Var v) T, + Pretty.fbrk, pretty_typing thy' u U]), [T, U], [Var v, u]) end; -fun add_instT (cT, cU) (thy, sorts) = +fun add_instT (v as (_, S), cU) (thy, sorts) = let - val Ctyp {T, thy = thy1, ...} = cT - and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; - val thy' = Theory.merge (thy, Theory.merge (thy1, thy2)); + val Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; + val thy' = Theory.merge (thy, thy2); val sorts' = Sorts.union sorts_U sorts; in - (case T of TVar (v as (_, S)) => - if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) - else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) - | _ => raise TYPE (Pretty.string_of (Pretty.block - [Pretty.str "instantiate: not a type variable", - Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], [])) + if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) + else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) end; in diff -r 03a25d3e759e -r 143ac4d9504a src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Pure/variable.ML Mon Jul 06 14:27:03 2015 +0200 @@ -71,10 +71,11 @@ (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context val importT_terms: term list -> Proof.context -> term list * Proof.context val import_terms: bool -> term list -> Proof.context -> term list * Proof.context - val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context + val importT: thm list -> Proof.context -> + (((indexname * sort) * ctyp) list * thm list) * Proof.context val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context val import: bool -> thm list -> Proof.context -> - (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context + ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context diff -r 03a25d3e759e -r 143ac4d9504a src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Mon Jul 06 14:27:03 2015 +0200 @@ -174,7 +174,7 @@ val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) - val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts; + val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; (* type instantiated versions *) val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; @@ -198,7 +198,7 @@ (* create certms of instantiations *) val cinsts_tyinst = - map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst; + map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; (* The instantiated rule *) val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); @@ -217,7 +217,7 @@ val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst - |> Thm.instantiate ([], cterm_renamings) + |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = Conv.fconv_rule Drule.beta_eta_conversion @@ -227,7 +227,7 @@ val tgt_th_inst = tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst) - |> Thm.instantiate ([], cterm_renamings); + |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in diff -r 03a25d3e759e -r 143ac4d9504a src/Tools/coherent.ML --- a/src/Tools/coherent.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Tools/coherent.ML Mon Jul 06 14:27:03 2015 +0200 @@ -179,10 +179,10 @@ val th' = Drule.implies_elim_list (Thm.instantiate - (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye), + (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye), map (fn (ixn, (T, t)) => - apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @ - map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th) + ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @ + map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th) (map (nth asms) is); val (_, cases) = dest_elim (Thm.prop_of th'); in diff -r 03a25d3e759e -r 143ac4d9504a src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Tools/induct.ML Mon Jul 06 14:27:03 2015 +0200 @@ -573,8 +573,8 @@ val pairs = Vartab.dest (Envir.term_env env); val types = Vartab.dest (Envir.type_env env); val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; - val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts); - in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end; + val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts; + in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end; in diff -r 03a25d3e759e -r 143ac4d9504a src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Tools/misc_legacy.ML Mon Jul 06 14:27:03 2015 +0200 @@ -173,9 +173,9 @@ then ((v, T), true, free_of "METAHYP2_" (v, T)) else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) (*Instantiate subgoal vars by Free applied to params*) - fun mk_ctpair (v, in_concl, u) = - if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u) - else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams)) + fun mk_inst (v, in_concl, u) = + if in_concl then (v, Thm.cterm_of ctxt u) + else (v, Thm.cterm_of ctxt (list_comb (u, fparams))) (*Restore Vars with higher type and index*) fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T)) @@ -191,7 +191,7 @@ fold Term.add_vars (Logic.strip_imp_prems prop) [] and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars - val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st + val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) @@ -269,7 +269,7 @@ fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) - in (Thm.instantiate ([],insts) fth, thaw) end + in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end end; (*Basic version of the function above. No option to rename Vars apart in thaw. @@ -291,7 +291,7 @@ fun thaw th' = th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map #1 insts) - in (Thm.instantiate ([],insts) fth, thaw) end + in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end end; end; diff -r 03a25d3e759e -r 143ac4d9504a src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/Tools/nbe.ML Mon Jul 06 14:27:03 2015 +0200 @@ -101,11 +101,10 @@ val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []); fun instantiate thm = let - val cert_tvars = map (Thm.ctyp_of ctxt o TVar) (Term.add_tvars - ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []); - val instantiation = - map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab; - in Thm.instantiate (instantiation, []) thm end; + val tvars = + Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) []; + val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab; + in Thm.instantiate (instT, []) thm end; fun of_class (TFree (v, _), class) = the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class) | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T); diff -r 03a25d3e759e -r 143ac4d9504a src/ZF/Tools/cartprod.ML --- a/src/ZF/Tools/cartprod.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/ZF/Tools/cartprod.ML Mon Jul 06 14:27:03 2015 +0200 @@ -109,7 +109,7 @@ in remove_split ctxt (Drule.instantiate_normalize ([], - [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl) + [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl) end | split_rule_var _ (t,T,rl) = rl; diff -r 03a25d3e759e -r 143ac4d9504a src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/ZF/Tools/datatype_package.ML Mon Jul 06 14:27:03 2015 +0200 @@ -17,7 +17,7 @@ recursor_eqns : thm list, (*equations for the recursor*) free_iffs : thm list, (*freeness rewrite rules*) free_SEs : thm list, (*freeness destruct rules*) - mk_free : string -> thm}; (*function to make freeness theorems*) + mk_free : Proof.context -> string -> thm}; (*function to make freeness theorems*) signature DATATYPE_ARG = sig @@ -343,10 +343,9 @@ (*Typical theorems have the form ~con1=con2, con1=con2==>False, con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) - fun mk_free s = + fun mk_free ctxt s = let - val thy = Thm.theory_of_thm elim; - val ctxt = Proof_Context.init_global thy; + val thy = Proof_Context.theory_of ctxt; in Goal.prove_global thy [] [] (Syntax.read_prop ctxt s) (fn {context = ctxt', ...} => EVERY diff -r 03a25d3e759e -r 143ac4d9504a src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Jul 03 10:17:29 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Mon Jul 06 14:27:03 2015 +0200 @@ -495,7 +495,7 @@ The name "x.1" comes from the "RS spec" !*) val inst = case elem_frees of [_] => I - | _ => Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy (Var(("x",1), Ind_Syntax.iT)), + | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)), Thm.global_cterm_of thy elem_tuple)]); (*strip quantifier and the implication*)