Nominal-General/nominal_library.ML
changeset 2389 0f24c961b5f6
parent 2384 841b7e34e70a
child 2397 c670a849af65
equal deleted inserted replaced
2388:ebf253d80670 2389:0f24c961b5f6
    33 
    33 
    34   val mk_diff: term * term -> term
    34   val mk_diff: term * term -> term
    35   val mk_append: term * term -> term
    35   val mk_append: term * term -> term
    36   val mk_union: term * term -> term
    36   val mk_union: term * term -> term
    37   val fold_union: term list -> term
    37   val fold_union: term list -> term
       
    38   val mk_conj: term * term -> term
       
    39   val fold_conj: term list -> term
    38 
    40 
    39   (* datatype operations *)
    41   (* datatype operations *)
    40   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
    42   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
    41   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
    43   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
    42   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
    44   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
   100 
   102 
   101 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   103 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   102   | mk_diff (t1, @{term "{}::atom set"}) = t1
   104   | mk_diff (t1, @{term "{}::atom set"}) = t1
   103   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
   105   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
   104 
   106 
   105 fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}
   107 fun mk_append (t1, @{term "[]::atom list"}) = t1
   106   | mk_append (t1, @{term "[]::atom list"}) = t1
       
   107   | mk_append (@{term "[]::atom list"}, t2) = t2
   108   | mk_append (@{term "[]::atom list"}, t2) = t2
   108   | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 
   109   | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 
   109 
   110 
   110 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
   111 fun mk_union (t1, @{term "{}::atom set"}) = t1
   111   | mk_union (t1 , @{term "{}::atom set"}) = t1
       
   112   | mk_union (@{term "{}::atom set"}, t2) = t2
   112   | mk_union (@{term "{}::atom set"}, t2) = t2
   113   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
   113   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
   114  
   114  
   115 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
   115 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
   116 
   116 
   117 
   117 fun mk_conj (t1, @{term "True"}) = t1
   118 
   118   | mk_conj (@{term "True"}, t2) = t2
       
   119   | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
       
   120 
       
   121 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
   119 
   122 
   120 (** datatypes **)
   123 (** datatypes **)
   121 
   124 
   122 
   125 
   123 (* returns the type of the nth datatype *)
   126 (* returns the type of the nth datatype *)