split Predicate_Compile examples into separate theory
authorhaftmann
Tue May 12 21:17:47 2009 +0200 (2009-05-12)
changeset 31129d2cead76fca2
parent 31128 b3bb28c87409
child 31130 94cb206f8f6a
split Predicate_Compile examples into separate theory
src/HOL/IsaMakefile
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/Predicate_Compile_ex.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue May 12 21:17:38 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 12 21:17:47 2009 +0200
     1.3 @@ -854,7 +854,7 @@
     1.4    ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
     1.5    ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
     1.6    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
     1.7 -  ex/Predicate_Compile.thy ex/predicate_compile.ML
     1.8 +  ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
     1.9  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    1.10  
    1.11  
     2.1 --- a/src/HOL/ex/Predicate_Compile.thy	Tue May 12 21:17:38 2009 +0200
     2.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Tue May 12 21:17:47 2009 +0200
     2.3 @@ -46,51 +46,4 @@
     2.4  end;
     2.5  *}
     2.6  
     2.7 -
     2.8 -text {* Example(s) *}
     2.9 -
    2.10 -inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
    2.11 -    "even 0"
    2.12 -  | "even n \<Longrightarrow> odd (Suc n)"
    2.13 -  | "odd n \<Longrightarrow> even (Suc n)"
    2.14 -
    2.15 -code_pred even
    2.16 -  using assms by (rule even.cases)
    2.17 -
    2.18 -thm even.equation
    2.19 -
    2.20 -
    2.21 -inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    2.22 -    append_Nil: "append [] xs xs"
    2.23 -  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    2.24 -
    2.25 -code_pred append
    2.26 -  using assms by (rule append.cases)
    2.27 -
    2.28 -thm append.equation
    2.29 -
    2.30 -
    2.31 -inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.32 -  for f where
    2.33 -    "partition f [] [] []"
    2.34 -  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
    2.35 -  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
    2.36 -
    2.37 -code_pred partition
    2.38 -  using assms by (rule partition.cases)
    2.39 -
    2.40 -thm partition.equation
    2.41 -
    2.42 -
    2.43 -code_pred tranclp
    2.44 -  using assms by (rule tranclp.cases)
    2.45 -
    2.46 -thm tranclp.equation
    2.47 -
    2.48 -
    2.49 -ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *}
    2.50 -ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *}
    2.51 -
    2.52 -ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
    2.53 -
    2.54  end
    2.55 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue May 12 21:17:47 2009 +0200
     3.3 @@ -0,0 +1,43 @@
     3.4 +theory Predicate_Compile_ex
     3.5 +imports Complex_Main Predicate_Compile
     3.6 +begin
     3.7 +
     3.8 +inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
     3.9 +    "even 0"
    3.10 +  | "even n \<Longrightarrow> odd (Suc n)"
    3.11 +  | "odd n \<Longrightarrow> even (Suc n)"
    3.12 +
    3.13 +code_pred even
    3.14 +  using assms by (rule even.cases)
    3.15 +
    3.16 +thm even.equation
    3.17 +
    3.18 +
    3.19 +inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    3.20 +    append_Nil: "append [] xs xs"
    3.21 +  | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    3.22 +
    3.23 +code_pred append
    3.24 +  using assms by (rule append.cases)
    3.25 +
    3.26 +thm append.equation
    3.27 +
    3.28 +
    3.29 +inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    3.30 +  for f where
    3.31 +    "partition f [] [] []"
    3.32 +  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
    3.33 +  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
    3.34 +
    3.35 +code_pred partition
    3.36 +  using assms by (rule partition.cases)
    3.37 +
    3.38 +thm partition.equation
    3.39 +
    3.40 +
    3.41 +code_pred tranclp
    3.42 +  using assms by (rule tranclp.cases)
    3.43 +
    3.44 +thm tranclp.equation
    3.45 +
    3.46 +end
    3.47 \ No newline at end of file
     4.1 --- a/src/HOL/ex/ROOT.ML	Tue May 12 21:17:38 2009 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Tue May 12 21:17:47 2009 +0200
     4.3 @@ -16,7 +16,8 @@
     4.4    "Codegenerator_Pretty",
     4.5    "NormalForm",
     4.6    "../NumberTheory/Factorization",
     4.7 -  "Predicate_Compile"
     4.8 +  "Predicate_Compile",
     4.9 +  "Predicate_Compile_ex"
    4.10  ];
    4.11  
    4.12  use_thys [