author  haftmann 
Tue, 12 May 2009 21:17:47 +0200  
changeset 31129  d2cead76fca2 
parent 31123  src/HOL/ex/Predicate_Compile.thy@e3b4e52c01c2 
child 31195  12741f23527d 
permissions  rwrr 
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset

1 
theory Predicate_Compile_ex 
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
31123
diff
changeset

2 
imports Complex_Main Predicate_Compile 
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset

3 
begin 
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset

4 

30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

5 
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

6 
"even 0" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

7 
 "even n \<Longrightarrow> odd (Suc n)" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

8 
 "odd n \<Longrightarrow> even (Suc n)" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

9 

31123  10 
code_pred even 
11 
using assms by (rule even.cases) 

12 

13 
thm even.equation 

30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

14 

5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

15 

5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

16 
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

17 
append_Nil: "append [] xs xs" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

18 
 append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

19 

31123  20 
code_pred append 
21 
using assms by (rule append.cases) 

22 

23 
thm append.equation 

30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

24 

5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

25 

5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

26 
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

27 
for f where 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

28 
"partition f [] [] []" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

29 
 "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

30 
 "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)" 
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

31 

31123  32 
code_pred partition 
33 
using assms by (rule partition.cases) 

34 

35 
thm partition.equation 

36 

30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30953
diff
changeset

37 

31123  38 
code_pred tranclp 
39 
using assms by (rule tranclp.cases) 

40 

41 
thm tranclp.equation 

42 

30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset

43 
end 