src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 41047 9f1d3fcef1ca
parent 41046 f2e94005d283
child 41049 0edd245892ed
equal deleted inserted replaced
41046:f2e94005d283 41047:9f1d3fcef1ca
    53     Subset |
    53     Subset |
    54     DefEq |
    54     DefEq |
    55     Eq |
    55     Eq |
    56     Triad |
    56     Triad |
    57     Composition |
    57     Composition |
    58     Product |
       
    59     Image |
    58     Image |
    60     Apply |
    59     Apply |
    61     Lambda
    60     Lambda
    62 
    61 
    63   datatype op3 =
    62   datatype op3 =
   168   Subset |
   167   Subset |
   169   DefEq |
   168   DefEq |
   170   Eq |
   169   Eq |
   171   Triad |
   170   Triad |
   172   Composition |
   171   Composition |
   173   Product |
       
   174   Image |
   172   Image |
   175   Apply |
   173   Apply |
   176   Lambda
   174   Lambda
   177 
   175 
   178 datatype op3 =
   176 datatype op3 =
   233   | string_for_op2 Subset = "Subset"
   231   | string_for_op2 Subset = "Subset"
   234   | string_for_op2 DefEq = "DefEq"
   232   | string_for_op2 DefEq = "DefEq"
   235   | string_for_op2 Eq = "Eq"
   233   | string_for_op2 Eq = "Eq"
   236   | string_for_op2 Triad = "Triad"
   234   | string_for_op2 Triad = "Triad"
   237   | string_for_op2 Composition = "Composition"
   235   | string_for_op2 Composition = "Composition"
   238   | string_for_op2 Product = "Product"
       
   239   | string_for_op2 Image = "Image"
   236   | string_for_op2 Image = "Image"
   240   | string_for_op2 Apply = "Apply"
   237   | string_for_op2 Apply = "Apply"
   241   | string_for_op2 Lambda = "Lambda"
   238   | string_for_op2 Lambda = "Lambda"
   242 
   239 
   243 fun string_for_op3 Let = "Let"
   240 fun string_for_op3 Let = "Let"
   526           Op1 (Converse, range_type T, Any, sub t1)
   523           Op1 (Converse, range_type T, Any, sub t1)
   527         | (Const (@{const_name trancl}, T), [t1]) =>
   524         | (Const (@{const_name trancl}, T), [t1]) =>
   528           Op1 (Closure, range_type T, Any, sub t1)
   525           Op1 (Closure, range_type T, Any, sub t1)
   529         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   526         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   530           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   527           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   531         | (Const (@{const_name prod}, T), [t1, t2]) =>
       
   532           Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2)
       
   533         | (Const (@{const_name image}, T), [t1, t2]) =>
   528         | (Const (@{const_name image}, T), [t1, t2]) =>
   534           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
   529           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
   535         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   530         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   536           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   531           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   537           else if is_constr ctxt stds x then do_construct x []
   532           else if is_constr ctxt stds x then do_construct x []