# HG changeset patch # User haftmann # Date 1253528661 -7200 # Node ID 58b561b415a2b9bfb000b59187685eb89c7247ad # Parent f270520df7dee22297115fb9be109c2b4ee199a5# Parent 27530efec97a48b87db306c3ae3cf29daa3c7435 merged diff -r 27530efec97a -r 58b561b415a2 src/HOL/IsaMakefile --- 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 \ diff -r 27530efec97a -r 58b561b415a2 src/HOL/SMT/Examples/SMT_Examples.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 (\x. x mod 2) xs) mod 2 = l mod 2 \ eval_dioph ks (map (\x. x div 2) xs) = (l - eval_dioph ks (map (\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]) diff -r 27530efec97a -r 58b561b415a2 src/HOL/SMT/Tools/smt_solver.ML --- 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 diff -r 27530efec97a -r 58b561b415a2 src/HOL/SMT/lib/scripts/remote_smt.pl --- 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 diff -r 27530efec97a -r 58b561b415a2 src/HOL/UNITY/ROOT.ML --- 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"; diff -r 27530efec97a -r 58b561b415a2 src/HOL/UNITY/UNITY_Examples.thy --- /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