proper treatment of polymorphic sets;
authorwenzelm
Tue Sep 06 16:59:55 2005 +0200 (2005-09-06)
changeset 17280a6917ddc864f
parent 17279 7cd0099ae9bc
child 17281 3b9ff0131ed1
proper treatment of polymorphic sets;
tuned;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Sep 06 16:59:54 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Sep 06 16:59:55 2005 +0200
     1.3 @@ -61,9 +61,8 @@
     1.4    fun print _ _ = ();
     1.5  end);
     1.6  
     1.7 -fun put_typedef newT oldT Abs_name Rep_name thy =
     1.8 -  TypedefData.put (Symtab.curried_update_new
     1.9 -    (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)) (TypedefData.get thy)) thy;
    1.10 +fun put_typedef newT oldT Abs_name Rep_name =
    1.11 +  TypedefData.map (Symtab.curried_update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)));
    1.12  
    1.13  
    1.14  
    1.15 @@ -101,7 +100,7 @@
    1.16        witn1_tac THEN
    1.17        TRY (rewrite_goals_tac (List.filter is_def thms)) THEN
    1.18        TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.19 -      getOpt (witn2_tac, TRY (ALLGOALS (CLASET' blast_tac)));
    1.20 +      if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.21    in
    1.22      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.23      Tactic.prove thy [] [] goal (K tac)
    1.24 @@ -128,24 +127,29 @@
    1.25      val full_name = full name;
    1.26      val cset = prep_term thy vs raw_set;
    1.27      val {T = setT, t = set, ...} = Thm.rep_cterm cset;
    1.28 -    val rhs_tfrees = term_tfrees set;
    1.29 +    val rhs_tfrees = Term.add_tfrees set [];
    1.30 +    val rhs_tfreesT = Term.add_tfreesT setT [];
    1.31      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    1.32        error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT));
    1.33      fun mk_nonempty A =
    1.34        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    1.35      val goal = mk_nonempty set;
    1.36 -    val vname = take_suffix Symbol.is_digit (Symbol.explode name)
    1.37 -      |> apfst implode |> apsnd (#1 o Library.read_int);
    1.38 -    val goal_pat = mk_nonempty (Var (vname, setT));
    1.39 +    val goal_pat = mk_nonempty (Var (if_none (Syntax.read_variable name) (name, 0), setT));
    1.40  
    1.41      (*lhs*)
    1.42 -    val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs;
    1.43 +    val defS = Sign.defaultS thy;
    1.44 +    val lhs_tfrees = map (fn v => (v, if_none (AList.lookup (op =) rhs_tfrees v) defS)) vs;
    1.45 +    val args_setT = lhs_tfrees
    1.46 +      |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
    1.47 +      |> map TFree;
    1.48 +
    1.49      val tname = Syntax.type_name t mx;
    1.50      val full_tname = full tname;
    1.51      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.52  
    1.53 -    val (Rep_name, Abs_name) = getOpt (opt_morphs, ("Rep_" ^ name, "Abs_" ^ name));
    1.54 -    val setC = Const (full_name, setT);
    1.55 +    val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
    1.56 +    val setT' = map itselfT args_setT ---> setT;
    1.57 +    val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
    1.58      val RepC = Const (full Rep_name, newT --> oldT);
    1.59      val AbsC = Const (full Abs_name, oldT --> newT);
    1.60      val x_new = Free ("x", newT);
    1.61 @@ -164,7 +168,7 @@
    1.62        |> put_typedef newT oldT (full Abs_name) (full Rep_name)
    1.63        |> add_typedecls [(t, vs, mx)]
    1.64        |> Theory.add_consts_i
    1.65 -       ((if def then [(name, setT, NoSyn)] else []) @
    1.66 +       ((if def then [(name, setT', NoSyn)] else []) @
    1.67          [(Rep_name, newT --> oldT, NoSyn),
    1.68           (Abs_name, oldT --> newT, NoSyn)])
    1.69        |> (if def then (apsnd (SOME o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes))
    1.70 @@ -215,7 +219,7 @@
    1.71        | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
    1.72  
    1.73      val extra_rhs_tfrees =
    1.74 -      (case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => []
    1.75 +      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => []
    1.76        | extras => ["Extra type variables on rhs: " ^ show_names extras]);
    1.77  
    1.78      val illegal_frees =
    1.79 @@ -246,7 +250,7 @@
    1.80  
    1.81  fun sane_typedef prep_term def opt_name typ set opt_morphs tac =
    1.82    gen_typedef prep_term def
    1.83 -    (getOpt (opt_name, #1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
    1.84 +    (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
    1.85  
    1.86  fun add_typedef_x name typ set names thms tac =
    1.87    #1 o gen_typedef read_term true name typ set NONE (Tactic.rtac exI 1) names thms tac;
    1.88 @@ -307,7 +311,7 @@
    1.89        (case Symtab.curried_lookup (TypedefData.get thy) s of
    1.90           NONE => NONE
    1.91         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    1.92 -           if isSome (Codegen.get_assoc_type thy tname) then NONE else
    1.93 +           if is_some (Codegen.get_assoc_type thy tname) then NONE else
    1.94             let
    1.95               val module' = Codegen.if_library
    1.96                 (Codegen.thyname_of_type tname thy) module;
    1.97 @@ -383,7 +387,7 @@
    1.98      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    1.99  
   1.100  fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   1.101 -  typedef_proof ((def, getOpt (opt_name, Syntax.type_name t mx)), (t, vs, mx), A, morphs);
   1.102 +  typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
   1.103  
   1.104  val typedefP =
   1.105    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal