src/HOL/Tools/res_clause.ML
changeset 21290 33b6bb5d6ab8
parent 21254 d53f76357f41
child 21373 18f519614978
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Nov 10 19:04:18 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 10 20:58:48 2006 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val arity_clause_thy: theory -> arityClause list 
     1.5    val ascii_of : string -> string
     1.6    val bracket_pack : string list -> string
     1.7 -  val classrel_clauses_thy: theory -> classrelClause list 
     1.8 +  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
     1.9    val clause_prefix : string 
    1.10    val clause2tptp : clause -> string * string list
    1.11    val const_prefix : string
    1.12 @@ -529,23 +529,22 @@
    1.13  	 ClassrelClause of {axiom_name: axiom_name,
    1.14  			    subclass: class,
    1.15  			    superclass: class};
    1.16 -
    1.17 -fun make_axiom_classrelClause n subclass superclass =
    1.18 -  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^ 
    1.19 -                                "_" ^ Int.toString n,
    1.20 -                  subclass = make_type_class subclass, 
    1.21 -                  superclass = make_type_class superclass};
    1.22 + 
    1.23 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
    1.24 +fun class_pairs thy subs supers =
    1.25 +  let val class_less = Sorts.class_less(Sign.classes_of thy)
    1.26 +      fun add_super sub (super,pairs) = 
    1.27 +            if class_less (sub,super) then (sub,super)::pairs else pairs
    1.28 +      fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
    1.29 +  in  foldl add_supers [] subs  end;
    1.30  
    1.31 -fun classrelClauses_of_aux n sub [] = []
    1.32 -  | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*)
    1.33 -      classrelClauses_of_aux n sub sups
    1.34 -  | classrelClauses_of_aux n sub (sup::sups) =
    1.35 -      make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups;
    1.36 +fun make_classrelClause (sub,super) =
    1.37 +  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
    1.38 +                  subclass = make_type_class sub, 
    1.39 +                  superclass = make_type_class super};
    1.40  
    1.41 -fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
    1.42 -
    1.43 -val classrel_clauses_thy =
    1.44 -  maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
    1.45 +fun make_classrel_clauses thy subs supers =
    1.46 +  map make_classrelClause (class_pairs thy subs supers);
    1.47  
    1.48  
    1.49  (** Isabelle arities **)