--- a/src/HOL/IsaMakefile Mon Sep 21 12:23:52 2009 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 21 12:24:21 2009 +0200
@@ -643,7 +643,7 @@
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
- UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \
+ UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \
UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Mon Sep 21 12:23:52 2009 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Mon Sep 21 12:24:21 2009 +0200
@@ -9,7 +9,7 @@
begin
declare [[smt_solver=z3, z3_proofs=false]]
-declare [[smt_trace=true]] (*FIXME*)
+declare [[smt_trace=false]]
section {* Propositional and first-order logic *}
@@ -163,6 +163,7 @@
(eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
eval_dioph ks (map (\<lambda>x. x div 2) xs) =
(l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
+ using [[smt_solver=z3]]
by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
--- a/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 12:23:52 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Mon Sep 21 12:24:21 2009 +0200
@@ -121,7 +121,7 @@
fun cmd f1 f2 =
if path <> ""
then map qq (path :: args) @ [qf f1, ">", qf f2]
- else map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
+ else "perl -w" :: map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
end
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl Mon Sep 21 12:23:52 2009 +0200
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl Mon Sep 21 12:24:21 2009 +0200
@@ -1,4 +1,3 @@
-#!/usr/bin/env perl -w
#
# Script to invoke remote SMT solvers.
# Author: Sascha Boehme, TU Muenchen
--- a/src/HOL/UNITY/ROOT.ML Mon Sep 21 12:23:52 2009 +0200
+++ b/src/HOL/UNITY/ROOT.ML Mon Sep 21 12:24:21 2009 +0200
@@ -1,50 +1,13 @@
-(* Title: HOL/UNITY/ROOT
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Root file for UNITY proofs.
*)
(*Verifying security protocols using UNITY*)
no_document use_thy "../Auth/Public";
-use_thys [
- (*Basic meta-theory*)
- "UNITY_Main",
-
- (*Simple examples: no composition*)
- "Simple/Deadlock",
- "Simple/Common",
- "Simple/Network",
- "Simple/Token",
- "Simple/Channel",
- "Simple/Lift",
- "Simple/Mutex",
- "Simple/Reach",
- "Simple/Reachability",
-
- (*Verifying security protocols using UNITY*)
- "Simple/NSP_Bad",
+(*Basic meta-theory*)
+use_thy "UNITY_Main";
- (*Example of composition*)
- "Comp/Handshake",
-
- (*Universal properties examples*)
- "Comp/Counter",
- "Comp/Counterc",
- "Comp/Priority",
-
- "Comp/TimerArray",
- "Comp/Progress",
-
- (*obsolete*)
- "ELT"
-];
-
-(*Allocator example*)
-(* FIXME some parts no longer work -- had been commented out for a long time *)
-setmp_noncritical quick_and_dirty true
- use_thy "Comp/Alloc";
-
-use_thys ["Comp/AllocImpl", "Comp/Client"];
+(*Examples*)
+use_thy "UNITY_Examples";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_Examples.thy Mon Sep 21 12:24:21 2009 +0200
@@ -0,0 +1,45 @@
+(* Author: Lawrence C Paulson Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+*)
+
+header {* Various examples for UNITY *}
+
+theory UNITY_Examples
+imports
+ UNITY_Main
+
+ (*Simple examples: no composition*)
+ "Simple/Deadlock"
+ "Simple/Common"
+ "Simple/Network"
+ "Simple/Token"
+ "Simple/Channel"
+ "Simple/Lift"
+ "Simple/Mutex"
+ "Simple/Reach"
+ "Simple/Reachability"
+
+ (*Verifying security protocols using UNITY*)
+ "Simple/NSP_Bad"
+
+ (*Example of composition*)
+ "Comp/Handshake"
+
+ (*Universal properties examples*)
+ "Comp/Counter"
+ "Comp/Counterc"
+ "Comp/Priority"
+
+ "Comp/TimerArray"
+ "Comp/Progress"
+
+ "Comp/Alloc"
+ "Comp/AllocImpl"
+ "Comp/Client"
+
+ (*obsolete*)
+ "ELT"
+
+begin
+
+end