Lem_show_extra.thy

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 \<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 = (withoutTransitiveEdges 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