avoid raw equality on type thm;
authorwenzelm
Thu May 11 19:19:31 2006 +0200 (2006-05-11)
changeset 196177cb4b67d4b97
parent 19616 2545e8ab59a5
child 19618 9050a3b01e62
avoid raw equality on type thm;
src/HOL/Integ/int_arith1.ML
src/HOL/Library/EfficientNat.thy
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/typedef_package.ML
src/Provers/order.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu May 11 19:15:16 2006 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu May 11 19:19:31 2006 +0200
     1.3 @@ -281,8 +281,8 @@
     1.4  
     1.5  (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
     1.6    during re-arrangement*)
     1.7 -val non_add_bin_simps = 
     1.8 -    bin_simps \\ [add_number_of_left, number_of_add RS sym];
     1.9 +val non_add_bin_simps =
    1.10 +  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
    1.11  
    1.12  (*To evaluate binary negations of coefficients*)
    1.13  val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Thu May 11 19:15:16 2006 +0200
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu May 11 19:19:31 2006 +0200
     2.3 @@ -208,7 +208,7 @@
     2.4              (Thm.forall_intr (cert v) th'))
     2.5          in
     2.6            remove_suc_clause thy (map (fn th''' =>
     2.7 -            if th''' = th then th'' else th''') thms)
     2.8 +            if (op = o pairself prop_of) (th''', th) then th'' else th''') thms)
     2.9          end
    2.10    end;
    2.11  
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 11 19:15:16 2006 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 11 19:19:31 2006 +0200
     3.3 @@ -131,10 +131,10 @@
     3.4  fun get_assoc_snds [] xs assocs= assocs
     3.5  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
     3.6  
     3.7 -fun add_if_not_inlist [] xs newlist = newlist
     3.8 -|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
     3.9 -                                      add_if_not_inlist ys xs (y::newlist)
    3.10 -                                        else add_if_not_inlist ys xs (newlist)
    3.11 +fun add_if_not_inlist eq [] xs newlist = newlist
    3.12 +|   add_if_not_inlist eq (y::ys) xs newlist =
    3.13 +    if not (member eq xs y) then add_if_not_inlist eq ys xs (y::newlist)
    3.14 +    else add_if_not_inlist eq ys xs newlist
    3.15  
    3.16  (*Flattens a list of list of strings to one string*)
    3.17  fun onestr ls = String.concat (map String.concat ls);
    3.18 @@ -245,9 +245,9 @@
    3.19       val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
    3.20  
    3.21       (* get list of extra axioms as thms with their variables *)
    3.22 -     val extra_metas = add_if_not_inlist metas ax_metas []
    3.23 +     val extra_metas = add_if_not_inlist Thm.eq_thm metas ax_metas []
    3.24       val extra_vars = map thm_vars extra_metas
    3.25 -     val extra_with_vars = if (not (extra_metas = []) ) 
    3.26 +     val extra_with_vars = if not (null extra_metas)
    3.27  			   then ListPair.zip (extra_metas,extra_vars)
    3.28  			   else []
    3.29   in
    3.30 @@ -339,7 +339,7 @@
    3.31        val num_cls_vars =  map (addvars vars) numcls_strs;
    3.32        val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
    3.33        
    3.34 -      val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars))
    3.35 +      val extra_nums = if not (null extra_with_vars) then (1 upto (length extra_with_vars))
    3.36                         else []
    3.37        val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
    3.38        val frees_str = "["^(thmvars_to_string frees "")^"]"
     4.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 19:15:16 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 19:19:31 2006 +0200
     4.3 @@ -108,7 +108,7 @@
     4.4    val empty = ("", Symtab.empty);
     4.5    val copy = I;
     4.6    val extend = I;
     4.7 -  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (op =) (tab1, tab2))
     4.8 +  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2))
     4.9  
    4.10    fun print _ _ = ();
    4.11  end);
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 19:15:16 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu May 11 19:19:31 2006 +0200
     5.3 @@ -162,8 +162,8 @@
     5.4  
     5.5  (* congruence rules *)
     5.6  
     5.7 -val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
     5.8 -val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
     5.9 +val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
    5.10 +val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
    5.11  
    5.12  
    5.13  (* setup *)
     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:15:16 2006 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu May 11 19:19:31 2006 +0200
     6.3 @@ -436,7 +436,7 @@
     6.4      (** add realizers to theory **)
     6.5  
     6.6      val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
     6.7 -      (#intrs ind_info, find_index_eq r intrs)) rs) rss);
     6.8 +      (#intrs ind_info, find_index (fn th => eq_thm (th, r)) intrs)) rs) rss);
     6.9      val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
    6.10      val thy5 = Extraction.add_realizers_i
    6.11        (map (mk_realizer thy4 vs params')
     7.1 --- a/src/HOL/Tools/res_atp.ML	Thu May 11 19:15:16 2006 +0200
     7.2 +++ b/src/HOL/Tools/res_atp.ML	Thu May 11 19:19:31 2006 +0200
     7.3 @@ -269,9 +269,7 @@
     7.4  
     7.5  fun cnf_hyps_thms ctxt = 
     7.6      let val ths = ProofContext.prems_of ctxt
     7.7 -    in
     7.8 -	ResClause.union_all (map ResAxioms.skolem_thm ths)
     7.9 -    end;
    7.10 +    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
    7.11  
    7.12  
    7.13  (**** write to files ****)
     8.1 --- a/src/HOL/Tools/typedef_package.ML	Thu May 11 19:15:16 2006 +0200
     8.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu May 11 19:19:31 2006 +0200
     8.3 @@ -72,6 +72,7 @@
     8.4  
     8.5  (* theory data *)
     8.6  
     8.7 +(* FIXME self-descriptive record type *)
     8.8  type typedef_info = (typ * typ * string * string) * (thm option * thm * thm);
     8.9  
    8.10  structure TypedefData = TheoryDataFun
    8.11 @@ -81,7 +82,7 @@
    8.12    val empty = Symtab.empty;
    8.13    val copy = I;
    8.14    val extend = I;
    8.15 -  fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
    8.16 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
    8.17    fun print _ _ = ();
    8.18  end);
    8.19  
     9.1 --- a/src/Provers/order.ML	Thu May 11 19:15:16 2006 +0200
     9.2 +++ b/src/Provers/order.ML	Thu May 11 19:19:31 2006 +0200
     9.3 @@ -734,7 +734,7 @@
     9.4  in
     9.5    (* looking for x <= y: any path from x to y is sufficient *)
     9.6    case subgoal of (Le (x, y, _)) => (
     9.7 -  if sccGraph = [] then raise Cannot else ( 
     9.8 +  if null sccGraph then raise Cannot else ( 
     9.9     let 
    9.10      val xi = getIndex x ntc
    9.11      val yi = getIndex y ntc
    9.12 @@ -758,7 +758,7 @@
    9.13   (* looking for x < y: particular path required, which is not necessarily
    9.14      found by normal dfs *)
    9.15   |   (Less (x, y, _)) => (
    9.16 -  if sccGraph = [] then raise Cannot else (
    9.17 +  if null sccGraph then raise Cannot else (
    9.18     let 
    9.19      val xi = getIndex x ntc
    9.20      val yi = getIndex y ntc
    9.21 @@ -780,9 +780,9 @@
    9.22   )
    9.23  | (NotEq (x, y, _)) => (
    9.24    (* if there aren't any edges that are candidate for a ~= raise Cannot *)
    9.25 -  if neqE = [] then raise Cannot
    9.26 +  if null neqE then raise Cannot
    9.27    (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
    9.28 -  else if sccSubgraphs = [] then (
    9.29 +  else if null sccSubgraphs then (
    9.30       (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
    9.31         ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
    9.32            if  (x aconv x' andalso y aconv y') then p