moved recfun_codegen.ML to Code_Generator.thy
authorhaftmann
Wed May 09 07:53:06 2007 +0200 (2007-05-09)
changeset 22886cdff6ef76009
parent 22885 ebde66a71ab0
child 22887 2a3e9c7b894c
moved recfun_codegen.ML to Code_Generator.thy
src/HOL/Code_Generator.thy
src/HOL/Datatype.thy
src/HOL/Fun.thy
src/HOL/Inductive.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Code_Generator.thy	Wed May 09 07:53:04 2007 +0200
     1.2 +++ b/src/HOL/Code_Generator.thy	Wed May 09 07:53:06 2007 +0200
     1.3 @@ -6,8 +6,16 @@
     1.4  
     1.5  theory Code_Generator
     1.6  imports HOL
     1.7 +uses "~~/src/HOL/Tools/recfun_codegen.ML"
     1.8  begin
     1.9  
    1.10 +ML {*
    1.11 +structure HOL =
    1.12 +struct
    1.13 +  val thy = theory "HOL";
    1.14 +end;
    1.15 +*}  -- "belongs to theory HOL"
    1.16 +
    1.17  subsection {* SML code generator setup *}
    1.18  
    1.19  types_code
    1.20 @@ -55,6 +63,7 @@
    1.21  in
    1.22  
    1.23  Codegen.add_codegen "eq_codegen" eq_codegen
    1.24 +#> RecfunCodegen.setup
    1.25  
    1.26  end
    1.27  *}
    1.28 @@ -107,7 +116,7 @@
    1.29    shows "(\<not> True) = False"
    1.30      and "(\<not> False) = True" by (rule HOL.simp_thms)+
    1.31  
    1.32 -lemmas [code func] = imp_conv_disj
    1.33 +lemmas [code] = imp_conv_disj
    1.34  
    1.35  lemmas [code func] = if_True if_False
    1.36  
    1.37 @@ -174,7 +183,7 @@
    1.38  oracle eval_oracle ("term") = {* fn thy => fn t => 
    1.39    if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
    1.40    then t
    1.41 -  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
    1.42 +  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    1.43  *}
    1.44  
    1.45  method_setup eval = {*
     2.1 --- a/src/HOL/Datatype.thy	Wed May 09 07:53:04 2007 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Wed May 09 07:53:06 2007 +0200
     2.3 @@ -102,7 +102,7 @@
     2.4  
     2.5  (** apfst -- can be used in similar type definitions **)
     2.6  
     2.7 -lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)"
     2.8 +lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)"
     2.9  by (simp add: apfst_def)
    2.10  
    2.11  
    2.12 @@ -715,12 +715,12 @@
    2.13  
    2.14  constdefs
    2.15    option_map :: "('a => 'b) => ('a option => 'b option)"
    2.16 -  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.17 +  [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)"
    2.18  
    2.19 -lemma option_map_None [simp, code func]: "option_map f None = None"
    2.20 +lemma option_map_None [simp, code]: "option_map f None = None"
    2.21    by (simp add: option_map_def)
    2.22  
    2.23 -lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)"
    2.24 +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
    2.25    by (simp add: option_map_def)
    2.26  
    2.27  lemma option_map_is_None [iff]:
    2.28 @@ -742,13 +742,9 @@
    2.29  
    2.30  subsubsection {* Code generator setup *}
    2.31  
    2.32 -lemmas [code] = fst_conv snd_conv imp_conv_disj
    2.33 -
    2.34  definition
    2.35    is_none :: "'a option \<Rightarrow> bool" where
    2.36 -  is_none_none [normal post, symmetric]: "is_none x \<longleftrightarrow> x = None"
    2.37 -
    2.38 -lemmas [code inline] = is_none_none
    2.39 +  is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    2.40  
    2.41  lemma is_none_code [code]:
    2.42    shows "is_none None \<longleftrightarrow> True"
     3.1 --- a/src/HOL/Fun.thy	Wed May 09 07:53:04 2007 +0200
     3.2 +++ b/src/HOL/Fun.thy	Wed May 09 07:53:06 2007 +0200
     3.3 @@ -7,12 +7,12 @@
     3.4  header {* Notions about functions *}
     3.5  
     3.6  theory Fun
     3.7 -imports Set Code_Generator
     3.8 +imports Set
     3.9  begin
    3.10  
    3.11  constdefs
    3.12    fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    3.13 -  [code func]: "fun_upd f a b == % x. if x=a then b else f x"
    3.14 +  "fun_upd f a b == % x. if x=a then b else f x"
    3.15  
    3.16  nonterminals
    3.17    updbinds updbind
     4.1 --- a/src/HOL/Inductive.thy	Wed May 09 07:53:04 2007 +0200
     4.2 +++ b/src/HOL/Inductive.thy	Wed May 09 07:53:06 2007 +0200
     4.3 @@ -21,7 +21,6 @@
     4.4    ("Tools/datatype_case.ML")
     4.5    ("Tools/datatype_package.ML")
     4.6    ("Tools/datatype_codegen.ML")
     4.7 -  ("Tools/recfun_codegen.ML")
     4.8    ("Tools/primrec_package.ML")
     4.9  begin
    4.10  
    4.11 @@ -61,7 +60,7 @@
    4.12  
    4.13  text {* Package setup. *}
    4.14  
    4.15 -use "Tools/old_inductive_package.ML"
    4.16 +ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *}
    4.17  setup OldInductivePackage.setup
    4.18  
    4.19  theorems basic_monos [mono] =
    4.20 @@ -90,12 +89,12 @@
    4.21    then show P ..
    4.22  next
    4.23    assume "\<And>P\<Colon>bool. P"
    4.24 -  then show "False" ..
    4.25 +  then show False ..
    4.26  qed
    4.27  
    4.28  lemma not_eq_False:
    4.29    assumes not_eq: "x \<noteq> y"
    4.30 -  and eq: "x == y"
    4.31 +  and eq: "x \<equiv> y"
    4.32    shows False
    4.33    using not_eq eq by auto
    4.34  
    4.35 @@ -107,9 +106,6 @@
    4.36  
    4.37  text {* Package setup. *}
    4.38  
    4.39 -use "Tools/recfun_codegen.ML"
    4.40 -setup RecfunCodegen.setup
    4.41 -
    4.42  use "Tools/datatype_aux.ML"
    4.43  use "Tools/datatype_prop.ML"
    4.44  use "Tools/datatype_rep_proofs.ML"
     5.1 --- a/src/HOL/Orderings.thy	Wed May 09 07:53:04 2007 +0200
     5.2 +++ b/src/HOL/Orderings.thy	Wed May 09 07:53:06 2007 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Syntactic and abstract orders *}
     5.5  
     5.6  theory Orderings
     5.7 -imports HOL
     5.8 +imports Code_Generator
     5.9  begin
    5.10  
    5.11  subsection {* Order syntax *}
    5.12 @@ -798,7 +798,7 @@
    5.13  
    5.14  subsection {* Order on bool *}
    5.15  
    5.16 -instance bool :: linorder 
    5.17 +instance bool :: order 
    5.18    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
    5.19    less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    5.20    by default (auto simp add: le_bool_def less_bool_def)
    5.21 @@ -892,11 +892,6 @@
    5.22  
    5.23  ML {*
    5.24  val monoI = @{thm monoI};
    5.25 -
    5.26 -structure HOL =
    5.27 -struct
    5.28 -  val thy = theory "HOL";
    5.29 -end;
    5.30 -*}  -- "belongs to theory HOL"
    5.31 +*}
    5.32  
    5.33  end
     6.1 --- a/src/HOL/Product_Type.thy	Wed May 09 07:53:04 2007 +0200
     6.2 +++ b/src/HOL/Product_Type.thy	Wed May 09 07:53:06 2007 +0200
     6.3 @@ -231,10 +231,10 @@
     6.4  lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
     6.5    by (blast elim!: Pair_inject)
     6.6  
     6.7 -lemma fst_conv [simp]: "fst (a, b) = a"
     6.8 +lemma fst_conv [simp, code]: "fst (a, b) = a"
     6.9    unfolding fst_def by blast
    6.10  
    6.11 -lemma snd_conv [simp]: "snd (a, b) = b"
    6.12 +lemma snd_conv [simp, code]: "snd (a, b) = b"
    6.13    unfolding snd_def by blast
    6.14  
    6.15  lemma fst_eqD: "fst (x, y) = a ==> x = a"
    6.16 @@ -602,18 +602,18 @@
    6.17  definition
    6.18    upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
    6.19  where
    6.20 -  "upd_fst f = prod_fun f id"
    6.21 +  [code func del]: "upd_fst f = prod_fun f id"
    6.22  
    6.23  definition
    6.24    upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
    6.25  where
    6.26 -  "upd_snd f = prod_fun id f"
    6.27 +  [code func del]: "upd_snd f = prod_fun id f"
    6.28  
    6.29 -lemma upd_fst_conv [simp, code func]:
    6.30 +lemma upd_fst_conv [simp, code]:
    6.31    "upd_fst f (x, y) = (f x, y)" 
    6.32    by (simp add: upd_fst_def)
    6.33  
    6.34 -lemma upd_snd_conv [simp, code func]:
    6.35 +lemma upd_snd_conv [simp, code]:
    6.36    "upd_snd f (x, y) = (x, f y)" 
    6.37    by (simp add: upd_snd_def)
    6.38  
    6.39 @@ -776,8 +776,6 @@
    6.40  
    6.41  subsection {* Code generator setup *}
    6.42  
    6.43 -lemmas [code func] = fst_conv snd_conv
    6.44 -
    6.45  instance unit :: eq ..
    6.46  
    6.47  lemma [code func]:
    6.48 @@ -910,8 +908,7 @@
    6.49  
    6.50    Codegen.add_codegen "let_codegen" let_codegen
    6.51    #> Codegen.add_codegen "split_codegen" split_codegen
    6.52 -  #> CodegenPackage.add_appconst
    6.53 -       ("Let", CodegenPackage.appgen_let)
    6.54 +  #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let)
    6.55  
    6.56  end
    6.57  *}