src/HOL/Datatype.thy
changeset 20453 855f07fabd76
parent 20105 454f4be984b7
child 20523 36a59e5d0039
equal deleted inserted replaced
20452:6d8b29c7a960 20453:855f07fabd76
   259 
   259 
   260 lemma split_is_prod_case [code inline]:
   260 lemma split_is_prod_case [code inline]:
   261   "split = prod_case"
   261   "split = prod_case"
   262 by (simp add: expand_fun_eq split_def prod.cases)
   262 by (simp add: expand_fun_eq split_def prod.cases)
   263 
   263 
   264 code_typapp bool
   264 code_type bool
   265   ml (target_atom "bool")
   265   (SML target_atom "bool")
   266   haskell (target_atom "Bool")
   266   (Haskell target_atom "Bool")
   267 
   267 
   268 code_constapp
   268 code_const True and False and Not and "op &" and "op |" and If
   269   True
   269   (SML target_atom "true" and target_atom "false" and target_atom "not"
   270     ml (target_atom "true")
   270     and infixl 1 "andalso" and infixl 0 "orelse"
   271     haskell (target_atom "True")
   271     and target_atom "(if __/ then __/ else __)")
   272   False
   272   (Haskell target_atom "True" and target_atom "False" and target_atom "not"
   273     ml (target_atom "false")
   273     and infixl 3 "&&" and infixl 2 "||"
   274     haskell (target_atom "False")
   274     and target_atom "(if __/ then __/ else __)")
   275   Not
   275 
   276     ml (target_atom "not")
   276 code_type *
   277     haskell (target_atom "not")
   277   (SML infix 2 "*")
   278   "op &"
   278   (Haskell target_atom "(__,/ __)")
   279     ml (infixl 1 "andalso")
   279 
   280     haskell (infixl 3 "&&")
   280 code_const Pair
   281   "op |"
   281   (SML target_atom "(__,/ __)")
   282     ml (infixl 0 "orelse")
   282   (Haskell target_atom "(__,/ __)")
   283     haskell (infixl 2 "||")
   283 
   284   If
   284 code_type unit
   285     ml (target_atom "(if __/ then __/ else __)")
   285   (SML target_atom "unit")
   286     haskell (target_atom "(if __/ then __/ else __)")
   286   (Haskell target_atom "()")
   287 
   287 
   288 code_typapp
   288 code_const Unity
   289   *
   289   (SML target_atom "()")
   290     ml (infix 2 "*")
   290   (Haskell target_atom "()")
   291     haskell (target_atom "(__,/ __)")
   291 
   292 
   292 code_type option
   293 code_constapp
   293   (SML "_ option")
   294   Pair
   294   (Haskell "Maybe _")
   295     ml (target_atom "(__,/ __)")
   295 
   296     haskell (target_atom "(__,/ __)")
   296 code_const None and Some
   297 
   297   (SML target_atom "NONE" and target_atom "SOME")
   298 code_typapp
   298   (Haskell target_atom "Nothing" and target_atom "Just")
   299   unit
       
   300     ml (target_atom "unit")
       
   301     haskell (target_atom "()")
       
   302 
       
   303 code_constapp
       
   304   Unity
       
   305     ml (target_atom "()")
       
   306     haskell (target_atom "()")
       
   307 
       
   308 code_typapp
       
   309   option
       
   310     ml ("_ option")
       
   311     haskell ("Maybe _")
       
   312 
       
   313 code_constapp
       
   314   None
       
   315     ml (target_atom "NONE")
       
   316     haskell (target_atom "Nothing")
       
   317   Some
       
   318     ml (target_atom "SOME")
       
   319     haskell (target_atom "Just")
       
   320 
   299 
   321 end
   300 end