--- a/src/Doc/ProgProve/Logic.thy Sat Mar 16 21:26:44 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Sat Mar 16 21:44:04 2013 +0100
@@ -5,10 +5,7 @@
(*>*)
text{*
\vspace{-5ex}
-\section{Logic and proof beyond equality}
-\label{sec:Logic}
-
-\subsection{Formulas}
+\section{Formulas}
The core syntax of formulas (\textit{form} below)
provides the standard logical constructs, in decreasing order of precedence:
@@ -71,7 +68,7 @@
but the first one works better when using the theorem in further proofs.
\end{warn}
-\subsection{Sets}
+\section{Sets}
\label{sec:Sets}
Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
@@ -108,7 +105,7 @@
Sets also allow bounded quantifications @{prop"ALL x : A. P"} and
@{prop"EX x : A. P"}.
-\subsection{Proof automation}
+\section{Proof automation}
So far we have only seen @{text simp} and @{text auto}: Both perform
rewriting, both can also prove linear arithmetic facts (no multiplication),
@@ -181,7 +178,7 @@
Because of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods.
-\subsubsection{Sledgehammer}
+\subsection{Sledgehammer}
Command \isacom{sledgehammer} calls a number of external automatic
theorem provers (ATPs) that run for up to 30 seconds searching for a
@@ -221,7 +218,7 @@
incomparable. Therefore it is recommended to apply @{text simp} or @{text
auto} before invoking \isacom{sledgehammer} on what is left.
-\subsubsection{Arithmetic}
+\subsection{Arithmetic}
By arithmetic formulas we mean formulas involving variables, numbers, @{text
"+"}, @{text"-"}, @{text "="}, @{text "<"}, @{text "\<le>"} and the usual logical
@@ -247,7 +244,7 @@
but we will not enlarge on that here.
-\subsubsection{Trying them all}
+\subsection{Trying them all}
If you want to try all of the above automatic proof methods you simply type
\begin{isabelle}
@@ -260,7 +257,7 @@
There is also a lightweight variant \isacom{try0} that does not call
sledgehammer.
-\subsection{Single step proofs}
+\section{Single step proofs}
Although automation is nice, it often fails, at least initially, and you need
to find out why. When @{text fastforce} or @{text blast} simply fail, you have
@@ -273,7 +270,7 @@
\]
to the proof state. We will now examine the details of this process.
-\subsubsection{Instantiating unknowns}
+\subsection{Instantiating unknowns}
We had briefly mentioned earlier that after proving some theorem,
Isabelle replaces all free variables @{text x} by so called \concept{unknowns}
@@ -301,7 +298,7 @@
@{text "conjI[where ?P = \"a=b\" and ?Q = \"False\"]"}.
-\subsubsection{Rule application}
+\subsection{Rule application}
\concept{Rule application} means applying a rule backwards to a proof state.
For example, applying rule @{thm[source]conjI} to a proof state
@@ -327,7 +324,7 @@
\end{quote}
This is also called \concept{backchaining} with rule @{text xyz}.
-\subsubsection{Introduction rules}
+\subsection{Introduction rules}
Conjunction introduction (@{thm[source] conjI}) is one example of a whole
class of rules known as \concept{introduction rules}. They explain under which
@@ -377,7 +374,7 @@
text{*
Of course this is just an example and could be proved by @{text arith}, too.
-\subsubsection{Forward proof}
+\subsection{Forward proof}
\label{sec:forward-proof}
Forward proof means deriving new theorems from old theorems. We have already
@@ -426,7 +423,7 @@
text{* In this particular example we could have backchained with
@{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.
-\subsubsection{Finding theorems}
+\subsection{Finding theorems}
Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
theory. Search criteria include pattern matching on terms and on names.
--- a/src/Doc/ProgProve/document/prelude.tex Sat Mar 16 21:26:44 2013 +0100
+++ b/src/Doc/ProgProve/document/prelude.tex Sat Mar 16 21:44:04 2013 +0100
@@ -9,9 +9,6 @@
\usepackage{ccfonts}
\usepackage[euler-digits]{eulervm}
-\let\bfdefaultold=\bfdefault
-\def\bfdefault{sbc} % make sans serif the default bold font
-
\usepackage{isabelle,isabellesym}
\usepackage{mathpartir}
\usepackage{amssymb}
@@ -63,7 +60,7 @@
% isabelle keyword, adapted from isabelle.sty
\renewcommand{\isakeyword}[1]
{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textbf{#1}}}
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\def\bfdefault{sbc}\textbf{#1}}}
% add \noindent to text blocks automatically
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
--- a/src/Doc/ProgProve/document/root.tex Sat Mar 16 21:26:44 2013 +0100
+++ b/src/Doc/ProgProve/document/root.tex Sat Mar 16 21:44:04 2013 +0100
@@ -34,7 +34,7 @@
%\label{sec:CaseStudyExp}
%\input{../generated/Expressions}
-\chapter{Logic}
+\chapter{Logic and proof beyond equality}
\label{ch:Logic}
\input{Logic}
--- a/src/HOL/IMP/Live_True.thy Sat Mar 16 21:26:44 2013 +0100
+++ b/src/HOL/IMP/Live_True.thy Sat Mar 16 21:44:04 2013 +0100
@@ -8,7 +8,7 @@
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
-"L (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
+"L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"
--- a/src/HOL/Library/RBT_Mapping.thy Sat Mar 16 21:26:44 2013 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy Sat Mar 16 21:44:04 2013 +0100
@@ -39,7 +39,7 @@
lemma map_entry_Mapping [code]:
"Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
-by (transfer fixing: t, case_tac "lookup t k") auto
+ apply (transfer fixing: t) by (case_tac "lookup t k") auto
lemma keys_Mapping [code]:
"Mapping.keys (Mapping t) = set (keys t)"
--- a/src/HOL/Tools/transfer.ML Sat Mar 16 21:26:44 2013 +0100
+++ b/src/HOL/Tools/transfer.ML Sat Mar 16 21:44:04 2013 +0100
@@ -29,22 +29,27 @@
{ transfer_raw : thm Item_Net.T,
known_frees : (string * typ) list,
compound_rhs : unit Net.net,
- relator_eq : thm Item_Net.T }
+ relator_eq : thm Item_Net.T,
+ relator_eq_raw : thm Item_Net.T }
val empty =
{ transfer_raw = Thm.full_rules,
known_frees = [],
compound_rhs = Net.empty,
- relator_eq = Thm.full_rules }
+ relator_eq = Thm.full_rules,
+ relator_eq_raw = Thm.full_rules }
val extend = I
fun merge
( { transfer_raw = t1, known_frees = k1,
- compound_rhs = c1, relator_eq = r1},
+ compound_rhs = c1, relator_eq = r1,
+ relator_eq_raw = rw1 },
{ transfer_raw = t2, known_frees = k2,
- compound_rhs = c2, relator_eq = r2}) =
+ compound_rhs = c2, relator_eq = r2,
+ relator_eq_raw = rw2 } ) =
{ transfer_raw = Item_Net.merge (t1, t2),
known_frees = Library.merge (op =) (k1, k2),
compound_rhs = Net.merge (K true) (c1, c2),
- relator_eq = Item_Net.merge (r1, r2) }
+ relator_eq = Item_Net.merge (r1, r2),
+ relator_eq_raw = Item_Net.merge (rw1, rw2) }
)
fun get_relator_eq ctxt = ctxt
@@ -55,6 +60,9 @@
|> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
|> map (Thm.symmetric o safe_mk_meta_eq)
+fun get_relator_eq_raw ctxt = ctxt
+ |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
+
fun get_transfer_raw ctxt = ctxt
|> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
@@ -64,17 +72,19 @@
fun get_compound_rhs ctxt = ctxt
|> (#compound_rhs o Data.get o Context.Proof)
-fun map_data f1 f2 f3 f4
- { transfer_raw, known_frees, compound_rhs, relator_eq } =
+fun map_data f1 f2 f3 f4 f5
+ { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw } =
{ transfer_raw = f1 transfer_raw,
known_frees = f2 known_frees,
compound_rhs = f3 compound_rhs,
- relator_eq = f4 relator_eq }
+ relator_eq = f4 relator_eq,
+ relator_eq_raw = f5 relator_eq_raw }
-fun map_transfer_raw f = map_data f I I I
-fun map_known_frees f = map_data I f I I
-fun map_compound_rhs f = map_data I I f I
-fun map_relator_eq f = map_data I I I f
+fun map_transfer_raw f = map_data f I I I I
+fun map_known_frees f = map_data I f I I I
+fun map_compound_rhs f = map_data I I f I I
+fun map_relator_eq f = map_data I I I f I
+fun map_relator_eq_raw f = map_data I I I I f
fun add_transfer_thm thm = Data.map
(map_transfer_raw (Item_Net.update thm) o
@@ -277,12 +287,15 @@
Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
end
+fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
+
fun transfer_tac equiv ctxt i =
let
val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
val start_rule =
if equiv then @{thm transfer_start} else @{thm transfer_start'}
val rules = get_transfer_raw ctxt
+ val eq_rules = get_relator_eq_raw ctxt
(* allow unsolved subgoals only for standard transfer method, not for transfer' *)
val end_tac = if equiv then K all_tac else K no_tac
val err_msg = "Transfer failed to convert goal to an object-logic formula"
@@ -290,7 +303,7 @@
rtac start_rule i THEN
(rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
THEN_ALL_NEW
- (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
+ (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
ORELSE' end_tac)) (i + 1)
handle TERM (_, ts) => raise TERM (err_msg, ts)
in
@@ -307,12 +320,13 @@
val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
val rule1 = transfer_rule_of_term ctxt rhs
val rules = get_transfer_raw ctxt
+ val eq_rules = get_relator_eq_raw ctxt
in
EVERY
[CONVERSION prep_conv i,
rtac @{thm transfer_prover_start} i,
(rtac rule1 THEN_ALL_NEW
- REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
+ (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
rtac @{thm refl} i]
end)
@@ -350,9 +364,9 @@
let
val name = @{binding relator_eq}
fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
- #> add_transfer_thm (abstract_equalities_relator_eq thm)
+ #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
- #> del_transfer_thm (abstract_equalities_relator_eq thm)
+ #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
val add = Thm.declaration_attribute add_thm
val del = Thm.declaration_attribute del_thm
val text = "declaration of relator equality rule (used by transfer method)"
@@ -368,6 +382,8 @@
"transfer rule for transfer method"
#> Global_Theory.add_thms_dynamic
(@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
+ #> Global_Theory.add_thms_dynamic
+ (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
#> Method.setup @{binding transfer} (transfer_method true)
"generic theorem transfer method"
#> Method.setup @{binding transfer'} (transfer_method false)
--- a/src/HOL/Transfer.thy Sat Mar 16 21:26:44 2013 +0100
+++ b/src/HOL/Transfer.thy Sat Mar 16 21:44:04 2013 +0100
@@ -57,6 +57,9 @@
definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
where "is_equality R \<longleftrightarrow> R = (op =)"
+lemma is_equality_eq: "is_equality (op =)"
+ unfolding is_equality_def by simp
+
text {* Handling of meta-logic connectives *}
definition transfer_forall where
@@ -179,9 +182,6 @@
subsection {* Properties of relators *}
-lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
- unfolding is_equality_def by simp
-
lemma right_total_eq [transfer_rule]: "right_total (op =)"
unfolding right_total_def by simp