normalized basic type abbreviations;
authorwenzelm
Tue Oct 27 17:34:00 2009 +0100 (2009-10-27 ago)
changeset 3324317014b1b9353
parent 33242 99577c7085c8
child 33244 db230399f890
normalized basic type abbreviations;
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/SMT/Tools/smt_normalize.ML
src/HOL/SMT/Tools/z3_proof.ML
src/HOL/SMT/Tools/z3_proof_rules.ML
src/HOL/SMT/Tools/z3_proof_terms.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_funcs.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Oct 27 17:19:31 2009 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Oct 27 17:34:00 2009 +0100
     1.3 @@ -28,8 +28,8 @@
     1.4    val goal_thm_of : Proof.state -> thm
     1.5    val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     1.6      Proof.state -> bool
     1.7 -  val theorems_in_proof_term : Thm.thm -> Thm.thm list
     1.8 -  val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
     1.9 +  val theorems_in_proof_term : thm -> thm list
    1.10 +  val theorems_of_sucessful_proof : Toplevel.state option -> thm list
    1.11    val get_setting : (string * string) list -> string * string -> string
    1.12    val get_int_setting : (string * string) list -> string * int -> int
    1.13    val cpu_time : ('a -> 'b) -> 'a -> 'b * int
     2.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Tue Oct 27 17:19:31 2009 +0100
     2.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Tue Oct 27 17:34:00 2009 +0100
     2.3 @@ -14,8 +14,8 @@
     2.4  signature SMT_NORMALIZE =
     2.5  sig
     2.6    val normalize_rule: Proof.context -> thm -> thm
     2.7 -  val instantiate_free: Thm.cterm * Thm.cterm -> thm -> thm
     2.8 -  val discharge_definition: Thm.cterm -> thm -> thm
     2.9 +  val instantiate_free: cterm * cterm -> thm -> thm
    2.10 +  val discharge_definition: cterm -> thm -> thm
    2.11  
    2.12    val trivial_let: Proof.context -> thm list -> thm list
    2.13    val positive_numerals: Proof.context -> thm list -> thm list
    2.14 @@ -33,8 +33,7 @@
    2.15      AddFunUpdRules |
    2.16      AddAbsMinMaxRules
    2.17  
    2.18 -  val normalize: config list -> Proof.context -> thm list ->
    2.19 -    Thm.cterm list * thm list
    2.20 +  val normalize: config list -> Proof.context -> thm list -> cterm list * thm list
    2.21  
    2.22    val setup: theory -> theory
    2.23  end
     3.1 --- a/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 27 17:19:31 2009 +0100
     3.2 +++ b/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 27 17:34:00 2009 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4  
     3.5  datatype context = Context of {
     3.6    Ttab: typ Symtab.table,
     3.7 -  ttab: Thm.cterm Symtab.table,
     3.8 +  ttab: cterm Symtab.table,
     3.9    etab: T.preterm Inttab.table,
    3.10    ptab: R.proof Inttab.table,
    3.11    nctxt: Name.context }
     4.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 27 17:19:31 2009 +0100
     4.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 27 17:34:00 2009 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4  
     4.5    (*proof reconstruction*)
     4.6    type proof
     4.7 -  val make_proof: rule -> int list -> Thm.cterm * Thm.cterm list -> proof
     4.8 +  val make_proof: rule -> int list -> cterm * cterm list -> proof
     4.9    val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
    4.10      thm
    4.11  
    4.12 @@ -103,11 +103,11 @@
    4.13    Unproved of {
    4.14      rule: rule,
    4.15      subs: int list,
    4.16 -    prop: Thm.cterm,
    4.17 -    vars: Thm.cterm list } |
    4.18 +    prop: cterm,
    4.19 +    vars: cterm list } |
    4.20    Sequent of {
    4.21 -    hyps: Thm.cterm list,
    4.22 -    vars: Thm.cterm list,
    4.23 +    hyps: cterm list,
    4.24 +    vars: cterm list,
    4.25      thm: theorem }
    4.26  
    4.27  fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs}
     5.1 --- a/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 27 17:19:31 2009 +0100
     5.2 +++ b/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 27 17:34:00 2009 +0100
     5.3 @@ -6,15 +6,15 @@
     5.4  
     5.5  signature Z3_PROOF_TERMS =
     5.6  sig
     5.7 -  val mk_prop: Thm.cterm -> Thm.cterm
     5.8 -  val mk_meta_eq: Thm.cterm -> Thm.cterm -> Thm.cterm
     5.9 +  val mk_prop: cterm -> cterm
    5.10 +  val mk_meta_eq: cterm -> cterm -> cterm
    5.11  
    5.12    type preterm
    5.13  
    5.14 -  val compile: theory -> Name.context -> preterm -> Thm.cterm * Thm.cterm list
    5.15 +  val compile: theory -> Name.context -> preterm -> cterm * cterm list
    5.16  
    5.17    val mk_bound: theory -> int -> typ -> preterm
    5.18 -  val mk_fun: Thm.cterm -> preterm list -> preterm
    5.19 +  val mk_fun: cterm -> preterm list -> preterm
    5.20    val mk_forall: theory -> string * typ -> preterm -> preterm
    5.21    val mk_exists: theory -> string * typ -> preterm -> preterm
    5.22  
    5.23 @@ -73,8 +73,8 @@
    5.24  
    5.25  
    5.26  datatype preterm = Preterm of {
    5.27 -  cterm: Thm.cterm,
    5.28 -  vars: (int * Thm.cterm) list }
    5.29 +  cterm: cterm,
    5.30 +  vars: (int * cterm) list }
    5.31  
    5.32  fun mk_preterm (ct, vs) = Preterm {cterm=ct, vars=vs}
    5.33  fun dest_preterm (Preterm {cterm, vars}) = (cterm, vars)
     6.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:19:31 2009 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:34:00 2009 +0100
     6.3 @@ -74,7 +74,7 @@
     6.4    val get_rec_types : descr -> (string * sort) list -> typ list
     6.5    val interpret_construction : descr -> (string * sort) list
     6.6      -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
     6.7 -    -> ((string * Term.typ list) * (string * 'a list) list) list
     6.8 +    -> ((string * typ list) * (string * 'a list) list) list
     6.9    val check_nonempty : descr list -> unit
    6.10    val unfold_datatypes : 
    6.11      theory -> descr -> (string * sort) list -> info Symtab.table ->
     7.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Oct 27 17:19:31 2009 +0100
     7.2 +++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 27 17:34:00 2009 +0100
     7.3 @@ -589,7 +589,7 @@
     7.4  (* ------------------------------------------------------------------------- *)
     7.5  
     7.6  type logic_map =
     7.7 -  {axioms : (Metis.Thm.thm * Thm.thm) list,
     7.8 +  {axioms : (Metis.Thm.thm * thm) list,
     7.9     tfrees : ResClause.type_literal list};
    7.10  
    7.11  fun const_in_metis c (pred, tm_list) =
     8.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:19:31 2009 +0100
     8.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:34:00 2009 +0100
     8.3 @@ -37,9 +37,9 @@
     8.4  	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
     8.5  
     8.6  	(* propositional representation of HOL terms *)
     8.7 -	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
     8.8 +	val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table
     8.9  	(* HOL term representation of propositional formulae *)
    8.10 -	val term_of_prop_formula : prop_formula -> Term.term
    8.11 +	val term_of_prop_formula : prop_formula -> term
    8.12  end;
    8.13  
    8.14  structure PropLogic : PROP_LOGIC =
     9.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 27 17:19:31 2009 +0100
     9.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 27 17:34:00 2009 +0100
     9.3 @@ -8,7 +8,7 @@
     9.4    type seed = Random_Engine.seed
     9.5    val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     9.6      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     9.7 -    -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
     9.8 +    -> seed -> (('a -> 'b) * (unit -> term)) * seed
     9.9    val ensure_random_typecopy: string -> theory -> theory
    9.10    val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
    9.11    val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
    10.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 27 17:19:31 2009 +0100
    10.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 27 17:34:00 2009 +0100
    10.3 @@ -25,16 +25,15 @@
    10.4  
    10.5    exception MAXVARS_EXCEEDED
    10.6  
    10.7 -  val add_interpreter : string -> (theory -> model -> arguments -> Term.term ->
    10.8 +  val add_interpreter : string -> (theory -> model -> arguments -> term ->
    10.9      (interpretation * model * arguments) option) -> theory -> theory
   10.10 -  val add_printer     : string -> (theory -> model -> Term.typ ->
   10.11 -    interpretation -> (int -> bool) -> Term.term option) -> theory -> theory
   10.12 +  val add_printer     : string -> (theory -> model -> typ ->
   10.13 +    interpretation -> (int -> bool) -> term option) -> theory -> theory
   10.14  
   10.15 -  val interpret : theory -> model -> arguments -> Term.term ->
   10.16 +  val interpret : theory -> model -> arguments -> term ->
   10.17      (interpretation * model * arguments)
   10.18  
   10.19 -  val print       : theory -> model -> Term.typ -> interpretation ->
   10.20 -    (int -> bool) -> Term.term
   10.21 +  val print       : theory -> model -> typ -> interpretation -> (int -> bool) -> term
   10.22    val print_model : theory -> model -> (int -> bool) -> string
   10.23  
   10.24  (* ------------------------------------------------------------------------- *)
   10.25 @@ -46,10 +45,10 @@
   10.26    val get_default_params : theory -> (string * string) list
   10.27    val actual_params      : theory -> (string * string) list -> params
   10.28  
   10.29 -  val find_model : theory -> params -> Term.term -> bool -> unit
   10.30 +  val find_model : theory -> params -> term -> bool -> unit
   10.31  
   10.32    (* tries to find a model for a formula: *)
   10.33 -  val satisfy_term   : theory -> (string * string) list -> Term.term -> unit
   10.34 +  val satisfy_term   : theory -> (string * string) list -> term -> unit
   10.35    (* tries to find a model that refutes a formula: *)
   10.36    val refute_term : theory -> (string * string) list -> term -> unit
   10.37    val refute_goal : theory -> (string * string) list -> thm -> int -> unit
   10.38 @@ -60,20 +59,18 @@
   10.39  (* Additional functions used by Nitpick (to be factored out)                 *)
   10.40  (* ------------------------------------------------------------------------- *)
   10.41  
   10.42 -  val close_form : Term.term -> Term.term
   10.43 -  val get_classdef : theory -> string -> (string * Term.term) option
   10.44 -  val norm_rhs : Term.term -> Term.term
   10.45 -  val get_def : theory -> string * Term.typ -> (string * Term.term) option
   10.46 -  val get_typedef : theory -> Term.typ -> (string * Term.term) option
   10.47 -  val is_IDT_constructor : theory -> string * Term.typ -> bool
   10.48 -  val is_IDT_recursor : theory -> string * Term.typ -> bool
   10.49 -  val is_const_of_class: theory -> string * Term.typ -> bool
   10.50 -  val monomorphic_term : Type.tyenv -> Term.term -> Term.term
   10.51 -  val specialize_type : theory -> (string * Term.typ) -> Term.term -> Term.term
   10.52 -  val string_of_typ : Term.typ -> string
   10.53 -  val typ_of_dtyp :
   10.54 -    Datatype.descr -> (Datatype.dtyp * Term.typ) list -> Datatype.dtyp
   10.55 -    -> Term.typ
   10.56 +  val close_form : term -> term
   10.57 +  val get_classdef : theory -> string -> (string * term) option
   10.58 +  val norm_rhs : term -> term
   10.59 +  val get_def : theory -> string * typ -> (string * term) option
   10.60 +  val get_typedef : theory -> typ -> (string * term) option
   10.61 +  val is_IDT_constructor : theory -> string * typ -> bool
   10.62 +  val is_IDT_recursor : theory -> string * typ -> bool
   10.63 +  val is_const_of_class: theory -> string * typ -> bool
   10.64 +  val monomorphic_term : Type.tyenv -> term -> term
   10.65 +  val specialize_type : theory -> (string * typ) -> term -> term
   10.66 +  val string_of_typ : typ -> string
   10.67 +  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
   10.68  end;  (* signature REFUTE *)
   10.69  
   10.70  structure Refute : REFUTE =
   10.71 @@ -185,7 +182,7 @@
   10.72  (* ------------------------------------------------------------------------- *)
   10.73  
   10.74    type model =
   10.75 -    (Term.typ * int) list * (Term.term * interpretation) list;
   10.76 +    (typ * int) list * (term * interpretation) list;
   10.77  
   10.78  (* ------------------------------------------------------------------------- *)
   10.79  (* arguments: additional arguments required during interpretation of terms   *)
   10.80 @@ -207,10 +204,10 @@
   10.81    structure RefuteData = TheoryDataFun
   10.82    (
   10.83      type T =
   10.84 -      {interpreters: (string * (theory -> model -> arguments -> Term.term ->
   10.85 +      {interpreters: (string * (theory -> model -> arguments -> term ->
   10.86          (interpretation * model * arguments) option)) list,
   10.87 -       printers: (string * (theory -> model -> Term.typ -> interpretation ->
   10.88 -        (int -> bool) -> Term.term option)) list,
   10.89 +       printers: (string * (theory -> model -> typ -> interpretation ->
   10.90 +        (int -> bool) -> term option)) list,
   10.91         parameters: string Symtab.table};
   10.92      val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   10.93      val copy = I;
    11.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 27 17:19:31 2009 +0100
    11.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 27 17:34:00 2009 +0100
    11.3 @@ -10,17 +10,17 @@
    11.4    val fix_sorts: sort Vartab.table -> term -> term
    11.5    val invert_const: string -> string
    11.6    val invert_type_const: string -> string
    11.7 -  val num_typargs: Context.theory -> string -> int
    11.8 +  val num_typargs: theory -> string -> int
    11.9    val make_tvar: string -> typ
   11.10    val strip_prefix: string -> string -> string option
   11.11 -  val setup: Context.theory -> Context.theory
   11.12 +  val setup: theory -> theory
   11.13    (* extracting lemma list*)
   11.14    val find_failure: string -> string option
   11.15    val lemma_list: bool -> string ->
   11.16 -    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
   11.17 +    string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   11.18    (* structured proofs *)
   11.19    val structured_proof: string ->
   11.20 -    string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
   11.21 +    string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   11.22  end;
   11.23  
   11.24  structure ResReconstruct : RES_RECONSTRUCT =
    12.1 --- a/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 17:19:31 2009 +0100
    12.2 +++ b/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 17:34:00 2009 +0100
    12.3 @@ -92,8 +92,8 @@
    12.4  (* ------------------------------------------------------------------------- *)
    12.5  
    12.6  datatype CLAUSE = NO_CLAUSE
    12.7 -                | ORIG_CLAUSE of Thm.thm
    12.8 -                | RAW_CLAUSE of Thm.thm * (int * Thm.cterm) list;
    12.9 +                | ORIG_CLAUSE of thm
   12.10 +                | RAW_CLAUSE of thm * (int * cterm) list;
   12.11  
   12.12  (* ------------------------------------------------------------------------- *)
   12.13  (* resolve_raw_clauses: given a non-empty list of raw clauses, we fold       *)
    13.1 --- a/src/Tools/eqsubst.ML	Tue Oct 27 17:19:31 2009 +0100
    13.2 +++ b/src/Tools/eqsubst.ML	Tue Oct 27 17:34:00 2009 +0100
    13.3 @@ -269,7 +269,7 @@
    13.4  (* FOR DEBUGGING...
    13.5  type trace_subst_errT = int (* subgoal *)
    13.6          * thm (* thm with all goals *)
    13.7 -        * (Thm.cterm list (* certified free var placeholders for vars *)
    13.8 +        * (cterm list (* certified free var placeholders for vars *)
    13.9             * thm)  (* trivial thm of goal concl *)
   13.10              (* possible matches/unifiers *)
   13.11          * thm (* rule *)