interface for unchecked definitions
authorhaftmann
Mon Dec 03 16:04:16 2007 +0100 (2007-12-03)
changeset 2551800d5cc16e891
parent 25517 36d710d1dbce
child 25519 8570745cb40b
interface for unchecked definitions
src/Pure/Isar/class.ML
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Dec 03 16:04:14 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 03 16:04:16 2007 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
     1.5    val conclude_instantiation: local_theory -> local_theory
     1.6  
     1.7 -  val overloaded_const: string * typ * mixfix -> theory -> term * theory
     1.8 +  val overloaded_const: string * typ -> theory -> term * theory
     1.9    val overloaded_def: string -> string * term -> theory -> thm * theory
    1.10    val instantiation_param: Proof.context -> string -> string option
    1.11    val confirm_declaration: string -> local_theory -> local_theory
    1.12 @@ -206,11 +206,8 @@
    1.13    PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
    1.14    #>> (fn [(_, [thm])] => thm);
    1.15  
    1.16 -fun overloaded_const (c, ty, mx) thy =
    1.17 +fun overloaded_const (c, ty) thy =
    1.18    let
    1.19 -    val _ = if mx <> NoSyn then
    1.20 -      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
    1.21 -      else ();
    1.22      val SOME class = AxClass.class_of_param thy c;
    1.23      val SOME tyco = inst_tyco thy (c, ty);
    1.24      val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
    1.25 @@ -221,7 +218,7 @@
    1.26      |> Sign.sticky_prefix name_inst
    1.27      |> Sign.no_base_names
    1.28      |> Sign.declare_const [] (c', ty', NoSyn)
    1.29 -    |-> (fn const' as Const (c'', _) => Thm.add_def true
    1.30 +    |-> (fn const' as Const (c'', _) => Thm.add_def false true
    1.31            (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
    1.32      #>> Thm.varifyT
    1.33      #-> (fn thm => add_inst (c, tyco) (c'', thm)
    1.34 @@ -241,7 +238,7 @@
    1.35        (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
    1.36    in
    1.37      thy
    1.38 -    |> Thm.add_def false (name', prop)
    1.39 +    |> Thm.add_def false false (name', prop)
    1.40      |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
    1.41    end;
    1.42  
    1.43 @@ -796,7 +793,7 @@
    1.44    in
    1.45      thy'
    1.46      |> Sign.declare_const pos (c, ty'', mx) |> snd
    1.47 -    |> Thm.add_def false (c, def_eq)
    1.48 +    |> Thm.add_def false false (c, def_eq)
    1.49      |>> Thm.symmetric
    1.50      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
    1.51            #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
    1.52 @@ -911,7 +908,6 @@
    1.53      explode #> scan_valids #> implode
    1.54    end;
    1.55  
    1.56 -
    1.57  fun init_instantiation arities thy =
    1.58    let
    1.59      val _ = if null arities then error "At least one arity must be given" else ();
    1.60 @@ -990,7 +986,7 @@
    1.61          |> Sign.sticky_prefix name_inst
    1.62          |> Sign.no_base_names
    1.63          |> Sign.declare_const [] (c', ty, NoSyn)
    1.64 -        |-> (fn const' as Const (c'', _) => Thm.add_def true
    1.65 +        |-> (fn const' as Const (c'', _) => Thm.add_def false true
    1.66                (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
    1.67          #>> Thm.varifyT
    1.68          #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
     2.1 --- a/src/Pure/more_thm.ML	Mon Dec 03 16:04:14 2007 +0100
     2.2 +++ b/src/Pure/more_thm.ML	Mon Dec 03 16:04:16 2007 +0100
     2.3 @@ -54,7 +54,7 @@
     2.4    val elim_implies: thm -> thm -> thm
     2.5    val unvarify: thm -> thm
     2.6    val add_axiom: term list -> bstring * term -> theory -> thm * theory
     2.7 -  val add_def: bool -> bstring * term -> theory -> thm * theory
     2.8 +  val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
     2.9  end;
    2.10  
    2.11  structure Thm: THM =
    2.12 @@ -264,7 +264,7 @@
    2.13      val thm = fold elim_implies prems axm;
    2.14    in (thm, thy') end;
    2.15  
    2.16 -fun add_def overloaded (name, prop) thy =
    2.17 +fun add_def unchecked overloaded (name, prop) thy =
    2.18    let
    2.19      val tfrees = rev (map TFree (Term.add_tfrees prop []));
    2.20      val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
    2.21 @@ -272,7 +272,7 @@
    2.22      val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
    2.23  
    2.24      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
    2.25 -    val thy' = Theory.add_defs_i false overloaded [(name, prop')] thy;
    2.26 +    val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
    2.27      val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    2.28      val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
    2.29    in (thm, thy') end;