Theory Lem_show_extra

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

theory "Lem_show_extra" 

imports
  Main
  "Lem_string"
  "Lem_maybe"
  "Lem_num"
  "Lem_basic_classes"
  "Lem_set"
  "Lem_relation"
  "Lem_show"
  "Lem_set_extra"
  "Lem_string_extra"

begin 



― ‹‹open import String Maybe Num Basic_classes Set Relation Show›› 
― ‹‹import Set_extra String_extra››

definition instance_Show_Show_nat_dict  :: "(nat)Show_class "  where 
     " instance_Show_Show_nat_dict = ((|

  show_method = Lem_string_extra.stringFromNat |) )"


definition instance_Show_Show_Num_natural_dict  :: "(nat)Show_class "  where 
     " instance_Show_Show_Num_natural_dict = ((|

  show_method = Lem_string_extra.stringFromNatural |) )"


definition instance_Show_Show_Num_int_dict  :: "(int)Show_class "  where 
     " instance_Show_Show_Num_int_dict = ((|

  show_method = Lem_string_extra.stringFromInt |) )"


definition instance_Show_Show_Num_integer_dict  :: "(int)Show_class "  where 
     " instance_Show_Show_Num_integer_dict = ((|

  show_method = Lem_string_extra.stringFromInteger |) )"


definition stringFromSet  :: "('a ⇒ string)⇒ 'a set ⇒ string "  where 
     " stringFromSet showX xs = (
  (''{'') @ (Lem_show.stringFromListAux showX (list_of_set xs) @ (''}'')))"


― ‹‹ Abbreviates the representation if the relation is transitive. ››
definition stringFromRelation  :: "('a*'a ⇒ string)⇒('a*'a)set ⇒ string "  where 
     " stringFromRelation showX rel = (
  if trans rel then
    (let pruned_rel = (LemExtraDefs.without_trans_edges rel) in
    if ((∀ e ∈ rel.  (e ∈ pruned_rel))) then
      ― ‹‹ The relations are the same (there are no transitive edges),
         so we can just as well print the original one. ››
      stringFromSet showX rel
    else
      (''trancl of '') @ stringFromSet showX pruned_rel)
  else
    stringFromSet showX rel )"


definition instance_Show_Show_set_dict  :: " 'a Show_class ⇒('a set)Show_class "  where 
     " instance_Show_Show_set_dict dict_Show_Show_a = ((|

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

end