HOL/W0/README

# HG changeset patch # User huffman # Date 1266965083 28800 # Node ID f9801fdeb7890e9630f3a8863c3438e238494d26 # Parent c6331256b087d736b8f3ec15fb0d6d53ea40e626# Parent cac5a37fb638c0afbec149b4631746bae893a4e2 merged diff -r c6331256b087 -r f9801fdeb789 NEWS --- a/NEWS Tue Feb 23 14:44:24 2010 -0800 +++ b/NEWS Tue Feb 23 14:44:43 2010 -0800 @@ -122,9 +122,6 @@ INCOMPATIBILITY. -* New theory Algebras contains generic algebraic structures and -generic algebraic operations. - * HOLogic.strip_psplit: types are returned in syntactic order, similar to other strip and tuple operations. INCOMPATIBILITY. diff -r c6331256b087 -r f9801fdeb789 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 14:44:24 2010 -0800 +++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 14:44:43 2010 -0800 @@ -150,11 +150,11 @@ \postw The results presented here were obtained using the JNI version of MiniSat and -with multithreading disabled to reduce nondeterminism. This was done by adding -the line +with multithreading disabled to reduce nondeterminism and a time limit of +15~seconds (instead of 30~seconds). This was done by adding the line \prew -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1] +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$] \postw after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with @@ -499,7 +499,7 @@ \prew \textbf{lemma} ``$P~\textit{Suc}$'' \\ -\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount] +\textbf{nitpick} \\[2\smallskipamount] \slshape Nitpick found no counterexample. \postw @@ -1617,7 +1617,7 @@ ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\ ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\ \textbf{nitpick} \\[2\smallskipamount] -\slshape Nitpick found no counterexample. +\slshape Nitpick ran out of time after checking 7 of 8 scopes. \postw \subsection{AA Trees} @@ -1726,7 +1726,7 @@ ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\ ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\ \textbf{nitpick} \\[2\smallskipamount] -{\slshape Nitpick found no counterexample.} +{\slshape Nitpick ran out of time after checking 7 of 8 scopes.} \postw Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree diff -r c6331256b087 -r f9801fdeb789 src/HOL/Algebra/abstract/Ideal2.thy --- a/src/HOL/Algebra/abstract/Ideal2.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,6 +1,5 @@ (* Ideals for commutative rings - $Id$ Author: Clemens Ballarin, started 24 September 1999 *) @@ -23,9 +22,8 @@ text {* Principle ideal domains *} -axclass pid < "domain" - pid_ax: "is_ideal I ==> is_pideal I" - +class pid = + assumes pid_ax: "is_ideal (I :: 'a::domain \ _) \ is_pideal I" (* is_ideal *) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Tue Feb 23 14:44:24 2010 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -(* Title: HOL/Algebras.thy - Author: Florian Haftmann, TU Muenchen -*) - -header {* Generic algebraic structures and operations *} - -theory Algebras -imports HOL -begin - -text {* - These locales provide basic structures for interpretation into - bigger structures; extensions require careful thinking, otherwise - undesired effects may occur due to interpretation. -*} - -ML {* -structure Ac_Simps = Named_Thms( - val name = "ac_simps" - val description = "associativity and commutativity simplification rules" -) -*} - -setup Ac_Simps.setup - -locale semigroup = - fixes f :: "'a \ 'a \ 'a" (infixl "*" 70) - assumes assoc [ac_simps]: "a * b * c = a * (b * c)" - -locale abel_semigroup = semigroup + - assumes commute [ac_simps]: "a * b = b * a" -begin - -lemma left_commute [ac_simps]: - "b * (a * c) = a * (b * c)" -proof - - have "(b * a) * c = (a * b) * c" - by (simp only: commute) - then show ?thesis - by (simp only: assoc) -qed - -end - -locale semilattice = abel_semigroup + - assumes idem [simp]: "a * a = a" -begin - -lemma left_idem [simp]: - "a * (a * b) = a * b" - by (simp add: assoc [symmetric]) - -end - -end \ No newline at end of file diff -r c6331256b087 -r f9801fdeb789 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Bali/Decl.thy Tue Feb 23 14:44:43 2010 -0800 @@ -230,18 +230,22 @@ datatype memberid = fid vname | mid sig -axclass has_memberid < "type" -consts - memberid :: "'a::has_memberid \ memberid" +class has_memberid = + fixes memberid :: "'a \ memberid" -instance memberdecl::has_memberid .. +instantiation memberdecl :: has_memberid +begin -defs (overloaded) +definition memberdecl_memberid_def: "memberid m \ (case m of fdecl (vn,f) \ fid vn | mdecl (sig,m) \ mid sig)" +instance .. + +end + lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn" by (simp add: memberdecl_memberid_def) @@ -254,12 +258,17 @@ lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)" by (cases m) (simp add: memberdecl_memberid_def) -instance * :: (type, has_memberid) has_memberid .. +instantiation * :: (type, has_memberid) has_memberid +begin -defs (overloaded) +definition pair_memberid_def: "memberid p \ memberid (snd p)" +instance .. + +end + lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m" by (simp add: pair_memberid_def) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Bali/DeclConcepts.thy Tue Feb 23 14:44:43 2010 -0800 @@ -79,41 +79,60 @@ text {* overloaded selector @{text accmodi} to select the access modifier out of various HOL types *} -axclass has_accmodi < "type" -consts accmodi:: "'a::has_accmodi \ acc_modi" +class has_accmodi = + fixes accmodi:: "'a \ acc_modi" + +instantiation acc_modi :: has_accmodi +begin -instance acc_modi::has_accmodi .. +definition + acc_modi_accmodi_def: "accmodi (a::acc_modi) \ a" -defs (overloaded) -acc_modi_accmodi_def: "accmodi (a::acc_modi) \ a" +instance .. + +end lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" by (simp add: acc_modi_accmodi_def) -instance decl_ext_type:: ("type") has_accmodi .. +instantiation decl_ext_type:: (type) has_accmodi +begin -defs (overloaded) -decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \ access d" +definition + decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \ access d" +instance .. + +end lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d" by (simp add: decl_acc_modi_def) -instance * :: ("type",has_accmodi) has_accmodi .. +instantiation * :: (type, has_accmodi) has_accmodi +begin -defs (overloaded) -pair_acc_modi_def: "accmodi p \ (accmodi (snd p))" +definition + pair_acc_modi_def: "accmodi p \ (accmodi (snd p))" + +instance .. + +end lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)" by (simp add: pair_acc_modi_def) -instance memberdecl :: has_accmodi .. +instantiation memberdecl :: has_accmodi +begin -defs (overloaded) -memberdecl_acc_modi_def: "accmodi m \ (case m of +definition + memberdecl_acc_modi_def: "accmodi m \ (case m of fdecl f \ accmodi f | mdecl m \ accmodi m)" +instance .. + +end + lemma memberdecl_fdecl_acc_modi_simp[simp]: "accmodi (fdecl m) = accmodi m" by (simp add: memberdecl_acc_modi_def) @@ -125,21 +144,35 @@ text {* overloaded selector @{text declclass} to select the declaring class out of various HOL types *} -axclass has_declclass < "type" -consts declclass:: "'a::has_declclass \ qtname" +class has_declclass = + fixes declclass:: "'a \ qtname" + +instantiation qtname_ext_type :: (type) has_declclass +begin -instance qtname_ext_type::("type") has_declclass .. +definition + "declclass q \ \ pid = pid q, tid = tid q \" + +instance .. -defs (overloaded) -qtname_declclass_def: "declclass (q::qtname) \ q" +end + +lemma qtname_declclass_def: + "declclass q \ (q::qtname)" + by (induct q) (simp add: declclass_qtname_ext_type_def) lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" by (simp add: qtname_declclass_def) -instance * :: ("has_declclass","type") has_declclass .. +instantiation * :: (has_declclass, type) has_declclass +begin -defs (overloaded) -pair_declclass_def: "declclass p \ declclass (fst p)" +definition + pair_declclass_def: "declclass p \ declclass (fst p)" + +instance .. + +end lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" by (simp add: pair_declclass_def) @@ -147,25 +180,38 @@ text {* overloaded selector @{text is_static} to select the static modifier out of various HOL types *} +class has_static = + fixes is_static :: "'a \ bool" -axclass has_static < "type" -consts is_static :: "'a::has_static \ bool" +instantiation decl_ext_type :: (has_static) has_static +begin -instance decl_ext_type :: ("has_static") has_static .. +instance .. + +end -instance member_ext_type :: ("type") has_static .. +instantiation member_ext_type :: (type) has_static +begin + +instance .. -defs (overloaded) -static_field_type_is_static_def: - "is_static (m::('b member_scheme)) \ static m" +end + +axiomatization where + static_field_type_is_static_def: "is_static (m::('a member_scheme)) \ static m" lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" by (simp add: static_field_type_is_static_def) -instance * :: ("type","has_static") has_static .. +instantiation * :: (type, has_static) has_static +begin -defs (overloaded) -pair_is_static_def: "is_static p \ is_static (snd p)" +definition + pair_is_static_def: "is_static p \ is_static (snd p)" + +instance .. + +end lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s" by (simp add: pair_is_static_def) @@ -173,14 +219,19 @@ lemma pair_is_static_simp1: "is_static p = is_static (snd p)" by (simp add: pair_is_static_def) -instance memberdecl:: has_static .. +instantiation memberdecl :: has_static +begin -defs (overloaded) +definition memberdecl_is_static_def: "is_static m \ (case m of fdecl f \ is_static f | mdecl m \ is_static m)" +instance .. + +end + lemma memberdecl_is_static_fdecl_simp[simp]: "is_static (fdecl f) = is_static f" by (simp add: memberdecl_is_static_def) @@ -389,18 +440,32 @@ text {* overloaded selector @{text resTy} to select the result type out of various HOL types *} -axclass has_resTy < "type" -consts resTy:: "'a::has_resTy \ ty" +class has_resTy = + fixes resTy:: "'a \ ty" + +instantiation decl_ext_type :: (has_resTy) has_resTy +begin -instance decl_ext_type :: ("has_resTy") has_resTy .. +instance .. + +end + +instantiation member_ext_type :: (has_resTy) has_resTy +begin -instance member_ext_type :: ("has_resTy") has_resTy .. +instance .. -instance mhead_ext_type :: ("type") has_resTy .. +end + +instantiation mhead_ext_type :: (type) has_resTy +begin -defs (overloaded) -mhead_ext_type_resTy_def: - "resTy (m::('b mhead_scheme)) \ resT m" +instance .. + +end + +axiomatization where + mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \ resT m" lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" by (simp add: mhead_ext_type_resTy_def) @@ -408,10 +473,15 @@ lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" by (simp add: mhead_def mhead_resTy_simp) -instance * :: ("type","has_resTy") has_resTy .. +instantiation * :: ("type","has_resTy") has_resTy +begin -defs (overloaded) -pair_resTy_def: "resTy p \ resTy (snd p)" +definition + pair_resTy_def: "resTy p \ resTy (snd p)" + +instance .. + +end lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m" by (simp add: pair_resTy_def) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Bali/Name.thy --- a/src/HOL/Bali/Name.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Bali/Name.thy Tue Feb 23 14:44:43 2010 -0800 @@ -48,29 +48,34 @@ pid :: pname tid :: tname -axclass has_pname < "type" -consts pname::"'a::has_pname \ pname" +class has_pname = + fixes pname :: "'a \ pname" -instance pname::has_pname .. +instantiation pname :: has_pname +begin -defs (overloaded) -pname_pname_def: "pname (p::pname) \ p" +definition + pname_pname_def: "pname (p::pname) \ p" -axclass has_tname < "type" -consts tname::"'a::has_tname \ tname" +instance .. + +end -instance tname::has_tname .. +class has_tname = + fixes tname :: "'a \ tname" -defs (overloaded) -tname_tname_def: "tname (t::tname) \ t" +instantiation tname :: has_tname +begin -axclass has_qtname < type -consts qtname:: "'a::has_qtname \ qtname" +definition + tname_tname_def: "tname (t::tname) \ t" + +instance .. -instance qtname_ext_type :: (type) has_qtname .. +end -defs (overloaded) -qtname_qtname_def: "qtname (q::qtname) \ q" +definition + qtname_qtname_def: "qtname (q::'a qtname_ext_type) \ q" translations "mname" <= "Name.mname" diff -r c6331256b087 -r f9801fdeb789 src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Bali/Term.thy Tue Feb 23 14:44:43 2010 -0800 @@ -295,8 +295,8 @@ following. *} -axclass inj_term < "type" -consts inj_term:: "'a::inj_term \ term" ("\_\" 1000) +class inj_term = + fixes inj_term:: "'a \ term" ("\_\" 1000) text {* How this overloaded injections work can be seen in the theory @{text DefiniteAssignment}. Other big inductive relations on @@ -308,10 +308,15 @@ as bridge between the different conventions. *} -instance stmt::inj_term .. +instantiation stmt :: inj_term +begin -defs (overloaded) -stmt_inj_term_def: "\c::stmt\ \ In1r c" +definition + stmt_inj_term_def: "\c::stmt\ \ In1r c" + +instance .. + +end lemma stmt_inj_term_simp: "\c::stmt\ = In1r c" by (simp add: stmt_inj_term_def) @@ -319,10 +324,15 @@ lemma stmt_inj_term [iff]: "\x::stmt\ = \y\ \ x = y" by (simp add: stmt_inj_term_simp) -instance expr::inj_term .. +instantiation expr :: inj_term +begin -defs (overloaded) -expr_inj_term_def: "\e::expr\ \ In1l e" +definition + expr_inj_term_def: "\e::expr\ \ In1l e" + +instance .. + +end lemma expr_inj_term_simp: "\e::expr\ = In1l e" by (simp add: expr_inj_term_def) @@ -330,10 +340,15 @@ lemma expr_inj_term [iff]: "\x::expr\ = \y\ \ x = y" by (simp add: expr_inj_term_simp) -instance var::inj_term .. +instantiation var :: inj_term +begin -defs (overloaded) -var_inj_term_def: "\v::var\ \ In2 v" +definition + var_inj_term_def: "\v::var\ \ In2 v" + +instance .. + +end lemma var_inj_term_simp: "\v::var\ = In2 v" by (simp add: var_inj_term_def) @@ -341,10 +356,32 @@ lemma var_inj_term [iff]: "\x::var\ = \y\ \ x = y" by (simp add: var_inj_term_simp) -instance "list":: (type) inj_term .. +class expr_of = + fixes expr_of :: "'a \ expr" + +instantiation expr :: expr_of +begin + +definition + "expr_of = (\(e::expr). e)" + +instance .. + +end -defs (overloaded) -expr_list_inj_term_def: "\es::expr list\ \ In3 es" +instantiation list :: (expr_of) inj_term +begin + +definition + "\es::'a list\ \ In3 (map expr_of es)" + +instance .. + +end + +lemma expr_list_inj_term_def: + "\es::expr list\ \ In3 es" + by (simp add: inj_term_list_def expr_of_expr_def) lemma expr_list_inj_term_simp: "\es::expr list\ = In3 es" by (simp add: expr_list_inj_term_def) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy --- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Tue Feb 23 14:44:43 2010 -0800 @@ -56,10 +56,12 @@ text {* Let's find out which assertions of @{text max} are hard to prove: *} -boogie_status (narrow timeout: 4) max +boogie_status (narrow step_timeout: 4 final_timeout: 15) max (simp add: labels, (fast | metis)?) - -- {* The argument @{text timeout} is optional, restricting the runtime of - each narrowing step by the given number of seconds. *} + -- {* The argument @{text step_timeout} is optional, restricting the runtime + of each intermediate narrowing step by the given number of seconds. *} + -- {* The argument @{text final_timeout} is optional, restricting the + runtime of the final narrowing steps by the given number of seconds. *} -- {* The last argument should be a method to be applied at each narrowing step. Note that different methods may be composed to one method by a language similar to regular expressions. *} diff -r c6331256b087 -r f9801fdeb789 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Tue Feb 23 14:44:43 2010 -0800 @@ -156,26 +156,27 @@ |> Seq.hd |> Proof.global_done_proof in -fun boogie_narrow_vc timeout vc_name meth thy = +fun boogie_narrow_vc (quick, timeout) vc_name meth thy = let - val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth) + fun tp t = TimeLimit.timeLimit (Time.fromSeconds t) (prove thy meth) - fun try_vc (tag, split_tag) split vc = (trying tag; - (case try tp vc of + fun try_vc t (tag, split_tag) split vc = (trying tag; + (case try (tp t) vc of SOME _ => (success_on tag; []) | NONE => (failure_on tag split_tag; split vc))) fun some_asserts vc = - try_vc (string_of_asserts vc, - if Boogie_VCs.size_of vc = 1 then "." else ", further splitting ...") - (divide some_asserts) vc + let + val (t, sep) = if Boogie_VCs.size_of vc = 1 then (timeout, ".") + else (quick, ", further splitting ...") + in try_vc t (string_of_asserts vc, sep) (divide some_asserts) vc end fun single_path p = - try_vc (string_of_path p, ", splitting into assertions ...") + try_vc quick (string_of_path p, ", splitting into assertions ...") (divide some_asserts) val complete_vc = - try_vc ("full goal", ", splitting into paths ...") + try_vc quick ("full goal", ", splitting into paths ...") (par_map (uncurry single_path) o itemize_paths o Boogie_VCs.paths_of) val unsolved = complete_vc (get_vc thy vc_name) @@ -262,15 +263,18 @@ (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args)))) -val default_timeout = 5 +val quick_timeout = 5 +val default_timeout = 20 + +fun timeout name = Scan.optional (scan_val name OuterParse.nat) val status_test = scan_arg ( - (Args.$$$ "scan" >> K boogie_scan_vc || - Args.$$$ "narrow" >> K boogie_narrow_vc) -- - Scan.optional (scan_val "timeout" OuterParse.nat) default_timeout) -- + Args.$$$ "scan" |-- timeout "timeout" quick_timeout >> boogie_scan_vc || + Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout -- + timeout "final_timeout" default_timeout >> boogie_narrow_vc) -- vc_name -- Method.parse >> - (fn (((f, timeout), vc_name), meth) => f timeout vc_name meth) + (fn ((f, vc_name), meth) => f vc_name meth) val status_vc = (scan_arg diff -r c6331256b087 -r f9801fdeb789 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Code_Evaluation.thy Tue Feb 23 14:44:43 2010 -0800 @@ -76,7 +76,8 @@ andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; in if need_inst then add_term_of tyco raw_vs thy else thy end; in - Code.type_interpretation ensure_term_of + Code.datatype_interpretation ensure_term_of + #> Code.abstype_interpretation ensure_term_of end *} @@ -114,7 +115,7 @@ val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; in - Code.type_interpretation ensure_term_of_code + Code.datatype_interpretation ensure_term_of_code end *} diff -r c6331256b087 -r f9801fdeb789 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Groups.thy Tue Feb 23 14:44:43 2010 -0800 @@ -9,6 +9,65 @@ uses ("~~/src/Provers/Arith/abel_cancel.ML") begin +subsection {* Fact collections *} + +ML {* +structure Algebra_Simps = Named_Thms( + val name = "algebra_simps" + val description = "algebra simplification rules" +) +*} + +setup Algebra_Simps.setup + +text{* The rewrites accumulated in @{text algebra_simps} deal with the +classical algebraic structures of groups, rings and family. They simplify +terms by multiplying everything out (in case of a ring) and bringing sums and +products into a canonical form (by ordered rewriting). As a result it decides +group and ring equalities but also helps with inequalities. + +Of course it also works for fields, but it knows nothing about multiplicative +inverses or division. This is catered for by @{text field_simps}. *} + + +ML {* +structure Ac_Simps = Named_Thms( + val name = "ac_simps" + val description = "associativity and commutativity simplification rules" +) +*} + +setup Ac_Simps.setup + + +subsection {* Abstract structures *} + +text {* + These locales provide basic structures for interpretation into + bigger structures; extensions require careful thinking, otherwise + undesired effects may occur due to interpretation. +*} + +locale semigroup = + fixes f :: "'a \ 'a \ 'a" (infixl "*" 70) + assumes assoc [ac_simps]: "a * b * c = a * (b * c)" + +locale abel_semigroup = semigroup + + assumes commute [ac_simps]: "a * b = b * a" +begin + +lemma left_commute [ac_simps]: + "b * (a * c) = a * (b * c)" +proof - + have "(b * a) * c = (a * b) * c" + by (simp only: commute) + then show ?thesis + by (simp only: assoc) +qed + +end + + subsection {* Generic operations *} class zero = @@ -64,37 +123,6 @@ use "~~/src/Provers/Arith/abel_cancel.ML" -text {* - The theory of partially ordered groups is taken from the books: - \begin{itemize} - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 - \end{itemize} - Most of the used notions can also be looked up in - \begin{itemize} - \item \url{http://www.mathworld.com} by Eric Weisstein et. al. - \item \emph{Algebra I} by van der Waerden, Springer. - \end{itemize} -*} - -ML {* -structure Algebra_Simps = Named_Thms( - val name = "algebra_simps" - val description = "algebra simplification rules" -) -*} - -setup Algebra_Simps.setup - -text{* The rewrites accumulated in @{text algebra_simps} deal with the -classical algebraic structures of groups, rings and family. They simplify -terms by multiplying everything out (in case of a ring) and bringing sums and -products into a canonical form (by ordered rewriting). As a result it decides -group and ring equalities but also helps with inequalities. - -Of course it also works for fields, but it knows nothing about multiplicative -inverses or division. This is catered for by @{text field_simps}. *} - subsection {* Semigroups and Monoids *} @@ -144,19 +172,6 @@ theorems mult_ac = mult_assoc mult_commute mult_left_commute -class ab_semigroup_idem_mult = ab_semigroup_mult + - assumes mult_idem: "x * x = x" - -sublocale ab_semigroup_idem_mult < times!: semilattice times proof -qed (fact mult_idem) - -context ab_semigroup_idem_mult -begin - -lemmas mult_left_idem = times.left_idem - -end - class monoid_add = zero + semigroup_add + assumes add_0_left [simp]: "0 + a = a" and add_0_right [simp]: "a + 0 = a" @@ -411,6 +426,19 @@ subsection {* (Partially) Ordered Groups *} +text {* + The theory of partially ordered groups is taken from the books: + \begin{itemize} + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 + \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 + \end{itemize} + Most of the used notions can also be looked up in + \begin{itemize} + \item \url{http://www.mathworld.com} by Eric Weisstein et. al. + \item \emph{Algebra I} by van der Waerden, Springer. + \end{itemize} +*} + class ordered_ab_semigroup_add = order + ab_semigroup_add + assumes add_left_mono: "a \ b \ c + a \ c + b" begin diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Examples.thy --- a/src/HOL/Hoare/Examples.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/Examples.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,12 +1,11 @@ (* Title: HOL/Hoare/Examples.thy - ID: $Id$ Author: Norbert Galm Copyright 1998 TUM Various examples. *) -theory Examples imports Hoare Arith2 begin +theory Examples imports Hoare_Logic Arith2 begin (*** ARITHMETIC ***) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/ExamplesAbort.thy --- a/src/HOL/Hoare/ExamplesAbort.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/ExamplesAbort.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,12 +1,11 @@ (* Title: HOL/Hoare/ExamplesAbort.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Some small examples for programs that may abort. *) -theory ExamplesAbort imports HoareAbort begin +theory ExamplesAbort imports Hoare_Logic_Abort begin lemma "VARS x y z::nat {y = z & z \ 0} z \ 0 \ x := y div z {x = 1}" diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/HeapSyntax.thy --- a/src/HOL/Hoare/HeapSyntax.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/HeapSyntax.thy Tue Feb 23 14:44:43 2010 -0800 @@ -3,7 +3,7 @@ Copyright 2002 TUM *) -theory HeapSyntax imports Hoare Heap begin +theory HeapSyntax imports Hoare_Logic Heap begin subsection "Field access and update" diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/HeapSyntaxAbort.thy --- a/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 14:44:43 2010 -0800 @@ -3,7 +3,7 @@ Copyright 2002 TUM *) -theory HeapSyntaxAbort imports HoareAbort Heap begin +theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin subsection "Field access and update" diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/Hoare.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,245 +1,9 @@ -(* Title: HOL/Hoare/Hoare.thy - Author: Leonor Prensa Nieto & Tobias Nipkow - Copyright 1998 TUM - -Sugared semantic embedding of Hoare logic. -Strictly speaking a shallow embedding (as implemented by Norbert Galm -following Mike Gordon) would suffice. Maybe the datatype com comes in useful -later. +(* Author: Tobias Nipkow + Copyright 1998-2003 TUM *) theory Hoare -imports Main -uses ("hoare_tac.ML") +imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation begin -types - 'a bexp = "'a set" - 'a assn = "'a set" - -datatype - 'a com = Basic "'a \ 'a" - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) - -abbreviation annskip ("SKIP") where "SKIP == Basic id" - -types 'a sem = "'a => 'a => bool" - -consts iter :: "nat => 'a bexp => 'a sem => 'a sem" -primrec -"iter 0 b S = (%s s'. s ~: b & (s=s'))" -"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))" - -consts Sem :: "'a com => 'a sem" -primrec -"Sem(Basic f) s s' = (s' = f s)" -"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" -"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & - (s ~: b --> Sem c2 s s'))" -"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" - -constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" - - - -(** parse translations **) - -syntax - "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) - -syntax - "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax ("" output) - "_hoare" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) -ML {* - -local - -fun abs((a,T),body) = - let val a = absfree(a, dummyT, body) - in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end -in - -fun mk_abstuple [x] body = abs (x, body) - | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); - -fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b - | mk_fbody a e ((b,_)::xs) = - Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs; - -fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) end -*} - -(* bexp_tr & assn_tr *) -(*all meta-variables for bexp except for TRUE are translated as if they - were boolean expressions*) -ML{* -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) - | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; - -fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; -*} -(* com_tr *) -ML{* -fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = - Syntax.const @{const_syntax Basic} $ mk_fexp a e xs - | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f - | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = - Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = - Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = - Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs - | com_tr t _ = t (* if t is just a Free/Var *) -*} - -(* triple_tr *) (* FIXME does not handle "_idtdummy" *) -ML{* -local - -fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) - | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T); - -fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars - | vars_tr t = [var_tr t] - -in -fun hoare_vars_tr [vars, pre, prg, post] = - let val xs = vars_tr vars - in Syntax.const @{const_syntax Valid} $ - assn_tr pre xs $ com_tr prg xs $ assn_tr post xs - end - | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); -end -*} - -parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} - - -(*****************************************************************************) - -(*** print translations ***) -ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = - subst_bound (Syntax.free v, dest_abstuple body) - | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) - | dest_abstuple trm = trm; - -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] - | abs2list _ = []; - -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t - | mk_ts (Abs(x,_,t)) = mk_ts t - | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) - | mk_ts t = [t]; - -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = - ((Syntax.free x)::(abs2list t), mk_ts t) - | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) - | mk_vts t = raise Match; - -fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) - | find_ch ((v,t)::vts) i xs = - if t = Bound i then find_ch vts (i-1) xs - else (true, (v, subst_bounds (xs, t))); - -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true - | is_f (Abs(x,_,t)) = true - | is_f t = false; -*} - -(* assn_tr' & bexp_tr'*) -ML{* -fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | assn_tr' (Const (@{const_syntax inter}, _) $ - (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) = - Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 - | assn_tr' t = t; - -fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | bexp_tr' t = t; -*} - -(*com_tr' *) -ML{* -fun mk_assign f = - let val (vs, ts) = mk_vts f; - val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) - in - if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which - else Syntax.const @{const_syntax annskip} - end; - -fun com_tr' (Const (@{const_syntax Basic},_) $ f) = - if is_f f then mk_assign f - else Syntax.const @{const_syntax Basic} $ f - | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = - Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = - Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = - Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c - | com_tr' t = t; - -fun spec_tr' [p, c, q] = - Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q -*} - -print_translation {* [(@{const_syntax Valid}, spec_tr')] *} - -lemma SkipRule: "p \ q \ Valid p (Basic id) q" -by (auto simp:Valid_def) - -lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" -by (auto simp:Valid_def) - -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" -by (auto simp:Valid_def) - -lemma CondRule: - "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} - \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" -by (auto simp:Valid_def) - -lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==> - (\s s'. s : I \ iter n b (Sem c) s s' \ s' : I & s' ~: b)"; -apply(induct n) - apply clarsimp -apply(simp (no_asm_use)) -apply blast -done - -lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" -apply (clarsimp simp:Valid_def) -apply(drule iter_aux) - prefer 2 apply assumption - apply blast -apply blast -done - - -lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" - by blast - -lemmas AbortRule = SkipRule -- "dummy version" -use "hoare_tac.ML" - -method_setup vcg = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} - "verification condition generator" - -method_setup vcg_simp = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} - "verification condition generator plus simplification" - -end diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/HoareAbort.thy --- a/src/HOL/Hoare/HoareAbort.thy Tue Feb 23 14:44:24 2010 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,269 +0,0 @@ -(* Title: HOL/Hoare/HoareAbort.thy - Author: Leonor Prensa Nieto & Tobias Nipkow - Copyright 2003 TUM - -Like Hoare.thy, but with an Abort statement for modelling run time errors. -*) - -theory HoareAbort -imports Main -uses ("hoare_tac.ML") -begin - -types - 'a bexp = "'a set" - 'a assn = "'a set" - -datatype - 'a com = Basic "'a \ 'a" - | Abort - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) - -abbreviation annskip ("SKIP") where "SKIP == Basic id" - -types 'a sem = "'a option => 'a option => bool" - -consts iter :: "nat => 'a bexp => 'a sem => 'a sem" -primrec -"iter 0 b S = (\s s'. s \ Some ` b \ s=s')" -"iter (Suc n) b S = - (\s s'. s \ Some ` b \ (\s''. S s s'' \ iter n b S s'' s'))" - -consts Sem :: "'a com => 'a sem" -primrec -"Sem(Basic f) s s' = (case s of None \ s' = None | Some t \ s' = Some(f t))" -"Sem Abort s s' = (s' = None)" -"Sem(c1;c2) s s' = (\s''. Sem c1 s s'' \ Sem c2 s'' s')" -"Sem(IF b THEN c1 ELSE c2 FI) s s' = - (case s of None \ s' = None - | Some t \ ((t \ b \ Sem c1 s s') \ (t \ b \ Sem c2 s s')))" -"Sem(While b x c) s s' = - (if s = None then s' = None else \n. iter n b (Sem c) s s')" - -constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - "Valid p c q == \s s'. Sem c s s' \ s : Some ` p \ s' : Some ` q" - - - -(** parse translations **) - -syntax - "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) - -syntax - "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax ("" output) - "_hoare" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) -ML {* - -local -fun free a = Free(a,dummyT) -fun abs((a,T),body) = - let val a = absfree(a, dummyT, body) - in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end -in - -fun mk_abstuple [x] body = abs (x, body) - | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); - -fun mk_fbody a e [x as (b,_)] = if a=b then e else free b - | mk_fbody a e ((b,_)::xs) = - Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs; - -fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) -end -*} - -(* bexp_tr & assn_tr *) -(*all meta-variables for bexp except for TRUE are translated as if they - were boolean expressions*) -ML{* -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) - | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; - -fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; -*} -(* com_tr *) -ML{* -fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = - Syntax.const @{const_syntax Basic} $ mk_fexp a e xs - | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f - | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = - Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = - Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = - Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs - | com_tr t _ = t (* if t is just a Free/Var *) -*} - -(* triple_tr *) (* FIXME does not handle "_idtdummy" *) -ML{* -local - -fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *) - | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T); - -fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars - | vars_tr t = [var_tr t] - -in -fun hoare_vars_tr [vars, pre, prg, post] = - let val xs = vars_tr vars - in Syntax.const @{const_syntax Valid} $ - assn_tr pre xs $ com_tr prg xs $ assn_tr post xs - end - | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); -end -*} - -parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} - - -(*****************************************************************************) - -(*** print translations ***) -ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = - subst_bound (Syntax.free v, dest_abstuple body) - | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) - | dest_abstuple trm = trm; - -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] - | abs2list _ = []; - -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t - | mk_ts (Abs(x,_,t)) = mk_ts t - | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) - | mk_ts t = [t]; - -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = - ((Syntax.free x)::(abs2list t), mk_ts t) - | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) - | mk_vts t = raise Match; - -fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) - | find_ch ((v,t)::vts) i xs = - if t = Bound i then find_ch vts (i-1) xs - else (true, (v, subst_bounds (xs,t))); - -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true - | is_f (Abs(x,_,t)) = true - | is_f t = false; -*} - -(* assn_tr' & bexp_tr'*) -ML{* -fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $ - (Const (@{const_syntax Collect},_) $ T2)) = - Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 - | assn_tr' t = t; - -fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | bexp_tr' t = t; -*} - -(*com_tr' *) -ML{* -fun mk_assign f = - let val (vs, ts) = mk_vts f; - val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) - in - if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which - else Syntax.const @{const_syntax annskip} - end; - -fun com_tr' (Const (@{const_syntax Basic},_) $ f) = - if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f - | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = - Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = - Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = - Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c - | com_tr' t = t; - -fun spec_tr' [p, c, q] = - Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q -*} - -print_translation {* [(@{const_syntax Valid}, spec_tr')] *} - -(*** The proof rules ***) - -lemma SkipRule: "p \ q \ Valid p (Basic id) q" -by (auto simp:Valid_def) - -lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" -by (auto simp:Valid_def) - -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" -by (auto simp:Valid_def) - -lemma CondRule: - "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} - \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" -by (fastsimp simp:Valid_def image_def) - -lemma iter_aux: - "! s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ - (\s s'. s \ Some ` I \ iter n b (Sem c) s s' \ s' \ Some ` (I \ -b))"; -apply(unfold image_def) -apply(induct n) - apply clarsimp -apply(simp (no_asm_use)) -apply blast -done - -lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" -apply(simp add:Valid_def) -apply(simp (no_asm) add:image_def) -apply clarify -apply(drule iter_aux) - prefer 2 apply assumption - apply blast -apply blast -done - -lemma AbortRule: "p \ {s. False} \ Valid p Abort q" -by(auto simp:Valid_def) - - -subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} - -lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" - by blast - -use "hoare_tac.ML" - -method_setup vcg = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} - "verification condition generator" - -method_setup vcg_simp = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} - "verification condition generator plus simplification" - -(* Special syntax for guarded statements and guarded array updates: *) - -syntax - guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) - array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) -translations - "P \ c" == "IF P THEN c ELSE CONST Abort FI" - "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" - (* reverse translation not possible because of duplicate "a" *) - -text{* Note: there is no special syntax for guarded array access. Thus -you must write @{text"j < length a \ a[i] := a!j"}. *} - -end diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Hoare_Logic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Feb 23 14:44:43 2010 -0800 @@ -0,0 +1,245 @@ +(* Title: HOL/Hoare/Hoare.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM + +Sugared semantic embedding of Hoare logic. +Strictly speaking a shallow embedding (as implemented by Norbert Galm +following Mike Gordon) would suffice. Maybe the datatype com comes in useful +later. +*) + +theory Hoare_Logic +imports Main +uses ("hoare_tac.ML") +begin + +types + 'a bexp = "'a set" + 'a assn = "'a set" + +datatype + 'a com = Basic "'a \ 'a" + | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) + | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +abbreviation annskip ("SKIP") where "SKIP == Basic id" + +types 'a sem = "'a => 'a => bool" + +consts iter :: "nat => 'a bexp => 'a sem => 'a sem" +primrec +"iter 0 b S = (%s s'. s ~: b & (s=s'))" +"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))" + +consts Sem :: "'a com => 'a sem" +primrec +"Sem(Basic f) s s' = (s' = f s)" +"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" +"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & + (s ~: b --> Sem c2 s s'))" +"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" + +constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" + + + +(** parse translations **) + +syntax + "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) + +syntax + "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) +syntax ("" output) + "_hoare" :: "['a assn,'a com,'a assn] => bool" + ("{_} // _ // {_}" [0,55,0] 50) +ML {* + +local + +fun abs((a,T),body) = + let val a = absfree(a, dummyT, body) + in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end +in + +fun mk_abstuple [x] body = abs (x, body) + | mk_abstuple (x::xs) body = + Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + +fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b + | mk_fbody a e ((b,_)::xs) = + Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs; + +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) +end +*} + +(* bexp_tr & assn_tr *) +(*all meta-variables for bexp except for TRUE are translated as if they + were boolean expressions*) +ML{* +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) + | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; + +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; +*} +(* com_tr *) +ML{* +fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = + Syntax.const @{const_syntax Basic} $ mk_fexp a e xs + | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f + | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = + Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = + Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = + Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr t _ = t (* if t is just a Free/Var *) +*} + +(* triple_tr *) (* FIXME does not handle "_idtdummy" *) +ML{* +local + +fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) + | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T); + +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars + | vars_tr t = [var_tr t] + +in +fun hoare_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const @{const_syntax Valid} $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); +end +*} + +parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} + + +(*****************************************************************************) + +(*** print translations ***) +ML{* +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = + subst_bound (Syntax.free v, dest_abstuple body) + | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) + | dest_abstuple trm = trm; + +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; + +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t + | mk_ts (Abs(x,_,t)) = mk_ts t + | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) + | mk_ts t = [t]; + +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = + ((Syntax.free x)::(abs2list t), mk_ts t) + | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) + | mk_vts t = raise Match; + +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) + | find_ch ((v,t)::vts) i xs = + if t = Bound i then find_ch vts (i-1) xs + else (true, (v, subst_bounds (xs, t))); + +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true + | is_f (Abs(x,_,t)) = true + | is_f t = false; +*} + +(* assn_tr' & bexp_tr'*) +ML{* +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | assn_tr' (Const (@{const_syntax inter}, _) $ + (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) = + Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 + | assn_tr' t = t; + +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | bexp_tr' t = t; +*} + +(*com_tr' *) +ML{* +fun mk_assign f = + let val (vs, ts) = mk_vts f; + val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) + in + if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which + else Syntax.const @{const_syntax annskip} + end; + +fun com_tr' (Const (@{const_syntax Basic},_) $ f) = + if is_f f then mk_assign f + else Syntax.const @{const_syntax Basic} $ f + | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = + Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = + Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = + Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' t = t; + +fun spec_tr' [p, c, q] = + Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q +*} + +print_translation {* [(@{const_syntax Valid}, spec_tr')] *} + +lemma SkipRule: "p \ q \ Valid p (Basic id) q" +by (auto simp:Valid_def) + +lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" +by (auto simp:Valid_def) + +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +by (auto simp:Valid_def) + +lemma CondRule: + "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} + \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" +by (auto simp:Valid_def) + +lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==> + (\s s'. s : I \ iter n b (Sem c) s s' \ s' : I & s' ~: b)"; +apply(induct n) + apply clarsimp +apply(simp (no_asm_use)) +apply blast +done + +lemma WhileRule: + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" +apply (clarsimp simp:Valid_def) +apply(drule iter_aux) + prefer 2 apply assumption + apply blast +apply blast +done + + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + +lemmas AbortRule = SkipRule -- "dummy version" +use "hoare_tac.ML" + +method_setup vcg = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + "verification condition generator" + +method_setup vcg_simp = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} + "verification condition generator plus simplification" + +end diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Hoare_Logic_Abort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Feb 23 14:44:43 2010 -0800 @@ -0,0 +1,269 @@ +(* Title: HOL/Hoare/HoareAbort.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 2003 TUM + +Like Hoare.thy, but with an Abort statement for modelling run time errors. +*) + +theory Hoare_Logic_Abort +imports Main +uses ("hoare_tac.ML") +begin + +types + 'a bexp = "'a set" + 'a assn = "'a set" + +datatype + 'a com = Basic "'a \ 'a" + | Abort + | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) + | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +abbreviation annskip ("SKIP") where "SKIP == Basic id" + +types 'a sem = "'a option => 'a option => bool" + +consts iter :: "nat => 'a bexp => 'a sem => 'a sem" +primrec +"iter 0 b S = (\s s'. s \ Some ` b \ s=s')" +"iter (Suc n) b S = + (\s s'. s \ Some ` b \ (\s''. S s s'' \ iter n b S s'' s'))" + +consts Sem :: "'a com => 'a sem" +primrec +"Sem(Basic f) s s' = (case s of None \ s' = None | Some t \ s' = Some(f t))" +"Sem Abort s s' = (s' = None)" +"Sem(c1;c2) s s' = (\s''. Sem c1 s s'' \ Sem c2 s'' s')" +"Sem(IF b THEN c1 ELSE c2 FI) s s' = + (case s of None \ s' = None + | Some t \ ((t \ b \ Sem c1 s s') \ (t \ b \ Sem c2 s s')))" +"Sem(While b x c) s s' = + (if s = None then s' = None else \n. iter n b (Sem c) s s')" + +constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + "Valid p c q == \s s'. Sem c s s' \ s : Some ` p \ s' : Some ` q" + + + +(** parse translations **) + +syntax + "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) + +syntax + "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) +syntax ("" output) + "_hoare_abort" :: "['a assn,'a com,'a assn] => bool" + ("{_} // _ // {_}" [0,55,0] 50) +ML {* + +local +fun free a = Free(a,dummyT) +fun abs((a,T),body) = + let val a = absfree(a, dummyT, body) + in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end +in + +fun mk_abstuple [x] body = abs (x, body) + | mk_abstuple (x::xs) body = + Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + +fun mk_fbody a e [x as (b,_)] = if a=b then e else free b + | mk_fbody a e ((b,_)::xs) = + Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs; + +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) +end +*} + +(* bexp_tr & assn_tr *) +(*all meta-variables for bexp except for TRUE are translated as if they + were boolean expressions*) +ML{* +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) + | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; + +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; +*} +(* com_tr *) +ML{* +fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = + Syntax.const @{const_syntax Basic} $ mk_fexp a e xs + | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f + | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = + Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = + Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = + Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr t _ = t (* if t is just a Free/Var *) +*} + +(* triple_tr *) (* FIXME does not handle "_idtdummy" *) +ML{* +local + +fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *) + | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T); + +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars + | vars_tr t = [var_tr t] + +in +fun hoare_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const @{const_syntax Valid} $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); +end +*} + +parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] *} + + +(*****************************************************************************) + +(*** print translations ***) +ML{* +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = + subst_bound (Syntax.free v, dest_abstuple body) + | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) + | dest_abstuple trm = trm; + +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; + +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t + | mk_ts (Abs(x,_,t)) = mk_ts t + | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) + | mk_ts t = [t]; + +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = + ((Syntax.free x)::(abs2list t), mk_ts t) + | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) + | mk_vts t = raise Match; + +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) + | find_ch ((v,t)::vts) i xs = + if t = Bound i then find_ch vts (i-1) xs + else (true, (v, subst_bounds (xs,t))); + +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true + | is_f (Abs(x,_,t)) = true + | is_f t = false; +*} + +(* assn_tr' & bexp_tr'*) +ML{* +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $ + (Const (@{const_syntax Collect},_) $ T2)) = + Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 + | assn_tr' t = t; + +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | bexp_tr' t = t; +*} + +(*com_tr' *) +ML{* +fun mk_assign f = + let val (vs, ts) = mk_vts f; + val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) + in + if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which + else Syntax.const @{const_syntax annskip} + end; + +fun com_tr' (Const (@{const_syntax Basic},_) $ f) = + if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f + | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = + Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = + Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = + Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' t = t; + +fun spec_tr' [p, c, q] = + Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q +*} + +print_translation {* [(@{const_syntax Valid}, spec_tr')] *} + +(*** The proof rules ***) + +lemma SkipRule: "p \ q \ Valid p (Basic id) q" +by (auto simp:Valid_def) + +lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" +by (auto simp:Valid_def) + +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +by (auto simp:Valid_def) + +lemma CondRule: + "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} + \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" +by (fastsimp simp:Valid_def image_def) + +lemma iter_aux: + "! s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ + (\s s'. s \ Some ` I \ iter n b (Sem c) s s' \ s' \ Some ` (I \ -b))"; +apply(unfold image_def) +apply(induct n) + apply clarsimp +apply(simp (no_asm_use)) +apply blast +done + +lemma WhileRule: + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" +apply(simp add:Valid_def) +apply(simp (no_asm) add:image_def) +apply clarify +apply(drule iter_aux) + prefer 2 apply assumption + apply blast +apply blast +done + +lemma AbortRule: "p \ {s. False} \ Valid p Abort q" +by(auto simp:Valid_def) + + +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + +use "hoare_tac.ML" + +method_setup vcg = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + "verification condition generator" + +method_setup vcg_simp = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} + "verification condition generator plus simplification" + +(* Special syntax for guarded statements and guarded array updates: *) + +syntax + guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) + array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) +translations + "P \ c" == "IF P THEN c ELSE CONST Abort FI" + "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" + (* reverse translation not possible because of duplicate "a" *) + +text{* Note: there is no special syntax for guarded array access. Thus +you must write @{text"j < length a \ a[i] := a!j"}. *} + +end diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/Pointer_Examples.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Hoare/Pointers.thy - ID: $Id$ Author: Tobias Nipkow Copyright 2002 TUM diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Pointers0.thy --- a/src/HOL/Hoare/Pointers0.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/Pointers0.thy Tue Feb 23 14:44:43 2010 -0800 @@ -9,12 +9,12 @@ - in fact in some case they appear to get (a bit) more complicated. *) -theory Pointers0 imports Hoare begin +theory Pointers0 imports Hoare_Logic begin subsection "References" -axclass ref < type -consts Null :: "'a::ref" +class ref = + fixes Null :: 'a subsection "Field access and update" diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/ROOT.ML Tue Feb 23 14:44:43 2010 -0800 @@ -1,8 +1,2 @@ -(* Title: HOL/Hoare/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1998-2003 TUM -*) -use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples", - "Pointer_ExamplesAbort", "SchorrWaite", "Separation"]; +use_thy "Hoare"; diff -r c6331256b087 -r f9801fdeb789 src/HOL/Hoare/Separation.thy --- a/src/HOL/Hoare/Separation.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Hoare/Separation.thy Tue Feb 23 14:44:43 2010 -0800 @@ -12,7 +12,7 @@ *) -theory Separation imports HoareAbort SepLogHeap begin +theory Separation imports Hoare_Logic_Abort SepLogHeap begin text{* The semantic definition of a few connectives: *} diff -r c6331256b087 -r f9801fdeb789 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/IsaMakefile Tue Feb 23 14:44:43 2010 -0800 @@ -66,7 +66,6 @@ TLA-Memory \ HOL-UNITY \ HOL-Unix \ - HOL-W0 \ HOL-Word-Examples \ HOL-ZF # ^ this is the sort position @@ -142,7 +141,6 @@ @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\ - Algebras.thy \ Complete_Lattice.thy \ Datatype.thy \ Extraction.thy \ @@ -385,7 +383,7 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \ Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy \ Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy \ - Library/Sum_Of_Squares/sos_wrapper.ML \ + Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML \ Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \ Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy \ Library/Infinite_Set.thy Library/FuncSet.thy \ @@ -591,9 +589,10 @@ $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \ + Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ - Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \ + Hoare/SchorrWaite.thy Hoare/Separation.thy \ Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib @$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare @@ -847,14 +846,6 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog -## HOL-W0 - -HOL-W0: HOL $(LOG)/HOL-W0.gz - -$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL W0 - - ## HOL-MicroJava HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz @@ -964,11 +955,12 @@ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \ ex/Codegenerator_Test.thy ex/Coherent.thy \ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ - ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ - ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Hilbert_Classical.thy ex/Induction_Schema.thy \ - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ - ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ + ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ + ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ + ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ + ex/Induction_Schema.thy ex/InductiveInvariant.thy \ + ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ @@ -1320,7 +1312,7 @@ $(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz \ $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ - $(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz \ + $(LOG)/HOL-Word-Examples.gz \ $(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \ $(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz \ $(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \ diff -r c6331256b087 -r f9801fdeb789 src/HOL/Isar_Examples/Group.thy --- a/src/HOL/Isar_Examples/Group.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Isar_Examples/Group.thy Tue Feb 23 14:44:43 2010 -0800 @@ -17,15 +17,12 @@ $\idt{times}$ is provided by the basic HOL theory. *} -consts - one :: "'a" - inverse :: "'a => 'a" +notation Groups.one ("one") -axclass - group < times - group_assoc: "(x * y) * z = x * (y * z)" - group_left_one: "one * x = x" - group_left_inverse: "inverse x * x = one" +class group = times + one + inverse + + assumes group_assoc: "(x * y) * z = x * (y * z)" + assumes group_left_one: "one * x = x" + assumes group_left_inverse: "inverse x * x = one" text {* The group axioms only state the properties of left one and inverse, @@ -144,10 +141,10 @@ \idt{one} :: \alpha)$ are defined like this. *} -axclass monoid < times - monoid_assoc: "(x * y) * z = x * (y * z)" - monoid_left_one: "one * x = x" - monoid_right_one: "x * one = x" +class monoid = times + one + + assumes monoid_assoc: "(x * y) * z = x * (y * z)" + assumes monoid_left_one: "one * x = x" + assumes monoid_right_one: "x * one = x" text {* Groups are \emph{not} yet monoids directly from the definition. For diff -r c6331256b087 -r f9801fdeb789 src/HOL/Lattice/Bounds.thy --- a/src/HOL/Lattice/Bounds.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Lattice/Bounds.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Bounds.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) diff -r c6331256b087 -r f9801fdeb789 src/HOL/Lattice/CompleteLattice.thy --- a/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/CompleteLattice.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -16,8 +15,8 @@ bounds (see \S\ref{sec:connect-bounds}). *} -axclass complete_lattice \ partial_order - ex_Inf: "\inf. is_Inf A inf" +class complete_lattice = + assumes ex_Inf: "\inf. is_Inf A inf" theorem ex_Sup: "\sup::'a::complete_lattice. is_Sup A sup" proof - diff -r c6331256b087 -r f9801fdeb789 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Lattice/Lattice.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Lattice.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -15,9 +14,9 @@ as well). *} -axclass lattice \ partial_order - ex_inf: "\inf. is_inf x y inf" - ex_sup: "\sup. is_sup x y sup" +class lattice = + assumes ex_inf: "\inf. is_inf x y inf" + assumes ex_sup: "\sup. is_sup x y sup" text {* The @{text \} (meet) and @{text \} (join) operations select such diff -r c6331256b087 -r f9801fdeb789 src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Tue Feb 23 14:44:24 2010 -0800 +++ b/src/HOL/Lattice/Orders.thy Tue Feb 23 14:44:43 2010 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Orders.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -18,21 +17,21 @@ required to be related (in either direction). *} -axclass leq < type -consts - leq :: "'a::leq \ 'a \ bool" (infixl "[=" 50) +class leq = + fixes leq :: "'a \ 'a \ bool" (infixl "[=" 50) + notation (xsymbols) leq (infixl "\" 50) -axclass quasi_order < leq - leq_refl [intro?]: "x \ x" - leq_trans [trans]: "x \ y \ y \ z \ x \ z" +class quasi_order = leq + + assumes leq_refl [intro?]: "x \ x" + assumes leq_trans [trans]: "x \ y \ y \ z \ x \ z" -axclass partial_order < quasi_order - leq_antisym [trans]: "x \ y \ y \ x \ x = y" +class partial_order = quasi_order + + assumes leq_antisym [trans]: "x \ y \ y \ x \ x = y" -axclass linear_order < partial_order - leq_linear: "x \ y \ y \ x" +class linear_order = partial_order + + assumes leq_linear: "x \ y \ y \ x" lemma linear_order_cases: "((x::'a::linear_order) \ y \ C) \ (y \ x \ C) \ C" @@ -54,11 +53,16 @@ primrec undual_dual: "undual (dual x) = x" -instance dual :: (leq) leq .. +instantiation dual :: (leq) leq +begin -defs (overloaded) +definition leq_dual_def: "x' \ y' \ undual y' \ undual x'" +instance .. + +end + lemma undual_leq [iff?]: "(undual x' \ undual y') = (y' \ x')" by (simp add: leq_dual_def) @@ -192,11 +196,16 @@ \emph{not} be linear in general. *} -instance * :: (leq, leq) leq .. +instantiation * :: (leq, leq) leq +begin -defs (overloaded) +definition leq_prod_def: "p \ q \ fst p \ fst q \ snd p \ snd q" +instance .. + +end + lemma leq_prodI [intro?]: "fst p \ fst q \ snd p \ snd q \ p \ q" by (unfold leq_prod_def) blast @@ -249,11 +258,16 @@ orders need \emph{not} be linear in general. *} -instance "fun" :: (type, leq) leq .. +instantiation "fun" :: (type, leq) leq +begin -defs (overloaded) +definition leq_fun_def: "f \

Type Inference for MiniML (without let)

Type Inference for MiniML (without `let`)