Theory Lem_show

chapter ‹Generated by Lem from ‹show.lem›.›

theory "Lem_show" 

imports
  Main
  "Lem_string"
  "Lem_maybe"
  "Lem_num"
  "Lem_basic_classes"

begin 



― ‹‹open import String Maybe Num Basic_classes››

― ‹‹open import {hol} `lemTheory`››

record 'a Show_class=

  show_method::" 'a ⇒ string "



definition instance_Show_Show_string_dict  :: "(string)Show_class "  where 
     " instance_Show_Show_string_dict = ((|

  show_method = (λ s. ([(CHR 0x27)]) @ (s @ ([(CHR 0x27)])))|) )"


― ‹‹val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string››
fun stringFromMaybe  :: "('a ⇒ string)⇒ 'a option ⇒ string "  where 
     " stringFromMaybe showX (Some x) = ( (''Just ('') @ (showX x @ ('')'')))"
|" stringFromMaybe showX None = ( (''Nothing''))"


definition instance_Show_Show_Maybe_maybe_dict  :: " 'a Show_class ⇒('a option)Show_class "  where 
     " instance_Show_Show_Maybe_maybe_dict dict_Show_Show_a = ((|

  show_method = (λ x_opt. stringFromMaybe 
  (show_method   dict_Show_Show_a) x_opt)|) )"


― ‹‹val stringFromListAux : forall 'a. ('a -> string) -> list 'a -> string››
function (sequential,domintros)  stringFromListAux  :: "('a ⇒ string)⇒ 'a list ⇒ string "  where 
     " stringFromListAux showX ([]) = ( (''''))"
|" stringFromListAux showX (x # xs') = (
      (case  xs' of
        [] => showX x
      | _ => showX x @ ((''; '') @ stringFromListAux showX xs')
      ))" 
by pat_completeness auto


― ‹‹val stringFromList : forall 'a. ('a -> string) -> list 'a -> string››
definition stringFromList  :: "('a ⇒ string)⇒ 'a list ⇒ string "  where 
     " stringFromList showX xs = (
  (''['') @ (stringFromListAux showX xs @ ('']'')))"


definition instance_Show_Show_list_dict  :: " 'a Show_class ⇒('a list)Show_class "  where 
     " instance_Show_Show_list_dict dict_Show_Show_a = ((|

  show_method = (λ xs. stringFromList 
  (show_method   dict_Show_Show_a) xs)|) )"


― ‹‹val stringFromPair : forall 'a 'b. ('a -> string) -> ('b -> string) -> ('a * 'b) -> string››
fun stringFromPair  :: "('a ⇒ string)⇒('b ⇒ string)⇒ 'a*'b ⇒ string "  where 
     " stringFromPair showX showY (x,y) = (
  (''('') @ (showX x @ (('', '') @ (showY y @ ('')'')))))"


definition instance_Show_Show_tup2_dict  :: " 'a Show_class ⇒ 'b Show_class ⇒('a*'b)Show_class "  where 
     " instance_Show_Show_tup2_dict dict_Show_Show_a dict_Show_Show_b = ((|

  show_method = (stringFromPair 
  (show_method   dict_Show_Show_a) (show_method   dict_Show_Show_b))|) )"


definition instance_Show_Show_bool_dict  :: "(bool)Show_class "  where 
     " instance_Show_Show_bool_dict = ((|

  show_method = (λ b. if b then (''true'') else (''false''))|) )"

end