# HG changeset patch
# User bulwahn
# Date 1284637754 -7200
# Node ID 139c694299f64929166a5e68333b8d28684b5045
# Parent  f3c5da707f3089de046f3a2b735351a4509a24b7
adding another context free grammar example for the predicate compiler

diff -r f3c5da707f30 -r 139c694299f6 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 13:49:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 13:49:14 2010 +0200
@@ -1310,6 +1310,10 @@
 values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
 values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
 
+text {* Redeclaring append.equation as code equation *}
+
+declare appendP.equation[code]
+
 subsection {* Function with tuples *}
 
 fun append'
@@ -1580,6 +1584,56 @@
 
 thm big_step.equation
 
+section {* General Context Free Grammars *}
+text {* a contribution by Aditi Barthwal *}
+
+datatype ('nts,'ts) symbol = NTS 'nts
+                            | TS 'ts
+
+                            
+datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
+
+types ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
+
+fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
+where
+  "rules (r, s) = r"
+
+definition derives 
+where
+"derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. 
+                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
+                         (s1 @ rhs @ s2) = rsl \<and>
+                         (rule lhs rhs) \<in> fst g }"
+
+abbreviation "example_grammar == 
+({ rule ''S'' [NTS ''A'', NTS ''B''],
+   rule ''S'' [TS ''a''],
+  rule ''A'' [TS ''b'']}, ''S'')"
+
+
+code_pred [inductify,skip_proof] derives .
+
+thm derives.equation
+
+definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
+
+code_pred (modes: o \<Rightarrow> bool) [inductify, show_modes, show_intermediate_results, skip_proof] test .
+thm test.equation
+
+values "{rhs. test rhs}"
+
+declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
+
+code_pred [inductify] rtrancl .
+
+definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^*  }"
+
+code_pred [inductify, skip_proof] test2 .
+
+values "{rhs. test2 rhs}"
+
+
 section {* Examples for detecting switches *}
 
 inductive detect_switches1 where