src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 45970 b6d0cff57d96
parent 43913 003f8c5f3e37
child 52666 391913d17d15
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  theory Context_Free_Grammar_Example
     1.5  imports "~~/src/HOL/Library/Code_Prolog"
     1.6  begin
     1.7 -
     1.8 +(*
     1.9  declare mem_def[code_pred_inline]
    1.10 -
    1.11 +*)
    1.12  
    1.13  subsection {* Alternative rules for length *}
    1.14  
    1.15 @@ -32,7 +32,7 @@
    1.16  | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    1.17  
    1.18  lemma
    1.19 -  "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
    1.20 +  "S\<^isub>1p w \<Longrightarrow> w = []"
    1.21  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.22  oops
    1.23  
    1.24 @@ -60,13 +60,13 @@
    1.25    {ensure_groundness = true,
    1.26    limit_globally = NONE,
    1.27    limited_types = [],
    1.28 -  limited_predicates = [(["s1", "a1", "b1"], 2)],
    1.29 -  replacing = [(("s1", "limited_s1"), "quickcheck")],
    1.30 +  limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
    1.31 +  replacing = [(("s1p", "limited_s1p"), "quickcheck")],
    1.32    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.33  
    1.34  
    1.35  theorem S\<^isub>1_sound:
    1.36 -"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.37 +"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.38  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.39  oops
    1.40  
    1.41 @@ -84,13 +84,13 @@
    1.42    {ensure_groundness = true,
    1.43    limit_globally = NONE,
    1.44    limited_types = [],
    1.45 -  limited_predicates = [(["s2", "a2", "b2"], 3)],
    1.46 -  replacing = [(("s2", "limited_s2"), "quickcheck")],
    1.47 +  limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
    1.48 +  replacing = [(("s2p", "limited_s2p"), "quickcheck")],
    1.49    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.50  
    1.51  
    1.52  theorem S\<^isub>2_sound:
    1.53 -"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.54 +  "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.55  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.56  oops
    1.57  
    1.58 @@ -107,12 +107,12 @@
    1.59    {ensure_groundness = true,
    1.60    limit_globally = NONE,
    1.61    limited_types = [],
    1.62 -  limited_predicates = [(["s3", "a3", "b3"], 6)],
    1.63 -  replacing = [(("s3", "limited_s3"), "quickcheck")],
    1.64 +  limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
    1.65 +  replacing = [(("s3p", "limited_s3p"), "quickcheck")],
    1.66    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.67  
    1.68  lemma S\<^isub>3_sound:
    1.69 -"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.70 +  "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.71  quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
    1.72  oops
    1.73  
    1.74 @@ -149,13 +149,13 @@
    1.75    {ensure_groundness = true,
    1.76    limit_globally = NONE,
    1.77    limited_types = [],
    1.78 -  limited_predicates = [(["s4", "a4", "b4"], 6)],
    1.79 -  replacing = [(("s4", "limited_s4"), "quickcheck")],
    1.80 +  limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
    1.81 +  replacing = [(("s4p", "limited_s4p"), "quickcheck")],
    1.82    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.83  
    1.84  
    1.85  theorem S\<^isub>4_sound:
    1.86 -"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.87 +  "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.88  quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
    1.89  oops
    1.90