fix ML warnings in pcpodef.ML
authorhuffman
Mon Mar 22 14:11:13 2010 -0700 (2010-03-22)
changeset 3590281608655c69e
parent 35901 12f09bf2c77f
child 35903 0b43ff2d2e91
fix ML warnings in pcpodef.ML
src/HOLCF/Tools/pcpodef.ML
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 13:27:35 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 14:11:13 2010 -0700
     1.3 @@ -87,29 +87,32 @@
     1.4      val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
     1.5      val (full_tname, Ts) = dest_Type newT;
     1.6      val lhs_sorts = map (snd o dest_TFree) Ts;
     1.7 -    val thy2 =
     1.8 -      thy
     1.9 -      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
    1.10 -          (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
    1.11 +    val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1;
    1.12 +    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy;
    1.13      (* transfer thms so that they will know about the new cpo instance *)
    1.14 -    val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
    1.15 +    val cpo_thms' = map (Thm.transfer thy) cpo_thms;
    1.16      fun make thm = Drule.export_without_context (thm OF cpo_thms');
    1.17 -    val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
    1.18 -      thy2
    1.19 +    val cont_Rep = make @{thm typedef_cont_Rep};
    1.20 +    val cont_Abs = make @{thm typedef_cont_Abs};
    1.21 +    val lub = make @{thm typedef_lub};
    1.22 +    val thelub = make @{thm typedef_thelub};
    1.23 +    val compact = make @{thm typedef_compact};
    1.24 +    val (_, thy) =
    1.25 +      thy
    1.26        |> Sign.add_path (Binding.name_of name)
    1.27        |> PureThy.add_thms
    1.28 -        ([((Binding.prefix_name "adm_" name, admissible'), []),
    1.29 -          ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
    1.30 -          ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
    1.31 -          ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
    1.32 -          ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
    1.33 -          ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
    1.34 -      ||> Sign.restore_naming thy2;
    1.35 +        ([((Binding.prefix_name "adm_"      name, admissible'), []),
    1.36 +          ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
    1.37 +          ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
    1.38 +          ((Binding.prefix_name "lub_"      name, lub        ), []),
    1.39 +          ((Binding.prefix_name "thelub_"   name, thelub     ), []),
    1.40 +          ((Binding.prefix_name "compact_"  name, compact    ), [])])
    1.41 +      ||> Sign.parent_path;
    1.42      val cpo_info : cpo_info =
    1.43        { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
    1.44          cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
    1.45    in
    1.46 -    (cpo_info, thy3)
    1.47 +    (cpo_info, thy)
    1.48    end;
    1.49  
    1.50  fun prove_pcpo
    1.51 @@ -127,29 +130,33 @@
    1.52      val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
    1.53      val (full_tname, Ts) = dest_Type newT;
    1.54      val lhs_sorts = map (snd o dest_TFree) Ts;
    1.55 -    val thy2 = thy
    1.56 -      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
    1.57 -        (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
    1.58 -    val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
    1.59 +    val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1;
    1.60 +    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy;
    1.61 +    val pcpo_thms' = map (Thm.transfer thy) pcpo_thms;
    1.62      fun make thm = Drule.export_without_context (thm OF pcpo_thms');
    1.63 -    val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
    1.64 -          Rep_defined, Abs_defined], thy3) =
    1.65 -      thy2
    1.66 +    val Rep_strict = make @{thm typedef_Rep_strict};
    1.67 +    val Abs_strict = make @{thm typedef_Abs_strict};
    1.68 +    val Rep_strict_iff = make @{thm typedef_Rep_strict_iff};
    1.69 +    val Abs_strict_iff = make @{thm typedef_Abs_strict_iff};
    1.70 +    val Rep_defined = make @{thm typedef_Rep_defined};
    1.71 +    val Abs_defined = make @{thm typedef_Abs_defined};
    1.72 +    val (_, thy) =
    1.73 +      thy
    1.74        |> Sign.add_path (Binding.name_of name)
    1.75        |> PureThy.add_thms
    1.76 -        ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
    1.77 -          ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
    1.78 -          ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
    1.79 -          ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
    1.80 -          ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
    1.81 -          ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
    1.82 -      ||> Sign.restore_naming thy2;
    1.83 +        ([((Binding.suffix_name "_strict"     Rep_name, Rep_strict), []),
    1.84 +          ((Binding.suffix_name "_strict"     Abs_name, Abs_strict), []),
    1.85 +          ((Binding.suffix_name "_strict_iff" Rep_name, Rep_strict_iff), []),
    1.86 +          ((Binding.suffix_name "_strict_iff" Abs_name, Abs_strict_iff), []),
    1.87 +          ((Binding.suffix_name "_defined"    Rep_name, Rep_defined), []),
    1.88 +          ((Binding.suffix_name "_defined"    Abs_name, Abs_defined), [])])
    1.89 +      ||> Sign.parent_path;
    1.90      val pcpo_info =
    1.91        { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
    1.92          Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
    1.93          Rep_defined = Rep_defined, Abs_defined = Abs_defined };
    1.94    in
    1.95 -    (pcpo_info, thy3)
    1.96 +    (pcpo_info, thy)
    1.97    end;
    1.98  
    1.99  (* prepare_cpodef *)
   1.100 @@ -319,7 +326,8 @@
   1.101      val args = map (apsnd (prep_constraint ctxt)) raw_args;
   1.102      val (goal1, goal2, make_result) =
   1.103        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
   1.104 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   1.105 +    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
   1.106 +      | after_qed _ = error "cpodef_proof";
   1.107    in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   1.108  
   1.109  fun gen_pcpodef_proof prep_term prep_constraint
   1.110 @@ -329,7 +337,8 @@
   1.111      val args = map (apsnd (prep_constraint ctxt)) raw_args;
   1.112      val (goal1, goal2, make_result) =
   1.113        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
   1.114 -    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   1.115 +    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
   1.116 +      | after_qed _ = error "pcpodef_proof";
   1.117    in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   1.118  
   1.119  in