src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 53015 a1119cf551e8
parent 52666 391913d17d15
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -26,16 +26,16 @@
     1.4  
     1.5  datatype alphabet = a | b
     1.6  
     1.7 -inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
     1.8 -  "[] \<in> S\<^isub>1"
     1.9 -| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    1.10 -| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
    1.11 -| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
    1.12 -| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    1.13 -| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    1.14 +inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
    1.15 +  "[] \<in> S\<^sub>1"
    1.16 +| "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    1.17 +| "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
    1.18 +| "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
    1.19 +| "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    1.20 +| "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
    1.21  
    1.22  lemma
    1.23 -  "S\<^isub>1p w \<Longrightarrow> w = []"
    1.24 +  "S\<^sub>1p w \<Longrightarrow> w = []"
    1.25  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.26  oops
    1.27  
    1.28 @@ -68,19 +68,19 @@
    1.29    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.30  
    1.31  
    1.32 -theorem S\<^isub>1_sound:
    1.33 -"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.34 +theorem S\<^sub>1_sound:
    1.35 +"S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.36  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.37  oops
    1.38  
    1.39  
    1.40 -inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
    1.41 -  "[] \<in> S\<^isub>2"
    1.42 -| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
    1.43 -| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
    1.44 -| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
    1.45 -| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
    1.46 -| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    1.47 +inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
    1.48 +  "[] \<in> S\<^sub>2"
    1.49 +| "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
    1.50 +| "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
    1.51 +| "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
    1.52 +| "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
    1.53 +| "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
    1.54  
    1.55  
    1.56  setup {* Code_Prolog.map_code_options (K
    1.57 @@ -92,18 +92,18 @@
    1.58    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.59  
    1.60  
    1.61 -theorem S\<^isub>2_sound:
    1.62 -  "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.63 +theorem S\<^sub>2_sound:
    1.64 +  "S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.65  quickcheck[tester = prolog, iterations=1, expect = counterexample]
    1.66  oops
    1.67  
    1.68 -inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
    1.69 -  "[] \<in> S\<^isub>3"
    1.70 -| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
    1.71 -| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
    1.72 -| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
    1.73 -| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
    1.74 -| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
    1.75 +inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
    1.76 +  "[] \<in> S\<^sub>3"
    1.77 +| "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
    1.78 +| "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
    1.79 +| "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
    1.80 +| "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
    1.81 +| "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
    1.82  
    1.83  
    1.84  setup {* Code_Prolog.map_code_options (K
    1.85 @@ -114,8 +114,8 @@
    1.86    replacing = [(("s3p", "limited_s3p"), "quickcheck")],
    1.87    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    1.88  
    1.89 -lemma S\<^isub>3_sound:
    1.90 -  "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.91 +lemma S\<^sub>3_sound:
    1.92 +  "S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.93  quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
    1.94  oops
    1.95  
    1.96 @@ -132,20 +132,20 @@
    1.97    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.98  
    1.99  
   1.100 -theorem S\<^isub>3_complete:
   1.101 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   1.102 +theorem S\<^sub>3_complete:
   1.103 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
   1.104  quickcheck[tester = prolog, size=1, iterations=1]
   1.105  oops
   1.106  *)
   1.107  
   1.108 -inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   1.109 -  "[] \<in> S\<^isub>4"
   1.110 -| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   1.111 -| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   1.112 -| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   1.113 -| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   1.114 -| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   1.115 -| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   1.116 +inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
   1.117 +  "[] \<in> S\<^sub>4"
   1.118 +| "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
   1.119 +| "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
   1.120 +| "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
   1.121 +| "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
   1.122 +| "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
   1.123 +| "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   1.124  
   1.125  
   1.126  setup {* Code_Prolog.map_code_options (K
   1.127 @@ -157,14 +157,14 @@
   1.128    manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   1.129  
   1.130  
   1.131 -theorem S\<^isub>4_sound:
   1.132 -  "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   1.133 +theorem S\<^sub>4_sound:
   1.134 +  "S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   1.135  quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
   1.136  oops
   1.137  
   1.138  (*
   1.139 -theorem S\<^isub>4_complete:
   1.140 -"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   1.141 +theorem S\<^sub>4_complete:
   1.142 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
   1.143  oops
   1.144  *)
   1.145