27 "derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. |
27 "derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. |
28 (s1 @ [NTS lhs] @ s2 = lsl) \<and> |
28 (s1 @ [NTS lhs] @ s2 = lsl) \<and> |
29 (s1 @ rhs @ s2) = rsl \<and> |
29 (s1 @ rhs @ s2) = rsl \<and> |
30 (rule lhs rhs) \<in> fst g }" |
30 (rule lhs rhs) \<in> fst g }" |
31 |
31 |
|
32 definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool" |
|
33 where |
|
34 "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))" |
|
35 |
|
36 lemma [code_pred_def]: |
|
37 "derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs. |
|
38 (s1 @ [NTS lhs] @ s2 = lsl) \<and> |
|
39 (s1 @ rhs @ s2) = rsl \<and> |
|
40 (fst g) (rule lhs rhs))" |
|
41 unfolding derivesp_def derives_def by auto |
|
42 |
32 abbreviation "example_grammar == |
43 abbreviation "example_grammar == |
33 ({ rule ''S'' [NTS ''A'', NTS ''B''], |
44 ({ rule ''S'' [NTS ''A'', NTS ''B''], |
34 rule ''S'' [TS ''a''], |
45 rule ''S'' [TS ''a''], |
35 rule ''A'' [TS ''b'']}, ''S'')" |
46 rule ''A'' [TS ''b'']}, ''S'')" |
36 |
47 |
37 |
48 definition "example_rules == |
38 code_pred [inductify, skip_proof] derives . |
49 (%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or> |
39 |
50 x = rule ''S'' [TS ''a''] \<or> |
40 thm derives.equation |
51 x = rule ''A'' [TS ''b''])" |
41 |
52 |
42 definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }" |
53 |
43 |
54 code_pred [inductify, skip_proof] derivesp . |
44 code_pred (modes: o \<Rightarrow> bool) [inductify] test . |
55 |
45 thm test.equation |
56 thm derivesp.equation |
46 |
57 |
47 values "{rhs. test rhs}" |
58 definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)" |
48 |
59 |
49 declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def] |
60 code_pred (modes: o \<Rightarrow> bool) [inductify] testp . |
50 |
61 thm testp.equation |
51 code_pred [inductify] rtrancl . |
62 |
52 |
63 values "{rhs. testp rhs}" |
53 definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^* }" |
64 |
|
65 declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def] |
|
66 |
|
67 code_pred [inductify] rtranclp . |
|
68 |
|
69 definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)" |
54 |
70 |
55 code_pred [inductify, skip_proof] test2 . |
71 code_pred [inductify, skip_proof] test2 . |
56 |
72 |
57 values "{rhs. test2 rhs}" |
73 values "{rhs. test2 rhs}" |
58 |
74 |