just one HOLogic.mk_comp;
authorwenzelm
Wed Dec 01 15:35:40 2010 +0100 (2010-12-01)
changeset 4084515b97bd4b5c0
parent 40844 5895c525739d
child 40847 df8c7dc30214
just one HOLogic.mk_comp;
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/record.ML
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 15:03:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Dec 01 15:35:40 2010 +0100
     1.3 @@ -87,14 +87,6 @@
     1.4      Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
     1.5    end;
     1.6  
     1.7 -fun mk_fun_comp (t, u) =
     1.8 -  let
     1.9 -    val (_, B) = dest_funT (fastype_of t)
    1.10 -    val (C, A) = dest_funT (fastype_of u)
    1.11 -  in
    1.12 -    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
    1.13 -  end;
    1.14 -
    1.15  fun dest_randomT (Type ("fun", [@{typ Random.seed},
    1.16    Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    1.17    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
     2.1 --- a/src/HOL/Tools/hologic.ML	Wed Dec 01 15:03:44 2010 +0100
     2.2 +++ b/src/HOL/Tools/hologic.ML	Wed Dec 01 15:35:40 2010 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  sig
     2.5    val typeS: sort
     2.6    val typeT: typ
     2.7 +  val mk_comp: term * term -> term
     2.8    val boolN: string
     2.9    val boolT: typ
    2.10    val Trueprop: term
    2.11 @@ -142,6 +143,16 @@
    2.12  val typeT = Type_Infer.anyT typeS;
    2.13  
    2.14  
    2.15 +(* functions *)
    2.16 +
    2.17 +fun mk_comp (f, g) =
    2.18 +  let
    2.19 +    val fT = fastype_of f;
    2.20 +    val gT = fastype_of g;
    2.21 +    val compT = fT --> gT --> domain_type gT --> range_type fT;
    2.22 +  in Const ("Fun.comp", compT) $ f $ g end;
    2.23 +
    2.24 +
    2.25  (* bool and set *)
    2.26  
    2.27  val boolN = "HOL.bool";
     3.1 --- a/src/HOL/Tools/record.ML	Wed Dec 01 15:03:44 2010 +0100
     3.2 +++ b/src/HOL/Tools/record.ML	Wed Dec 01 15:35:40 2010 +0100
     3.3 @@ -1013,17 +1013,9 @@
     3.4      SOME u_name => u_name = s
     3.5    | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
     3.6  
     3.7 -fun mk_comp f g =
     3.8 -  let
     3.9 -    val X = fastype_of g;
    3.10 -    val (A, B) = dest_funT X;
    3.11 -    val C = range_type (fastype_of f);
    3.12 -    val T = (B --> C) --> (A --> B) --> A --> C;
    3.13 -  in Const (@{const_name Fun.comp}, T) $ f $ g end;
    3.14 -
    3.15  fun mk_comp_id f =
    3.16    let val T = range_type (fastype_of f)
    3.17 -  in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end;
    3.18 +  in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
    3.19  
    3.20  fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
    3.21    | get_upd_funs _ = [];
    3.22 @@ -1036,10 +1028,10 @@
    3.23        let
    3.24          (* FIXME fresh "f" (!?) *)
    3.25          val T = domain_type (fastype_of upd);
    3.26 -        val lhs = mk_comp acc (upd $ Free ("f", T));
    3.27 +        val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
    3.28          val rhs =
    3.29            if is_sel_upd_pair thy acc upd
    3.30 -          then mk_comp (Free ("f", T)) acc
    3.31 +          then HOLogic.mk_comp (Free ("f", T), acc)
    3.32            else mk_comp_id acc;
    3.33          val prop = lhs === rhs;
    3.34          val othm =
    3.35 @@ -1060,11 +1052,11 @@
    3.36      (* FIXME fresh "f" (!?) *)
    3.37      val f = Free ("f", domain_type (fastype_of u));
    3.38      val f' = Free ("f'", domain_type (fastype_of u'));
    3.39 -    val lhs = mk_comp (u $ f) (u' $ f');
    3.40 +    val lhs = HOLogic.mk_comp (u $ f, u' $ f');
    3.41      val rhs =
    3.42        if comp
    3.43 -      then u $ mk_comp f f'
    3.44 -      else mk_comp (u' $ f') (u $ f);
    3.45 +      then u $ HOLogic.mk_comp (f, f')
    3.46 +      else HOLogic.mk_comp (u' $ f', u $ f);
    3.47      val prop = lhs === rhs;
    3.48      val othm =
    3.49        Goal.prove (ProofContext.init_global thy) [] [] prop
     4.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:03:44 2010 +0100
     4.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 01 15:35:40 2010 +0100
     4.3 @@ -18,14 +18,6 @@
     4.4  
     4.5  (** general term functions **)
     4.6  
     4.7 -fun mk_fun_comp (t, u) =
     4.8 -  let
     4.9 -    val (_, B) = dest_funT (fastype_of t)
    4.10 -    val (C, A) = dest_funT (fastype_of u)
    4.11 -  in
    4.12 -    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
    4.13 -  end;
    4.14 -
    4.15  fun mk_measure f =
    4.16    let
    4.17      val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    4.18 @@ -136,7 +128,7 @@
    4.19    let
    4.20      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    4.21      val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
    4.22 -    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
    4.23 +    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
    4.24        Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    4.25      fun mk_termination_measure T =
    4.26        let