src/HOLCF/Tools/pcpodef.ML
changeset 33678 2a2014cbb2a6
parent 33646 d2f3104ca3d2
child 33680 a47277e09012
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 15:29:48 2009 -0800
     1.3 @@ -87,6 +87,7 @@
     1.4        thy
     1.5        |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
     1.6            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
     1.7 +    (* transfer thms so that they will know about the new cpo instance *)
     1.8      val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
     1.9      fun make thm = Drule.standard (thm OF cpo_thms');
    1.10      val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
    1.11 @@ -152,7 +153,7 @@
    1.12  fun declare_type_name a =
    1.13    Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    1.14  
    1.15 -fun prepare prep_term _ name (t, vs, mx) raw_set opt_morphs thy =
    1.16 +fun prepare prep_term name (t, vs, mx) raw_set opt_morphs thy =
    1.17    let
    1.18      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
    1.19      val ctxt = ProofContext.init thy;
    1.20 @@ -167,7 +168,6 @@
    1.21      (*lhs*)
    1.22      val defS = Sign.defaultS thy;
    1.23      val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    1.24 -    val lhs_sorts = map snd lhs_tfrees;
    1.25      val tname = Binding.map_name (Syntax.type_name mx) t;
    1.26      val full_tname = Sign.full_name thy tname;
    1.27      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.28 @@ -175,7 +175,7 @@
    1.29      val morphs = opt_morphs
    1.30        |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
    1.31    in
    1.32 -    (newT, oldT, set, morphs, lhs_sorts)
    1.33 +    (newT, oldT, set, morphs)
    1.34    end
    1.35  
    1.36  fun add_podef def opt_name typ set opt_morphs tac thy =
    1.37 @@ -188,21 +188,20 @@
    1.38      val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
    1.39  
    1.40      val RepC = Const (Rep_name, newT --> oldT);
    1.41 -    val below_def = Logic.mk_equals (below_const newT,
    1.42 +    val below_eqn = Logic.mk_equals (below_const newT,
    1.43        Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
    1.44      val lthy3 = thy2
    1.45        |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
    1.46 -    val below_def' = Syntax.check_term lthy3 below_def;
    1.47 -    val ((_, (_, below_definition')), lthy4) = lthy3
    1.48 +    val ((_, (_, below_ldef)), lthy4) = lthy3
    1.49        |> Specification.definition (NONE,
    1.50 -          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
    1.51 +          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
    1.52      val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
    1.53 -    val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
    1.54 +    val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
    1.55      val thy5 = lthy4
    1.56        |> Class.prove_instantiation_instance
    1.57 -          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
    1.58 +          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1))
    1.59        |> LocalTheory.exit_global;
    1.60 -  in ((info, below_definition), thy5) end;
    1.61 +  in ((info, below_def), thy5) end;
    1.62  
    1.63  fun prepare_cpodef
    1.64        (prep_term: Proof.context -> 'a -> term)
    1.65 @@ -214,8 +213,8 @@
    1.66        (thy: theory)
    1.67      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
    1.68    let
    1.69 -    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
    1.70 -      prepare prep_term def name typ raw_set opt_morphs thy;
    1.71 +    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
    1.72 +      prepare prep_term name typ raw_set opt_morphs thy;
    1.73  
    1.74      val goal_nonempty =
    1.75        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
    1.76 @@ -247,8 +246,8 @@
    1.77        (thy: theory)
    1.78      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
    1.79    let
    1.80 -    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
    1.81 -      prepare prep_term def name typ raw_set opt_morphs thy;
    1.82 +    val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
    1.83 +      prepare prep_term name typ raw_set opt_morphs thy;
    1.84  
    1.85      val goal_UU_mem =
    1.86        HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));