# HG changeset patch
# User bulwahn
# Date 1283853113 -7200
# Node ID 475856793715a6a9a9c705bc5621f01d182f0ea9
# Parent  c035d01a7e77debb4c576be07c12cf72f5bb8d40
adding IMP quickcheck examples

diff -r c035d01a7e77 -r 475856793715 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
@@ -1327,6 +1327,10 @@
   Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
   Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 		\
   Predicate_Compile_Examples/Hotel_Example.thy 				\
+  Predicate_Compile_Examples/IMP_1.thy 					\
+  Predicate_Compile_Examples/IMP_2.thy 					\
+  Predicate_Compile_Examples/IMP_3.thy 					\
+  Predicate_Compile_Examples/IMP_4.thy 					\
   Predicate_Compile_Examples/Lambda_Example.thy 			\
   Predicate_Compile_Examples/List_Examples.thy 
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
diff -r c035d01a7e77 -r 475856793715 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,34 @@
+theory IMP_1
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+  In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
+*}
+
+types
+  var = unit
+  state = bool
+
+datatype com =
+  Skip |
+  Ass bool |
+  Seq com com |
+  IF com com
+
+inductive exec :: "com => state => state => bool" where
+  "exec Skip s s" |
+  "exec (Ass e) s e" |
+  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+  "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
+  "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t"
+
+lemma
+  "exec c s s' ==> exec (Seq c c) s s'"
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1, expect = counterexample]
+oops
+
+
+end
diff -r c035d01a7e77 -r 475856793715 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_2
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+  In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
+*}
+
+types
+  var = unit
+  state = bool
+
+datatype com =
+  Skip |
+  Ass bool |
+  Seq com com |
+  IF com com |
+  While com
+
+inductive exec :: "com => state => state => bool" where
+  "exec Skip s s" |
+  "exec (Ass e) s e" |
+  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+  "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
+  "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
+  "\<not> s ==> exec (While c) s s" |
+  "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''"
+
+lemma
+  "exec c s s' ==> exec (Seq c c) s s'"
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1]
+oops
+
+
+end
diff -r c035d01a7e77 -r 475856793715 src/HOL/Predicate_Compile_Examples/IMP_3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_3
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+  In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
+*}
+
+types
+  var = unit
+  state = int
+
+datatype com =
+  Skip |
+  Ass var "int" |
+  Seq com com |
+  IF "state list" com com |
+  While "state list" com
+
+inductive exec :: "com => state => state => bool" where
+  "exec Skip s s" |
+  "exec (Ass x e) s e" |
+  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+  "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+  "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+  "s \<notin> set b ==> exec (While b c) s s" |
+  "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+lemma
+  "exec c s s' ==> exec (Seq c c) s s'"
+  quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=3, quiet = false, expect = counterexample]
+oops
+
+
+end
\ No newline at end of file
diff -r c035d01a7e77 -r 475856793715 src/HOL/Predicate_Compile_Examples/IMP_4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_4
+imports Predicate_Compile_Quickcheck
+begin
+
+subsection {* IMP *}
+
+text {*
+  In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
+*}
+
+types
+  var = nat
+  state = "int list"
+
+datatype com =
+  Skip |
+  Ass var "int" |
+  Seq com com |
+  IF "state list" com com |
+  While "state list" com
+
+inductive exec :: "com => state => state => bool" where
+  "exec Skip s s" |
+  "exec (Ass x e) s (s[x := e])" |
+  "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+  "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+  "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+  "s \<notin> set b ==> exec (While b c) s s" |
+  "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+lemma
+  "exec c s s' ==> exec (Seq c c) s s'"
+  nitpick (* nitpick fails here! *)
+  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+oops
+
+end
\ No newline at end of file
diff -r c035d01a7e77 -r 475856793715 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
@@ -1,2 +1,2 @@
-use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
+use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
 if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"];