82 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
82 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
83 | "nullable (STAR r) = True" |
83 | "nullable (STAR r) = True" |
84 |
84 |
85 |
85 |
86 section \<open>Correctness Proof for Nullable\<close> |
86 section \<open>Correctness Proof for Nullable\<close> |
87 |
|
88 lemma nullable_correctness: |
|
89 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
90 apply(induct r) |
|
91 (* ZERO case *) |
|
92 apply(simp only: nullable.simps) |
|
93 apply(simp only: L.simps) |
|
94 apply(simp) |
|
95 (* ONE case *) |
|
96 apply(simp only: nullable.simps) |
|
97 apply(simp only: L.simps) |
|
98 apply(simp) |
|
99 (* CHAR case *) |
|
100 apply(simp only: nullable.simps) |
|
101 apply(simp only: L.simps) |
|
102 apply(simp) |
|
103 prefer 2 |
|
104 (* ALT case *) |
|
105 apply(simp (no_asm) only: nullable.simps) |
|
106 apply(simp only:) |
|
107 apply(simp only: L.simps) |
|
108 apply(simp) |
|
109 (* SEQ case *) |
|
110 apply(simp only: L.simps) |
|
111 apply(simp) |
|
112 oops |
|
113 |
|
114 lemma nullable_correctness: |
|
115 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
116 apply(induct r) |
|
117 apply(simp_all) |
|
118 (* all easy subgoals are proved except the last 2 *) |
|
119 (* where the definition of Seq needs to be unfolded. *) |
|
120 oops |
|
121 |
|
122 lemma nullable_correctness: |
|
123 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
124 apply(induct r) |
|
125 apply(simp_all add: Seq_def) |
|
126 (* except the star case every thing is proved *) |
|
127 (* we need to use the rule for Star.start *) |
|
128 oops |
|
129 |
87 |
130 lemma nullable_correctness: |
88 lemma nullable_correctness: |
131 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
89 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
132 apply(induct r) |
90 apply(induct r) |
133 apply(simp_all add: Seq_def Star.start) |
91 apply(simp_all add: Seq_def Star.start) |