# HG changeset patch # User wenzelm # Date 1363466644 -3600 # Node ID 8d3614b82c80e4bf8d691ece009bc7b86eef2b44 # Parent a614e456870b515bf897907bb4c3e3324c2158b0# Parent 37f699750430e2b58d4562120de3be92ae18b9bc merged diff -r 37f699750430 -r 8d3614b82c80 src/Doc/ProgProve/Logic.thy --- 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 "\"} 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. diff -r 37f699750430 -r 8d3614b82c80 src/Doc/ProgProve/document/prelude.tex --- 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}} diff -r 37f699750430 -r 8d3614b82c80 src/Doc/ProgProve/document/root.tex --- 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} diff -r 37f699750430 -r 8d3614b82c80 src/HOL/IMP/Live_True.thy --- 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 \ vname set \ vname set" where "L SKIP X = X" | -"L (x ::= a) X = (if x \ X then X - {x} \ vars a else X)" | +"L (x ::= a) X = (if x \ X then vars a \ (X - {x}) else X)" | "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \ L c\<^isub>2) X" | "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \ L c\<^isub>1 X \ L c\<^isub>2 X" | "L (WHILE b DO c) X = lfp(\Y. vars b \ X \ L c Y)" diff -r 37f699750430 -r 8d3614b82c80 src/HOL/Library/RBT_Mapping.thy --- 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)" diff -r 37f699750430 -r 8d3614b82c80 src/HOL/Tools/transfer.ML --- 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) diff -r 37f699750430 -r 8d3614b82c80 src/HOL/Transfer.thy --- 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 \ 'a \ bool) \ bool" where "is_equality R \ 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