# 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). \s1 s2 lhs rhs. + (s1 @ [NTS lhs] @ s2 = lsl) \ + (s1 @ rhs @ s2) = rsl \ + (rule lhs rhs) \ 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 \ 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) \ (derives example_grammar)^* }" + +code_pred [inductify, skip_proof] test2 . + +values "{rhs. test2 rhs}" + + section {* Examples for detecting switches *} inductive detect_switches1 where