src/HOL/Predicate_Compile_Examples/Examples.thy
changeset 45970 b6d0cff57d96
parent 42463 f270e3e18be5
child 51144 0ede9e2266a8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -29,28 +29,44 @@
     1.4                           (s1 @ rhs @ s2) = rsl \<and>
     1.5                           (rule lhs rhs) \<in> fst g }"
     1.6  
     1.7 +definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
     1.8 +where
     1.9 +  "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
    1.10 + 
    1.11 +lemma [code_pred_def]:
    1.12 +  "derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs. 
    1.13 +                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
    1.14 +                         (s1 @ rhs @ s2) = rsl \<and>
    1.15 +                         (fst g) (rule lhs rhs))"
    1.16 +unfolding derivesp_def derives_def by auto
    1.17 +
    1.18  abbreviation "example_grammar == 
    1.19  ({ rule ''S'' [NTS ''A'', NTS ''B''],
    1.20     rule ''S'' [TS ''a''],
    1.21    rule ''A'' [TS ''b'']}, ''S'')"
    1.22  
    1.23 -
    1.24 -code_pred [inductify, skip_proof] derives .
    1.25 +definition "example_rules == 
    1.26 +(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or>
    1.27 +   x = rule ''S'' [TS ''a''] \<or>
    1.28 +  x = rule ''A'' [TS ''b''])"
    1.29  
    1.30 -thm derives.equation
    1.31  
    1.32 -definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }"
    1.33 +code_pred [inductify, skip_proof] derivesp .
    1.34 +
    1.35 +thm derivesp.equation
    1.36  
    1.37 -code_pred (modes: o \<Rightarrow> bool) [inductify] test .
    1.38 -thm test.equation
    1.39 +definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)"
    1.40  
    1.41 -values "{rhs. test rhs}"
    1.42 +code_pred (modes: o \<Rightarrow> bool) [inductify] testp .
    1.43 +thm testp.equation
    1.44  
    1.45 -declare rtrancl.intros(1)[code_pred_def] converse_rtrancl_into_rtrancl[code_pred_def]
    1.46 +values "{rhs. testp rhs}"
    1.47 +
    1.48 +declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def]
    1.49  
    1.50 -code_pred [inductify] rtrancl .
    1.51 +code_pred [inductify] rtranclp .
    1.52  
    1.53 -definition "test2 = { rhs. ([NTS ''S''],rhs) \<in> (derives example_grammar)^*  }"
    1.54 +definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)"
    1.55  
    1.56  code_pred [inductify, skip_proof] test2 .
    1.57