merged Code_Generator.thy into HOL.thy
authorhaftmann
Tue Jun 05 15:16:08 2007 +0200 (2007-06-05)
changeset 23247b99dce43d252
parent 23246 309a57cae012
child 23248 ef04b4c12593
merged Code_Generator.thy into HOL.thy
src/HOL/Code_Generator.thy
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Typedef.thy
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Tue Jun 05 12:12:25 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,230 +0,0 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Author:     Florian Haftmann, TU Muenchen
     1.6 -*)
     1.7 -
     1.8 -header {* Setup of code generator tools *}
     1.9 -
    1.10 -theory Code_Generator
    1.11 -imports HOL
    1.12 -uses "~~/src/HOL/Tools/recfun_codegen.ML"
    1.13 -begin
    1.14 -
    1.15 -ML {*
    1.16 -structure HOL =
    1.17 -struct
    1.18 -  val thy = theory "HOL";
    1.19 -end;
    1.20 -*}  -- "belongs to theory HOL"
    1.21 -
    1.22 -subsection {* SML code generator setup *}
    1.23 -
    1.24 -types_code
    1.25 -  "bool"  ("bool")
    1.26 -attach (term_of) {*
    1.27 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.28 -*}
    1.29 -attach (test) {*
    1.30 -fun gen_bool i = one_of [false, true];
    1.31 -*}
    1.32 -  "prop"  ("bool")
    1.33 -attach (term_of) {*
    1.34 -fun term_of_prop b =
    1.35 -  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    1.36 -*}
    1.37 -
    1.38 -consts_code
    1.39 -  "Trueprop" ("(_)")
    1.40 -  "True"    ("true")
    1.41 -  "False"   ("false")
    1.42 -  "Not"     ("Bool.not")
    1.43 -  "op |"    ("(_ orelse/ _)")
    1.44 -  "op &"    ("(_ andalso/ _)")
    1.45 -  "If"      ("(if _/ then _/ else _)")
    1.46 -
    1.47 -setup {*
    1.48 -let
    1.49 -
    1.50 -fun eq_codegen thy defs gr dep thyname b t =
    1.51 -    (case strip_comb t of
    1.52 -       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.53 -     | (Const ("op =", _), [t, u]) =>
    1.54 -          let
    1.55 -            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.56 -            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    1.57 -            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    1.58 -          in
    1.59 -            SOME (gr''', Codegen.parens
    1.60 -              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.61 -          end
    1.62 -     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.63 -         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.64 -     | _ => NONE);
    1.65 -
    1.66 -in
    1.67 -
    1.68 -Codegen.add_codegen "eq_codegen" eq_codegen
    1.69 -#> RecfunCodegen.setup
    1.70 -
    1.71 -end
    1.72 -*}
    1.73 -
    1.74 -text {* Evaluation *}
    1.75 -
    1.76 -method_setup evaluation = {*
    1.77 -let
    1.78 -
    1.79 -fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    1.80 -  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
    1.81 -
    1.82 -in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
    1.83 -*} "solve goal by evaluation"
    1.84 -
    1.85 -
    1.86 -subsection {* Generic code generator setup *}
    1.87 -
    1.88 -text {* operational equality for code generation *}
    1.89 -
    1.90 -class eq (attach "op =") = type
    1.91 -
    1.92 -
    1.93 -text {* using built-in Haskell equality *}
    1.94 -
    1.95 -code_class eq
    1.96 -  (Haskell "Eq" where "op =" \<equiv> "(==)")
    1.97 -
    1.98 -code_const "op ="
    1.99 -  (Haskell infixl 4 "==")
   1.100 -
   1.101 -
   1.102 -text {* type bool *}
   1.103 -
   1.104 -code_datatype True False
   1.105 -
   1.106 -lemma [code func]:
   1.107 -  shows "(False \<and> x) = False"
   1.108 -    and "(True \<and> x) = x"
   1.109 -    and "(x \<and> False) = False"
   1.110 -    and "(x \<and> True) = x" by simp_all
   1.111 -
   1.112 -lemma [code func]:
   1.113 -  shows "(False \<or> x) = x"
   1.114 -    and "(True \<or> x) = True"
   1.115 -    and "(x \<or> False) = x"
   1.116 -    and "(x \<or> True) = True" by simp_all
   1.117 -
   1.118 -lemma [code func]:
   1.119 -  shows "(\<not> True) = False"
   1.120 -    and "(\<not> False) = True" by (rule HOL.simp_thms)+
   1.121 -
   1.122 -lemmas [code] = imp_conv_disj
   1.123 -
   1.124 -lemmas [code func] = if_True if_False
   1.125 -
   1.126 -instance bool :: eq ..
   1.127 -
   1.128 -lemma [code func]:
   1.129 -  shows "True = P \<longleftrightarrow> P"
   1.130 -    and "False = P \<longleftrightarrow> \<not> P"
   1.131 -    and "P = True \<longleftrightarrow> P"
   1.132 -    and "P = False \<longleftrightarrow> \<not> P" by simp_all
   1.133 -
   1.134 -code_type bool
   1.135 -  (SML "bool")
   1.136 -  (OCaml "bool")
   1.137 -  (Haskell "Bool")
   1.138 -
   1.139 -code_instance bool :: eq
   1.140 -  (Haskell -)
   1.141 -
   1.142 -code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   1.143 -  (Haskell infixl 4 "==")
   1.144 -
   1.145 -code_const True and False and Not and "op &" and "op |" and If
   1.146 -  (SML "true" and "false" and "not"
   1.147 -    and infixl 1 "andalso" and infixl 0 "orelse"
   1.148 -    and "!(if (_)/ then (_)/ else (_))")
   1.149 -  (OCaml "true" and "false" and "not"
   1.150 -    and infixl 4 "&&" and infixl 2 "||"
   1.151 -    and "!(if (_)/ then (_)/ else (_))")
   1.152 -  (Haskell "True" and "False" and "not"
   1.153 -    and infixl 3 "&&" and infixl 2 "||"
   1.154 -    and "!(if (_)/ then (_)/ else (_))")
   1.155 -
   1.156 -code_reserved SML
   1.157 -  bool true false not
   1.158 -
   1.159 -code_reserved OCaml
   1.160 -  bool true false not
   1.161 -
   1.162 -
   1.163 -text {* type prop *}
   1.164 -
   1.165 -code_datatype Trueprop "prop"
   1.166 -
   1.167 -
   1.168 -text {* type itself *}
   1.169 -
   1.170 -code_datatype "TYPE('a)"
   1.171 -
   1.172 -
   1.173 -text {* code generation for undefined as exception *}
   1.174 -
   1.175 -code_const undefined
   1.176 -  (SML "raise/ Fail/ \"undefined\"")
   1.177 -  (OCaml "failwith/ \"undefined\"")
   1.178 -  (Haskell "error/ \"undefined\"")
   1.179 -
   1.180 -code_reserved SML Fail
   1.181 -code_reserved OCaml failwith
   1.182 -
   1.183 -
   1.184 -subsection {* Evaluation oracle *}
   1.185 -
   1.186 -oracle eval_oracle ("term") = {* fn thy => fn t => 
   1.187 -  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   1.188 -  then t
   1.189 -  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   1.190 -*}
   1.191 -
   1.192 -method_setup eval = {*
   1.193 -let
   1.194 -  fun eval_tac thy = 
   1.195 -    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   1.196 -in 
   1.197 -  Method.ctxt_args (fn ctxt => 
   1.198 -    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   1.199 -end
   1.200 -*} "solve goal by evaluation"
   1.201 -
   1.202 -
   1.203 -subsection {* Normalization by evaluation *}
   1.204 -
   1.205 -method_setup normalization = {*
   1.206 -let
   1.207 -  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
   1.208 -    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
   1.209 -      NBE.normalization_conv)));
   1.210 -in
   1.211 -  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
   1.212 -end
   1.213 -*} "solve goal by normalization"
   1.214 -
   1.215 -
   1.216 -text {* lazy @{const If} *}
   1.217 -
   1.218 -definition
   1.219 -  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.220 -  [code func del]: "if_delayed b f g = (if b then f True else g False)"
   1.221 -
   1.222 -lemma [code func]:
   1.223 -  shows "if_delayed True f g = f True"
   1.224 -    and "if_delayed False f g = g False"
   1.225 -  unfolding if_delayed_def by simp_all
   1.226 -
   1.227 -lemma [normal pre, symmetric, normal post]:
   1.228 -  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
   1.229 -  unfolding if_delayed_def ..
   1.230 -
   1.231 -hide (open) const if_delayed
   1.232 -
   1.233 -end
     2.1 --- a/src/HOL/HOL.thy	Tue Jun 05 12:12:25 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Tue Jun 05 15:16:08 2007 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  theory HOL
     2.5  imports CPure
     2.6  uses
     2.7 +  "~~/src/Tools/integer.ML"
     2.8    "hologic.ML"
     2.9    "~~/src/Provers/splitter.ML"
    2.10    "~~/src/Provers/hypsubst.ML"
    2.11 @@ -20,8 +21,7 @@
    2.12    "~~/src/Provers/classical.ML"
    2.13    "~~/src/Provers/blast.ML"
    2.14    "~~/src/Provers/clasimp.ML"
    2.15 -  "~~/src/Pure/General/int.ML"
    2.16 -  "~~/src/Pure/General/rat.ML"
    2.17 +  "~~/src/Tools/rat.ML"
    2.18    "~~/src/Provers/Arith/fast_lin_arith.ML"
    2.19    "~~/src/Provers/Arith/cancel_sums.ML"
    2.20    "~~/src/Provers/quantifier1.ML"
    2.21 @@ -33,6 +33,7 @@
    2.22    "~~/src/Provers/quasi.ML"
    2.23    "~~/src/Provers/order.ML"
    2.24    ("simpdata.ML")
    2.25 +  ("~~/src/HOL/Tools/recfun_codegen.ML")
    2.26    "Tools/res_atpset.ML"
    2.27  begin
    2.28  
    2.29 @@ -1495,6 +1496,222 @@
    2.30  *}
    2.31  
    2.32  
    2.33 +subsection {* Code generator setup *}
    2.34 +
    2.35 +subsubsection {* SML code generator setup *}
    2.36 +
    2.37 +use "~~/src/HOL/Tools/recfun_codegen.ML"
    2.38 +
    2.39 +types_code
    2.40 +  "bool"  ("bool")
    2.41 +attach (term_of) {*
    2.42 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    2.43 +*}
    2.44 +attach (test) {*
    2.45 +fun gen_bool i = one_of [false, true];
    2.46 +*}
    2.47 +  "prop"  ("bool")
    2.48 +attach (term_of) {*
    2.49 +fun term_of_prop b =
    2.50 +  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    2.51 +*}
    2.52 +
    2.53 +consts_code
    2.54 +  "Trueprop" ("(_)")
    2.55 +  "True"    ("true")
    2.56 +  "False"   ("false")
    2.57 +  "Not"     ("Bool.not")
    2.58 +  "op |"    ("(_ orelse/ _)")
    2.59 +  "op &"    ("(_ andalso/ _)")
    2.60 +  "If"      ("(if _/ then _/ else _)")
    2.61 +
    2.62 +setup {*
    2.63 +let
    2.64 +
    2.65 +fun eq_codegen thy defs gr dep thyname b t =
    2.66 +    (case strip_comb t of
    2.67 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    2.68 +     | (Const ("op =", _), [t, u]) =>
    2.69 +          let
    2.70 +            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    2.71 +            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    2.72 +            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    2.73 +          in
    2.74 +            SOME (gr''', Codegen.parens
    2.75 +              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    2.76 +          end
    2.77 +     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    2.78 +         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    2.79 +     | _ => NONE);
    2.80 +
    2.81 +in
    2.82 +
    2.83 +Codegen.add_codegen "eq_codegen" eq_codegen
    2.84 +#> RecfunCodegen.setup
    2.85 +
    2.86 +end
    2.87 +*}
    2.88 +
    2.89 +text {* Evaluation *}
    2.90 +
    2.91 +method_setup evaluation = {*
    2.92 +let
    2.93 +
    2.94 +fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    2.95 +  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
    2.96 +
    2.97 +in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
    2.98 +*} "solve goal by evaluation"
    2.99 +
   2.100 +
   2.101 +subsubsection {* Generic code generator setup *}
   2.102 +
   2.103 +text {* operational equality for code generation *}
   2.104 +
   2.105 +class eq (attach "op =") = type
   2.106 +
   2.107 +
   2.108 +text {* using built-in Haskell equality *}
   2.109 +
   2.110 +code_class eq
   2.111 +  (Haskell "Eq" where "op =" \<equiv> "(==)")
   2.112 +
   2.113 +code_const "op ="
   2.114 +  (Haskell infixl 4 "==")
   2.115 +
   2.116 +
   2.117 +text {* type bool *}
   2.118 +
   2.119 +code_datatype True False
   2.120 +
   2.121 +lemma [code func]:
   2.122 +  shows "(False \<and> x) = False"
   2.123 +    and "(True \<and> x) = x"
   2.124 +    and "(x \<and> False) = False"
   2.125 +    and "(x \<and> True) = x" by simp_all
   2.126 +
   2.127 +lemma [code func]:
   2.128 +  shows "(False \<or> x) = x"
   2.129 +    and "(True \<or> x) = True"
   2.130 +    and "(x \<or> False) = x"
   2.131 +    and "(x \<or> True) = True" by simp_all
   2.132 +
   2.133 +lemma [code func]:
   2.134 +  shows "(\<not> True) = False"
   2.135 +    and "(\<not> False) = True" by (rule HOL.simp_thms)+
   2.136 +
   2.137 +lemmas [code] = imp_conv_disj
   2.138 +
   2.139 +lemmas [code func] = if_True if_False
   2.140 +
   2.141 +instance bool :: eq ..
   2.142 +
   2.143 +lemma [code func]:
   2.144 +  shows "True = P \<longleftrightarrow> P"
   2.145 +    and "False = P \<longleftrightarrow> \<not> P"
   2.146 +    and "P = True \<longleftrightarrow> P"
   2.147 +    and "P = False \<longleftrightarrow> \<not> P" by simp_all
   2.148 +
   2.149 +code_type bool
   2.150 +  (SML "bool")
   2.151 +  (OCaml "bool")
   2.152 +  (Haskell "Bool")
   2.153 +
   2.154 +code_instance bool :: eq
   2.155 +  (Haskell -)
   2.156 +
   2.157 +code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   2.158 +  (Haskell infixl 4 "==")
   2.159 +
   2.160 +code_const True and False and Not and "op &" and "op |" and If
   2.161 +  (SML "true" and "false" and "not"
   2.162 +    and infixl 1 "andalso" and infixl 0 "orelse"
   2.163 +    and "!(if (_)/ then (_)/ else (_))")
   2.164 +  (OCaml "true" and "false" and "not"
   2.165 +    and infixl 4 "&&" and infixl 2 "||"
   2.166 +    and "!(if (_)/ then (_)/ else (_))")
   2.167 +  (Haskell "True" and "False" and "not"
   2.168 +    and infixl 3 "&&" and infixl 2 "||"
   2.169 +    and "!(if (_)/ then (_)/ else (_))")
   2.170 +
   2.171 +code_reserved SML
   2.172 +  bool true false not
   2.173 +
   2.174 +code_reserved OCaml
   2.175 +  bool true false not
   2.176 +
   2.177 +
   2.178 +text {* type prop *}
   2.179 +
   2.180 +code_datatype Trueprop "prop"
   2.181 +
   2.182 +
   2.183 +text {* type itself *}
   2.184 +
   2.185 +code_datatype "TYPE('a)"
   2.186 +
   2.187 +
   2.188 +text {* code generation for undefined as exception *}
   2.189 +
   2.190 +code_const undefined
   2.191 +  (SML "raise/ Fail/ \"undefined\"")
   2.192 +  (OCaml "failwith/ \"undefined\"")
   2.193 +  (Haskell "error/ \"undefined\"")
   2.194 +
   2.195 +code_reserved SML Fail
   2.196 +code_reserved OCaml failwith
   2.197 +
   2.198 +
   2.199 +subsubsection {* Evaluation oracle *}
   2.200 +
   2.201 +oracle eval_oracle ("term") = {* fn thy => fn t => 
   2.202 +  if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   2.203 +  then t
   2.204 +  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   2.205 +*}
   2.206 +
   2.207 +method_setup eval = {*
   2.208 +let
   2.209 +  fun eval_tac thy = 
   2.210 +    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   2.211 +in 
   2.212 +  Method.ctxt_args (fn ctxt => 
   2.213 +    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   2.214 +end
   2.215 +*} "solve goal by evaluation"
   2.216 +
   2.217 +
   2.218 +subsubsection {* Normalization by evaluation *}
   2.219 +
   2.220 +method_setup normalization = {*
   2.221 +let
   2.222 +  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
   2.223 +    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
   2.224 +      NBE.normalization_conv)));
   2.225 +in
   2.226 +  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
   2.227 +end
   2.228 +*} "solve goal by normalization"
   2.229 +
   2.230 +
   2.231 +text {* lazy @{const If} *}
   2.232 +
   2.233 +definition
   2.234 +  if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.235 +  [code func del]: "if_delayed b f g = (if b then f True else g False)"
   2.236 +
   2.237 +lemma [code func]:
   2.238 +  shows "if_delayed True f g = f True"
   2.239 +    and "if_delayed False f g = g False"
   2.240 +  unfolding if_delayed_def by simp_all
   2.241 +
   2.242 +lemma [normal pre, symmetric, normal post]:
   2.243 +  "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
   2.244 +  unfolding if_delayed_def ..
   2.245 +
   2.246 +hide (open) const if_delayed
   2.247 +
   2.248 +
   2.249  subsection {* Legacy tactics and ML bindings *}
   2.250  
   2.251  ML {*
     3.1 --- a/src/HOL/IsaMakefile	Tue Jun 05 12:12:25 2007 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Jun 05 15:16:08 2007 +0200
     3.3 @@ -80,9 +80,9 @@
     3.4    $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
     3.5    $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
     3.6    $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
     3.7 -  $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML			\
     3.8 -  $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML			\
     3.9 -  ATP_Linkup.thy Accessible_Part.thy Code_Generator.thy Datatype.thy	\
    3.10 +  $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML			\
    3.11 +  $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML			\
    3.12 +  ATP_Linkup.thy Accessible_Part.thy Datatype.thy	\
    3.13    Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy		\
    3.14    FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy		\
    3.15    Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
    3.16 @@ -152,7 +152,7 @@
    3.17  
    3.18  HOL-Complex: HOL $(OUT)/HOL-Complex
    3.19  
    3.20 -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Pure/General/float.ML \
    3.21 +$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
    3.22    Library/Zorn.thy							\
    3.23    Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/float_arith.ML	\
    3.24    Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy	\
     4.1 --- a/src/HOL/Orderings.thy	Tue Jun 05 12:12:25 2007 +0200
     4.2 +++ b/src/HOL/Orderings.thy	Tue Jun 05 15:16:08 2007 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Syntactic and abstract orders *}
     4.5  
     4.6  theory Orderings
     4.7 -imports Code_Generator
     4.8 +imports HOL
     4.9  begin
    4.10  
    4.11  subsection {* Order syntax *}
     5.1 --- a/src/HOL/Product_Type.thy	Tue Jun 05 12:12:25 2007 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Tue Jun 05 15:16:08 2007 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Cartesian products *}
     5.5  
     5.6  theory Product_Type
     5.7 -imports Typedef Fun Code_Generator
     5.8 +imports Typedef Fun
     5.9  uses ("Tools/split_rule.ML")
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Typedef.thy	Tue Jun 05 12:12:25 2007 +0200
     6.2 +++ b/src/HOL/Typedef.thy	Tue Jun 05 15:16:08 2007 +0200
     6.3 @@ -13,14 +13,19 @@
     6.4    ("Tools/typedef_codegen.ML")
     6.5  begin
     6.6  
     6.7 +ML {*
     6.8 +structure HOL = struct val thy = theory "HOL" end;
     6.9 +*}  -- "belongs to theory HOL"
    6.10 +
    6.11  locale type_definition =
    6.12    fixes Rep and Abs and A
    6.13    assumes Rep: "Rep x \<in> A"
    6.14      and Rep_inverse: "Abs (Rep x) = x"
    6.15      and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
    6.16    -- {* This will be axiomatized for each typedef! *}
    6.17 +begin
    6.18  
    6.19 -lemma (in type_definition) Rep_inject:
    6.20 +lemma Rep_inject:
    6.21    "(Rep x = Rep y) = (x = y)"
    6.22  proof
    6.23    assume "Rep x = Rep y"
    6.24 @@ -33,7 +38,7 @@
    6.25    thus "Rep x = Rep y" by (simp only:)
    6.26  qed
    6.27  
    6.28 -lemma (in type_definition) Abs_inject:
    6.29 +lemma Abs_inject:
    6.30    assumes x: "x \<in> A" and y: "y \<in> A"
    6.31    shows "(Abs x = Abs y) = (x = y)"
    6.32  proof
    6.33 @@ -47,7 +52,7 @@
    6.34    thus "Abs x = Abs y" by (simp only:)
    6.35  qed
    6.36  
    6.37 -lemma (in type_definition) Rep_cases [cases set]:
    6.38 +lemma Rep_cases [cases set]:
    6.39    assumes y: "y \<in> A"
    6.40      and hyp: "!!x. y = Rep x ==> P"
    6.41    shows P
    6.42 @@ -56,7 +61,7 @@
    6.43    thus "y = Rep (Abs y)" ..
    6.44  qed
    6.45  
    6.46 -lemma (in type_definition) Abs_cases [cases type]:
    6.47 +lemma Abs_cases [cases type]:
    6.48    assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
    6.49    shows P
    6.50  proof (rule r)
    6.51 @@ -65,7 +70,7 @@
    6.52    show "Rep x \<in> A" by (rule Rep)
    6.53  qed
    6.54  
    6.55 -lemma (in type_definition) Rep_induct [induct set]:
    6.56 +lemma Rep_induct [induct set]:
    6.57    assumes y: "y \<in> A"
    6.58      and hyp: "!!x. P (Rep x)"
    6.59    shows "P y"
    6.60 @@ -75,7 +80,7 @@
    6.61    finally show "P y" .
    6.62  qed
    6.63  
    6.64 -lemma (in type_definition) Abs_induct [induct type]:
    6.65 +lemma Abs_induct [induct type]:
    6.66    assumes r: "!!y. y \<in> A ==> P (Abs y)"
    6.67    shows "P x"
    6.68  proof -
    6.69 @@ -85,6 +90,8 @@
    6.70    finally show "P x" .
    6.71  qed
    6.72  
    6.73 +end
    6.74 +
    6.75  use "Tools/typedef_package.ML"
    6.76  use "Tools/typecopy_package.ML"
    6.77  use "Tools/typedef_codegen.ML"
     7.1 --- a/src/HOL/hologic.ML	Tue Jun 05 12:12:25 2007 +0200
     7.2 +++ b/src/HOL/hologic.ML	Tue Jun 05 15:16:08 2007 +0200
     7.3 @@ -71,8 +71,8 @@
     7.4    val mk_Suc: term -> term
     7.5    val dest_Suc: term -> term
     7.6    val Suc_zero: term
     7.7 -  val mk_nat: IntInf.int -> term
     7.8 -  val dest_nat: term -> IntInf.int
     7.9 +  val mk_nat: integer -> term
    7.10 +  val dest_nat: term -> integer
    7.11    val class_size: string
    7.12    val size_const: typ -> term
    7.13    val bitT: typ
    7.14 @@ -84,12 +84,12 @@
    7.15    val pls_const: term
    7.16    val min_const: term
    7.17    val bit_const: term
    7.18 -  val mk_numeral: IntInf.int -> term
    7.19 -  val dest_numeral: term -> IntInf.int
    7.20 +  val mk_numeral: integer -> term
    7.21 +  val dest_numeral: term -> integer
    7.22    val number_of_const: typ -> term
    7.23    val add_numerals_of: term -> (term * typ) list -> (term * typ) list
    7.24 -  val mk_number: typ -> IntInf.int -> term
    7.25 -  val dest_number: term -> typ * IntInf.int
    7.26 +  val mk_number: typ -> integer -> term
    7.27 +  val dest_number: term -> typ * integer
    7.28    val realT: typ
    7.29    val nibbleT: typ
    7.30    val mk_nibble: int -> term
    7.31 @@ -186,7 +186,7 @@
    7.32  fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
    7.33  fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    7.34  
    7.35 -val class_eq = "Code_Generator.eq";
    7.36 +val class_eq = "HOL.eq";
    7.37  
    7.38  fun mk_mem (x, A) =
    7.39    let val setT = fastype_of A in
    7.40 @@ -298,14 +298,14 @@
    7.41  fun mk_nat n =
    7.42    let
    7.43      fun mk 0 = zero
    7.44 -      | mk n = mk_Suc (mk (IntInf.- (n, 1)));
    7.45 -  in if IntInf.< (n, 0)
    7.46 +      | mk n = mk_Suc (mk (n -% 1));
    7.47 +  in if n < 0
    7.48      then error "mk_nat: negative numeral"
    7.49      else mk n
    7.50    end;
    7.51  
    7.52 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
    7.53 -  | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1)
    7.54 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = Integer.zero
    7.55 +  | dest_nat (Const ("Suc", _) $ t) = Integer.inc (dest_nat t)
    7.56    | dest_nat t = raise TERM ("dest_nat", [t]);
    7.57  
    7.58  val class_size = "Nat.size";
    7.59 @@ -335,18 +335,18 @@
    7.60  
    7.61  val pls_const = Const ("Numeral.Pls", intT)
    7.62  and min_const = Const ("Numeral.Min", intT)
    7.63 -and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
    7.64 +and bit_const = Const ("Numeral.Bit", intT --> bitT --> intT);
    7.65  
    7.66  fun mk_numeral 0 = pls_const
    7.67    | mk_numeral ~1 = min_const
    7.68    | mk_numeral i =
    7.69 -      let val (q, r) = IntInf.divMod (i, 2)
    7.70 -      in bit_const $ mk_numeral q $ mk_bit (IntInf.toInt r) end;
    7.71 +      let val (q, r) = Integer.divmod i 2
    7.72 +      in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end;
    7.73  
    7.74  fun dest_numeral (Const ("Numeral.Pls", _)) = 0
    7.75    | dest_numeral (Const ("Numeral.Min", _)) = ~1
    7.76    | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
    7.77 -      2 * dest_numeral bs + IntInf.fromInt (dest_bit b)
    7.78 +      2 *% dest_numeral bs +% Integer.int (dest_bit b)
    7.79    | dest_numeral t = raise TERM ("dest_numeral", [t]);
    7.80  
    7.81  fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);