src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy

 theory Predicate_Compile_Quickcheck_ex
 imports Predicate_Compile_Quickcheck
-  Predicate_Compile_Alternative_Defs
 begin
 
-ML {* Predicate_Compile_Alternative_Defs.get *}
-
 section {* Sets *}
-(*
+
 lemma "x \<in> {(1::nat)} ==> False"
-quickcheck[generator=predicate_compile, iterations=10]
-oops
-*)
-(* TODO: some error with doubled negation *)
-(*
+quickcheck[generator=predicate_compile_wo_ff, iterations=10]
+oops
+
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
-quickcheck[generator=predicate_compile]
-oops
-*)
-(*
+quickcheck[generator=predicate_compile_wo_ff]
+oops
+
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
-quickcheck[generator=predicate_compile]
-oops
-*) 
+quickcheck[generator=predicate_compile_wo_ff]
+oops
+ 
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
 oops
 
 section {* Numerals *}
-(*
+
 lemma
   "x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
-quickcheck[generator=predicate_compile]
-oops
-*)
+quickcheck[generator=predicate_compile_wo_ff]
+oops
+
 lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
 oops
 
 lemma
   "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
-(*quickcheck[generator=predicate_compile]*)
+quickcheck[generator=predicate_compile_wo_ff]
 oops
 
 section {* Context Free Grammar *}
 
 datatype alphabet = a | b

 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
-(*
-code_pred [random_dseq inductify] "S\<^isub>1p" .
-*)
-(*thm B\<^isub>1p.random_dseq_equation*)
-(*
-values [random_dseq 2, 2, 4] 10 "{x. S\<^isub>1p x}"
-values [random_dseq 1, 1, 5] 20 "{x. S\<^isub>1p x}"
-
-ML {* set ML_Context.trace *}
-*)
-ML {* set Toplevel.debug *}
-(*
-quickcheck[generator = predicate_compile, size = 10, iterations = 1]
-oops
-*)
-ML {* Spec_Rules.get *}
-ML {* Item_Net.retrieve *}
-local_setup {* Local_Theory.checkpoint *}
-ML {* Predicate_Compile_Data.get_specification @{theory} @{term "append"} *}
-lemma
-  "w \<in> S\<^isub>1p \<Longrightarrow> w = []"
-quickcheck[generator = predicate_compile, iterations=1]
+
+lemma
+  "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
+quickcheck[generator = predicate_compile_ff_nofs, iterations=1]
 oops
 
 theorem S\<^isub>1_sound:
-"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=15]
+"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=predicate_compile_ff_nofs, size=15]
 oops
 
 
 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   "[] \<in> S\<^isub>2"
 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
-
+(*
 code_pred [random_dseq inductify] S\<^isub>2 .
 thm S\<^isub>2.random_dseq_equation
 thm A\<^isub>2.random_dseq_equation
 thm B\<^isub>2.random_dseq_equation
 

 
 lemma
 "w \<in> S\<^isub>2 ==> length [x \<leftarrow> w. x = a] <= Suc (Suc 0)"
 quickcheck[generator=predicate_compile, size = 10, iterations = 1]
 oops
-
+*)
 theorem S\<^isub>2_sound:
 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=15, iterations=1]
+quickcheck[generator=predicate_compile_ff_nofs, size=5, iterations=10]
 oops
 
 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   "[] \<in> S\<^isub>3"
 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"

 *)
 
 
 lemma S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=predicate_compile, size=10, iterations=10]
+quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=10]
 oops
 
 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = predicate_compile]
+quickcheck[size=10, generator = predicate_compile_ff_fs]
 oops
 
 theorem S\<^isub>3_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
 (*quickcheck[generator=SML]*)
-quickcheck[generator=predicate_compile, size=10, iterations=100]
+quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=100]
 oops
 
 
 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   "[] \<in> S\<^isub>4"

 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = predicate_compile, size=5, iterations=1]
+quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
 oops
 
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = predicate_compile, size=5, iterations=1]
-oops
-
-hide const b
+quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+oops
+
+hide const a b
 
 subsection {* Lexicographic order *}
+(* TODO *)
+(*
 lemma
   "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r"
-
+oops
+*)
 subsection {* IMP *}
 
 types
   var = nat
   state = "int list"

 
 values [random_dseq 1, 2, 3] 10 "{(c, s, s'). exec c s s'}"
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile, size=3, iterations=1]
+(*quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10]*)
 oops
 
 subsection {* Lambda *}
 
 datatype type =

   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
 
 lemma
   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = predicate_compile, size = 7, iterations = 10]
-oops
-
-(*
-code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
-thm typing.equation
-
-code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
-thm beta.equation
-
-values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
-
-definition "reduce t = Predicate.the (reduce' t)"
-
-value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
-
-code_pred [random] typing .
-code_pred [random_dseq] typing .
-
-(*values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
-*)*)
+quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10]
+oops
 
 subsection {* JAD *}
 
 definition matrix :: "('a :: semiring_0) list list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "matrix M rs cs \<longleftrightarrow> (\<forall> row \<in> set M. length row = cs) \<and> length M = rs"

 values [random_dseq 3, 2] 10 "{(M, rs, cs). matrix (M:: int list list) rs cs}"
 *)
 lemma [code_pred_intro]:
   "matrix [] 0 m"
   "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
-sorry
-
-code_pred [random_dseq inductify] matrix sorry
+proof -
+  show "matrix [] 0 m" unfolding matrix_def by auto
+next
+  show "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
+    unfolding matrix_def by auto
+qed
+
+code_pred [random_dseq inductify] matrix
+  apply (cases x)
+  unfolding matrix_def apply fastsimp
+  apply fastsimp done
 
 
 values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}"
 
 definition "scalar_product v w = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)"

   "sort f [] = []" |
   "sort f (x # xs) = insert f x (sort f xs)"
 
 definition
   "length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)"
-
+(*
 definition
   "transpose M = [map (\<lambda> xs. xs ! i) (takeWhile (\<lambda> xs. i < length xs) M). i \<leftarrow> [0 ..< length (M ! 0)]]"
-
+*)
 definition
   "inflate upds = foldr (\<lambda> (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)"
 
 definition
   "jad = apsnd transpose o length_permutate o map sparsify"
 
 definition
   "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
-ML {* ML_Context.trace := false *}
 
 lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
-quickcheck[generator = predicate_compile, size = 6]
+quickcheck[generator = predicate_compile_ff_nofs, size = 6]
 oops
 
 lemma
   "\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v"
-(*quickcheck[generator = predicate_compile]*)
+quickcheck[generator = predicate_compile_wo_ff]
 oops
 
 end