# HG changeset patch # User wenzelm # Date 1327522440 -3600 # Node ID 912b42e64fdefd403c194369e9f83ea9cbb1b9f0 # Parent b03897da3c90c2b1a23ca4b8e88a2137b6679137 tuned ML infixes; diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 21:14:00 2012 +0100 @@ -356,7 +356,7 @@ text %mlref {* \begin{mldecls} @{index_ML_type term} \\ - @{index_ML "op aconv": "term * term -> bool"} \\ + @{index_ML_op "aconv": "term * term -> bool"} \\ @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\ @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\ @@ -380,7 +380,7 @@ \item Type @{ML_type term} represents de-Bruijn terms, with comments in abstractions, and explicitly named free variables and constants; this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML - Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}. + Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}. \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text "\"}-equivalence of two terms. This is the basic equality relation @@ -700,7 +700,7 @@ \item @{ML Thm.capply}, @{ML Thm.cabs}, @{ML Thm.all}, @{ML Drule.mk_implies} etc.\ compose certified terms (or propositions) incrementally. This is equivalent to @{ML Thm.cterm_of} after - unchecked @{ML "op $"}, @{ML lambda}, @{ML Logic.all}, @{ML + unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML Logic.mk_implies} etc., but there can be a big difference in performance when large existing entities are composed by a few extra constructions on top. There are separate operations to decompose @@ -1084,14 +1084,14 @@ text %mlref {* \begin{mldecls} - @{index_ML "op RSN": "thm * (int * thm) -> thm"} \\ - @{index_ML "op RS": "thm * thm -> thm"} \\ + @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\ + @{index_ML_op "RS": "thm * thm -> thm"} \\ - @{index_ML "op RLN": "thm list * (int * thm list) -> thm list"} \\ - @{index_ML "op RL": "thm list * thm list -> thm list"} \\ + @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\ + @{index_ML_op "RL": "thm list * thm list -> thm list"} \\ - @{index_ML "op MRS": "thm list * thm -> thm"} \\ - @{index_ML "op OF": "thm * thm list -> thm"} \\ + @{index_ML_op "MRS": "thm list * thm -> thm"} \\ + @{index_ML_op "OF": "thm * thm list -> thm"} \\ \end{mldecls} \begin{description} diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 25 21:14:00 2012 +0100 @@ -849,10 +849,10 @@ text %mlref {* \begin{mldecls} - @{index_ML "op |> ": "'a * ('a -> 'b) -> 'b"} \\ - @{index_ML "op |-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\ - @{index_ML "op #> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\ - @{index_ML "op #-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\ + @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\ + @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\ + @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\ + @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\ \end{mldecls} %FIXME description!? @@ -1465,7 +1465,7 @@ @{index_ML_type "'a Unsynchronized.ref"} \\ @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\ - @{index_ML "op :=": "'a Unsynchronized.ref * 'a -> unit"} \\ + @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\ \end{mldecls} *} @@ -1477,7 +1477,7 @@ The unwieldy name of @{ML Unsynchronized.ref} for the constructor for references in Isabelle/ML emphasizes the inconveniences caused by - mutability. Existing operations @{ML "!"} and @{ML "op :="} are + mutability. Existing operations @{ML "!"} and @{ML_op ":="} are unchanged, but should be used with special precautions, say in a strictly local situation that is guaranteed to be restricted to sequential evaluation --- now and in the future. diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:14:00 2012 +0100 @@ -414,22 +414,23 @@ text {* Sequential composition and alternative choices are the most basic ways to combine tactics, similarly to ``@{verbatim ","}'' and ``@{verbatim "|"}'' in Isar method notation. This corresponds to - @{text "THEN"} and @{text "ORELSE"} in ML, but there are further - possibilities for fine-tuning alternation of tactics such as @{text + @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further + possibilities for fine-tuning alternation of tactics such as @{ML_op "APPEND"}. Further details become visible in ML due to explicit - subgoal addressing. *} + subgoal addressing. +*} text %mlref {* \begin{mldecls} - @{index_ML "op THEN": "tactic * tactic -> tactic"} \\ - @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\ - @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\ + @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\ + @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\ + @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\ @{index_ML "EVERY": "tactic list -> tactic"} \\ @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] - @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ - @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ - @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ @{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\ @@ -438,47 +439,50 @@ \begin{description} - \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of - @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a proof state, it - returns all states reachable in two steps by applying @{text "tac\<^sub>1"} - followed by @{text "tac\<^sub>2"}. First, it applies @{text "tac\<^sub>1"} to the - proof state, getting a sequence of possible next states; then, it - applies @{text "tac\<^sub>2"} to each of these and concatenates the results - to produce again one flat sequence of states. + \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential + composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a + proof state, it returns all states reachable in two steps by + applying @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it + applies @{text "tac\<^sub>1"} to the proof state, getting a sequence of + possible next states; then, it applies @{text "tac\<^sub>2"} to each of + these and concatenates the results to produce again one flat + sequence of states. - \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text - "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it tries @{text - "tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails - then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if - @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the - result. + \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice + between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it + tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text + "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}. This is a deterministic + choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded + from the result. - \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results - of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there - is \emph{no commitment} to either tactic, so @{text "APPEND"} helps - to avoid incompleteness during search, at the cost of potential - inefficiencies. + \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the + possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike + @{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so + @{ML_op "APPEND"} helps to avoid incompleteness during search, at + the cost of potential inefficiencies. - \item @{text "EVERY [tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN - \ THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML - all_tac}: it always succeeds. + \item @{ML EVERY}~@{text "[tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text + "tac\<^sub>1"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac\<^sub>n"}. + Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always + succeeds. - \item @{text "FIRST [tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 - ORELSE \ ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as - @{ML no_tac}: it always fails. + \item @{ML FIRST}~@{text "[tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text + "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\"}~@{ML_op "ORELSE"}~@{text + "tac\<^sub>n"}. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it + always fails. - \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are - lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text - "APPEND"}, for tactics with explicit subgoal addressing. This means - @{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN - tac\<^sub>2 i)"} etc. + \item @{ML_op "THEN'"}, @{ML_op "ORELSE'"}, and @{ML_op "APPEND'"} + are lifted versions of @{ML_op "THEN"}, @{ML_op "ORELSE"}, and + @{ML_op "APPEND"}, for tactics with explicit subgoal addressing. + This means @{text "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the + same as @{text "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"} etc. - \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of - @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit - subgoal addressing. + \item @{ML "EVERY'"} and @{ML "FIRST'"} are lifted versions of @{ML + "EVERY'"} and @{ML "FIRST'"}, for tactics with explicit subgoal + addressing. - \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions - of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1. + \item @{ML "EVERY1"} and @{ML "FIRST1"} are convenience versions of + @{ML "EVERY'"} and @{ML "FIRST'"}, applied to subgoal 1. \end{description} *} @@ -543,13 +547,13 @@ \begin{itemize} - \item @{ML all_tac} is the identity element of the tactical - @{ML "op THEN"}. + \item @{ML all_tac} is the identity element of the tactical @{ML_op + "THEN"}. - \item @{ML no_tac} is the identity element of @{ML "op ORELSE"} and - @{ML "op APPEND"}. Also, it is a zero element for @{ML "op THEN"}, - which means that @{text "tac THEN"}~@{ML no_tac} is equivalent to - @{ML no_tac}. + \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and + @{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"}, + which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is + equivalent to @{ML no_tac}. \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) functions over more basic combinators (ignoring some internal @@ -564,8 +568,8 @@ *} text {* If @{text "tac"} can return multiple outcomes then so can @{ML - REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML "op ORELSE"} and not - @{ML "op APPEND"}, it applies @{text "tac"} as many times as + REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not + @{ML_op "APPEND"}, it applies @{text "tac"} as many times as possible in each outcome. \begin{warn} diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/document/Logic.tex --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 21:14:00 2012 +0100 @@ -394,7 +394,7 @@ \begin{isamarkuptext}% \begin{mldecls} \indexdef{}{ML type}{term}\verb|type term| \\ - \indexdef{}{ML}{aconv}\verb|op aconv: term * term -> bool| \\ + \indexdef{}{ML infix}{aconv}\verb|infix aconv: term * term -> bool| \\ \indexdef{}{ML}{Term.map\_types}\verb|Term.map_types: (typ -> typ) -> term -> term| \\ \indexdef{}{ML}{Term.fold\_types}\verb|Term.fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\ \indexdef{}{ML}{Term.map\_aterms}\verb|Term.map_aterms: (term -> term) -> term -> term| \\ @@ -417,7 +417,7 @@ \item Type \verb|term| represents de-Bruijn terms, with comments in abstractions, and explicitly named free variables and constants; - this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|op $|. + this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|$|. \item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-equivalence of two terms. This is the basic equality relation on type \verb|term|; raw datatype equality should only be used @@ -769,7 +769,7 @@ \item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions) incrementally. This is equivalent to \verb|Thm.cterm_of| after - unchecked \verb|op $|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in + unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in performance when large existing entities are composed by a few extra constructions on top. There are separate operations to decompose certified terms and theorems to produce certified terms again. @@ -1226,14 +1226,14 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{RSN}\verb|op RSN: thm * (int * thm) -> thm| \\ - \indexdef{}{ML}{RS}\verb|op RS: thm * thm -> thm| \\ + \indexdef{}{ML infix}{RSN}\verb|infix RSN: thm * (int * thm) -> thm| \\ + \indexdef{}{ML infix}{RS}\verb|infix RS: thm * thm -> thm| \\ - \indexdef{}{ML}{RLN}\verb|op RLN: thm list * (int * thm list) -> thm list| \\ - \indexdef{}{ML}{RL}\verb|op RL: thm list * thm list -> thm list| \\ + \indexdef{}{ML infix}{RLN}\verb|infix RLN: thm list * (int * thm list) -> thm list| \\ + \indexdef{}{ML infix}{RL}\verb|infix RL: thm list * thm list -> thm list| \\ - \indexdef{}{ML}{MRS}\verb|op MRS: thm list * thm -> thm| \\ - \indexdef{}{ML}{OF}\verb|op OF: thm * thm list -> thm| \\ + \indexdef{}{ML infix}{MRS}\verb|infix MRS: thm list * thm -> thm| \\ + \indexdef{}{ML infix}{OF}\verb|infix OF: thm * thm list -> thm| \\ \end{mldecls} \begin{description} diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 25 21:14:00 2012 +0100 @@ -1076,10 +1076,10 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{$\mid$$>$}\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\ - \indexdef{}{ML}{$\mid$-$>$}\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ - \indexdef{}{ML}{\#$>$}\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\ - \indexdef{}{ML}{\#-$>$}\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\ + \indexdef{}{ML infix}{$\mid$$>$}\verb|infix |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\ + \indexdef{}{ML infix}{$\mid$-$>$}\verb|infix |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ + \indexdef{}{ML infix}{\#$>$}\verb|infix #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\ + \indexdef{}{ML infix}{\#-$>$}\verb|infix #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\ \end{mldecls} %FIXME description!?% @@ -1968,7 +1968,7 @@ \indexdef{}{ML type}{Unsynchronized.ref}\verb|type 'a Unsynchronized.ref| \\ \indexdef{}{ML}{Unsynchronized.ref}\verb|Unsynchronized.ref: 'a -> 'a Unsynchronized.ref| \\ \indexdef{}{ML}{!}\verb|! : 'a Unsynchronized.ref -> 'a| \\ - \indexdef{}{ML}{:=}\verb|op := : 'a Unsynchronized.ref * 'a -> unit| \\ + \indexdef{}{ML infix}{:=}\verb|infix := : 'a Unsynchronized.ref * 'a -> unit| \\ \end{mldecls}% \end{isamarkuptext}% \isamarkuptrue% @@ -1989,7 +1989,7 @@ The unwieldy name of \verb|Unsynchronized.ref| for the constructor for references in Isabelle/ML emphasizes the inconveniences caused by - mutability. Existing operations \verb|!| and \verb|op :=| are + mutability. Existing operations \verb|!| and \verb|:=| are unchanged, but should be used with special precautions, say in a strictly local situation that is guaranteed to be restricted to sequential evaluation --- now and in the future. diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:14:00 2012 +0100 @@ -495,8 +495,8 @@ Sequential composition and alternative choices are the most basic ways to combine tactics, similarly to ``\verb|,|'' and ``\verb||\verb,|,\verb||'' in Isar method notation. This corresponds to - \isa{THEN} and \isa{ORELSE} in ML, but there are further - possibilities for fine-tuning alternation of tactics such as \isa{APPEND}. Further details become visible in ML due to explicit + \verb|THEN| and \verb|ORELSE| in ML, but there are further + possibilities for fine-tuning alternation of tactics such as \verb|APPEND|. Further details become visible in ML due to explicit subgoal addressing.% \end{isamarkuptext}% \isamarkuptrue% @@ -509,15 +509,15 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{THEN}\verb|op THEN: tactic * tactic -> tactic| \\ - \indexdef{}{ML}{ORELSE}\verb|op ORELSE: tactic * tactic -> tactic| \\ - \indexdef{}{ML}{APPEND}\verb|op APPEND: tactic * tactic -> tactic| \\ + \indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\ + \indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\ + \indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\ \indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\ \indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex] - \indexdef{}{ML}{THEN'}\verb|op THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ - \indexdef{}{ML}{ORELSE'}\verb|op ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ - \indexdef{}{ML}{APPEND'}\verb|op APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML infix}{APPEND'}\verb|infix APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ \indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\ \indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\ \indexdef{}{ML}{EVERY1}\verb|EVERY1: (int -> tactic) list -> tactic| \\ @@ -526,40 +526,45 @@ \begin{description} - \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential composition of - \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a proof state, it - returns all states reachable in two steps by applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} - followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the - proof state, getting a sequence of possible next states; then, it - applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and concatenates the results - to produce again one flat sequence of states. + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential + composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a + proof state, it returns all states reachable in two steps by + applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it + applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the proof state, getting a sequence of + possible next states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of + these and concatenates the results to produce again one flat + sequence of states. - \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails - then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic choice: if - \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded from the - result. + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice + between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it + tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic + choice: if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded + from the result. - \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ APPEND\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the possible results - of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike \isa{ORELSE} there - is \emph{no commitment} to either tactic, so \isa{APPEND} helps - to avoid incompleteness during search, at the cost of potential - inefficiencies. + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|APPEND|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the + possible results of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike + \verb|ORELSE| there is \emph{no commitment} to either tactic, so + \verb|APPEND| helps to avoid incompleteness during search, at + the cost of potential inefficiencies. - \item \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as \verb|all_tac|: it always succeeds. - - \item \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as - \verb|no_tac|: it always fails. + \item \verb|EVERY|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. + Note that \verb|EVERY []| is the same as \verb|all_tac|: it always + succeeds. - \item \isa{THEN{\isaliteral{27}{\isacharprime}}}, \isa{ORELSE{\isaliteral{27}{\isacharprime}}}, and \isa{APPEND{\isaliteral{27}{\isacharprime}}} are - lifted versions of \isa{THEN}, \isa{ORELSE}, and \isa{APPEND}, for tactics with explicit subgoal addressing. This means - \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN{\isaliteral{27}{\isacharprime}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc. + \item \verb|FIRST|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \verb|FIRST []| is the same as \verb|no_tac|: it + always fails. - \item \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}} are lifted versions of - \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, for tactics with explicit - subgoal addressing. + \item \verb|THEN'|, \verb|ORELSE'|, and \verb|APPEND'| + are lifted versions of \verb|THEN|, \verb|ORELSE|, and + \verb|APPEND|, for tactics with explicit subgoal addressing. + This means \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the + same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc. - \item \isa{EVERY{\isadigit{1}}} and \isa{FIRST{\isadigit{1}}} are convenience versions - of \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, applied to subgoal 1. + \item \verb|EVERY'| and \verb|FIRST'| are lifted versions of \verb|EVERY'| and \verb|FIRST'|, for tactics with explicit subgoal + addressing. + + \item \verb|EVERY1| and \verb|FIRST1| are convenience versions of + \verb|EVERY'| and \verb|FIRST'|, applied to subgoal 1. \end{description}% \end{isamarkuptext}% @@ -654,13 +659,12 @@ \begin{itemize} - \item \verb|all_tac| is the identity element of the tactical - \verb|op THEN|. + \item \verb|all_tac| is the identity element of the tactical \verb|THEN|. - \item \verb|no_tac| is the identity element of \verb|op ORELSE| and - \verb|op APPEND|. Also, it is a zero element for \verb|op THEN|, - which means that \isa{tac\ THEN}~\verb|no_tac| is equivalent to - \verb|no_tac|. + \item \verb|no_tac| is the identity element of \verb|ORELSE| and + \verb|APPEND|. Also, it is a zero element for \verb|THEN|, + which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is + equivalent to \verb|no_tac|. \item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive) functions over more basic combinators (ignoring some internal @@ -695,8 +699,8 @@ \endisadelimML % \begin{isamarkuptext}% -If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|op ORELSE| and not - \verb|op APPEND|, it applies \isa{tac} as many times as +If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|ORELSE| and not + \verb|APPEND|, it applies \isa{tac} as many times as possible in each outcome. \begin{warn} diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed Jan 25 21:14:00 2012 +0100 @@ -160,8 +160,8 @@ compose rules by resolution. @{attribute THEN} resolves with the first premise of @{text a} (an alternative position may be also specified); the @{attribute COMP} version skips the automatic - lifting process that is normally intended (cf.\ @{ML "op RS"} and - @{ML "op COMP"} in \cite{isabelle-implementation}). + lifting process that is normally intended (cf.\ @{ML_op "RS"} and + @{ML_op "COMP"} in \cite{isabelle-implementation}). \item @{attribute unfolded}~@{text "a\<^sub>1 \ a\<^sub>n"} and @{attribute folded}~@{text "a\<^sub>1 \ a\<^sub>n"} expand and fold back again the given diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarRef/Thy/Proof.thy Wed Jan 25 21:14:00 2012 +0100 @@ -790,7 +790,7 @@ \item @{attribute OF}~@{text "a\<^sub>1 \ a\<^sub>n"} applies some theorem to all of the given rules @{text "a\<^sub>1, \, a\<^sub>n"} - (in parallel). This corresponds to the @{ML "op MRS"} operation in + (in parallel). This corresponds to the @{ML_op "MRS"} operation in ML, but note the reversed order. Positions may be effectively skipped by including ``@{text _}'' (underscore) as argument. diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Jan 25 21:14:00 2012 +0100 @@ -277,8 +277,8 @@ compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the first premise of \isa{a} (an alternative position may be also specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic - lifting process that is normally intended (cf.\ \verb|op RS| and - \verb|op COMP| in \cite{isabelle-implementation}). + lifting process that is normally intended (cf.\ \verb|RS| and + \verb|COMP| in \cite{isabelle-implementation}). \item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand and fold back again the given definitions throughout a rule. diff -r b03897da3c90 -r 912b42e64fde doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Wed Jan 25 21:10:54 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Wed Jan 25 21:14:00 2012 +0100 @@ -1113,7 +1113,7 @@ \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some theorem to all of the given rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} - (in parallel). This corresponds to the \verb|op MRS| operation in + (in parallel). This corresponds to the \verb|MRS| operation in ML, but note the reversed order. Positions may be effectively skipped by including ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' (underscore) as argument.