src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 41049 0edd245892ed
parent 41047 9f1d3fcef1ca
child 41856 7244589c8ccc
equal deleted inserted replaced
41048:d5ebe94248ad 41049:0edd245892ed
    53     Subset |
    53     Subset |
    54     DefEq |
    54     DefEq |
    55     Eq |
    55     Eq |
    56     Triad |
    56     Triad |
    57     Composition |
    57     Composition |
    58     Image |
       
    59     Apply |
    58     Apply |
    60     Lambda
    59     Lambda
    61 
    60 
    62   datatype op3 =
    61   datatype op3 =
    63     Let |
    62     Let |
   167   Subset |
   166   Subset |
   168   DefEq |
   167   DefEq |
   169   Eq |
   168   Eq |
   170   Triad |
   169   Triad |
   171   Composition |
   170   Composition |
   172   Image |
       
   173   Apply |
   171   Apply |
   174   Lambda
   172   Lambda
   175 
   173 
   176 datatype op3 =
   174 datatype op3 =
   177   Let |
   175   Let |
   231   | string_for_op2 Subset = "Subset"
   229   | string_for_op2 Subset = "Subset"
   232   | string_for_op2 DefEq = "DefEq"
   230   | string_for_op2 DefEq = "DefEq"
   233   | string_for_op2 Eq = "Eq"
   231   | string_for_op2 Eq = "Eq"
   234   | string_for_op2 Triad = "Triad"
   232   | string_for_op2 Triad = "Triad"
   235   | string_for_op2 Composition = "Composition"
   233   | string_for_op2 Composition = "Composition"
   236   | string_for_op2 Image = "Image"
       
   237   | string_for_op2 Apply = "Apply"
   234   | string_for_op2 Apply = "Apply"
   238   | string_for_op2 Lambda = "Lambda"
   235   | string_for_op2 Lambda = "Lambda"
   239 
   236 
   240 fun string_for_op3 Let = "Let"
   237 fun string_for_op3 Let = "Let"
   241   | string_for_op3 If = "If"
   238   | string_for_op3 If = "If"
   523           Op1 (Converse, range_type T, Any, sub t1)
   520           Op1 (Converse, range_type T, Any, sub t1)
   524         | (Const (@{const_name trancl}, T), [t1]) =>
   521         | (Const (@{const_name trancl}, T), [t1]) =>
   525           Op1 (Closure, range_type T, Any, sub t1)
   522           Op1 (Closure, range_type T, Any, sub t1)
   526         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   523         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   527           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   524           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   528         | (Const (@{const_name image}, T), [t1, t2]) =>
       
   529           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
       
   530         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   525         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   531           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   526           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   532           else if is_constr ctxt stds x then do_construct x []
   527           else if is_constr ctxt stds x then do_construct x []
   533           else ConstName (s, T, Any)
   528           else ConstName (s, T, Any)
   534         | (Const (@{const_name finite}, T), [t1]) =>
   529         | (Const (@{const_name finite}, T), [t1]) =>
   934               | (false, false) => non_opt_case ()
   929               | (false, false) => non_opt_case ()
   935             else
   930             else
   936               Cst (False, T, Formula Pos)
   931               Cst (False, T, Formula Pos)
   937               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
   932               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
   938           end
   933           end
   939         | Op2 (Image, T, _, u1, u2) =>
       
   940           let
       
   941             val u1' = sub u1
       
   942             val u2' = sub u2
       
   943           in
       
   944             (case (rep_of u1', rep_of u2') of
       
   945                (Func (R11, R12), Func (R21, Formula Neut)) =>
       
   946                if R21 = R11 andalso is_lone_rep R12 then
       
   947                  let
       
   948                    val R =
       
   949                      best_non_opt_set_rep_for_type scope T
       
   950                      |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
       
   951                  in s_op2 Image T R u1' u2' end
       
   952                else
       
   953                  raise SAME ()
       
   954              | _ => raise SAME ())
       
   955             handle SAME () =>
       
   956                    let
       
   957                      val T1 = type_of u1
       
   958                      val dom_T = domain_type T1
       
   959                      val ran_T = range_type T1
       
   960                      val x_u = BoundName (~1, dom_T, Any, "image.x")
       
   961                      val y_u = BoundName (~2, ran_T, Any, "image.y")
       
   962                    in
       
   963                      Op2 (Lambda, T, Any, y_u,
       
   964                           Op2 (Exist, bool_T, Any, x_u,
       
   965                                Op2 (And, bool_T, Any,
       
   966                                     case u2 of
       
   967                                       Op2 (Lambda, _, _, u21, u22) =>
       
   968                                       if num_occurrences_in_nut u21 u22 = 0 then
       
   969                                         u22
       
   970                                       else
       
   971                                         Op2 (Apply, bool_T, Any, u2, x_u)
       
   972                                     | _ => Op2 (Apply, bool_T, Any, u2, x_u),
       
   973 
       
   974                                     Op2 (Eq, bool_T, Any, y_u,
       
   975                                          Op2 (Apply, ran_T, Any, u1, x_u)))))
       
   976                      |> sub
       
   977                    end
       
   978           end
       
   979         | Op2 (Apply, T, _, u1, u2) =>
   934         | Op2 (Apply, T, _, u1, u2) =>
   980           let
   935           let
   981             val u1 = sub u1
   936             val u1 = sub u1
   982             val u2 = sub u2
   937             val u2 = sub u2
   983             val T1 = type_of u1
   938             val T1 = type_of u1