Lem_show_extra.thy

chapter \<open>Generated by Lem from \<open>show_extra.lem\<close>.\<close>

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 \<Rightarrow> string)\<Rightarrow> 'a set \<Rightarrow> 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 \<Rightarrow> string)\<Rightarrow>('a*'a)set \<Rightarrow> string "  where 
     " stringFromRelation showX rel = (
  if trans rel then
    (let pruned_rel = (LemExtraDefs.without_trans_edges rel) in
    if ((\<forall> e \<in> rel.  (e \<in> 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 \<Rightarrow>('a set)Show_class "  where 
     " instance_Show_Show_set_dict dict_Show_Show_a = ((|

  show_method = (\<lambda> xs. stringFromSet 
  (show_method   dict_Show_Show_a) xs)|) )"

end