eliminated Display.string_of_thm_without_context;
authorwenzelm
Wed Apr 20 22:57:29 2011 +0200 (2011-04-20)
changeset 424399efdd0af15ac
parent 42438 cf963c834435
child 42440 5e7a7343ab11
eliminated Display.string_of_thm_without_context;
tuned whitespace;
src/FOLP/classical.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/lin_arith.ML
src/Provers/classical.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/FOLP/classical.ML	Wed Apr 20 17:17:01 2011 +0200
     1.2 +++ b/src/FOLP/classical.ML	Wed Apr 20 22:57:29 2011 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    val addSDs: claset * thm list -> claset
     1.5    val addSEs: claset * thm list -> claset
     1.6    val addSIs: claset * thm list -> claset
     1.7 -  val print_cs: claset -> unit
     1.8 +  val print_cs: Proof.context -> claset -> unit
     1.9    val rep_cs: claset -> 
    1.10        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
    1.11         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
    1.12 @@ -122,12 +122,12 @@
    1.13  
    1.14  val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
    1.15  
    1.16 -fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
    1.17 +fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
    1.18    writeln (cat_lines
    1.19 -   (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
    1.20 -    ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
    1.21 -    ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
    1.22 -    ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
    1.23 +   (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
    1.24 +    ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
    1.25 +    ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
    1.26 +    ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
    1.27  
    1.28  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    1.29    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
     2.1 --- a/src/HOL/Tools/inductive.ML	Wed Apr 20 17:17:01 2011 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Apr 20 22:57:29 2011 +0200
     2.3 @@ -174,7 +174,7 @@
     2.4  val get_monos = #2 o get_inductives;
     2.5  val map_monos = InductiveData.map o apsnd;
     2.6  
     2.7 -fun mk_mono thm =
     2.8 +fun mk_mono ctxt thm =
     2.9    let
    2.10      fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
    2.11      fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    2.12 @@ -187,11 +187,15 @@
    2.13        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    2.14          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    2.15      | _ => thm
    2.16 -  end handle THM _ =>
    2.17 -    error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
    2.18 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
    2.19  
    2.20 -val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
    2.21 -val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
    2.22 +val mono_add =
    2.23 +  Thm.declaration_attribute (fn thm => fn context =>
    2.24 +    map_monos (Thm.add_thm (mk_mono (Context.proof_of context) thm)) context);
    2.25 +
    2.26 +val mono_del =
    2.27 +  Thm.declaration_attribute (fn thm => fn context =>
    2.28 +    map_monos (Thm.del_thm (mk_mono (Context.proof_of context) thm)) context);
    2.29  
    2.30  
    2.31  
    2.32 @@ -350,7 +354,7 @@
    2.33        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    2.34        REPEAT (FIRST
    2.35          [atac 1,
    2.36 -         resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
    2.37 +         resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
    2.38           etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
    2.39  
    2.40  
     3.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Apr 20 17:17:01 2011 +0200
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Apr 20 22:57:29 2011 +0200
     3.3 @@ -271,9 +271,9 @@
     3.4      val {discrete, inj_consts, ...} = get_arith_data ctxt
     3.5    in decomp_negation (thy, discrete, inj_consts) end;
     3.6  
     3.7 -fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
     3.8 +fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
     3.9    | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
    3.10 -  | domain_is_nat _                                                 = false;
    3.11 +  | domain_is_nat _ = false;
    3.12  
    3.13  
    3.14  (*---------------------------------------------------------------------------*)
    3.15 @@ -284,23 +284,25 @@
    3.16  
    3.17  (* checks if splitting with 'thm' is implemented                             *)
    3.18  
    3.19 -fun is_split_thm thm =
    3.20 -  case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
    3.21 +fun is_split_thm ctxt thm =
    3.22 +  (case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>
    3.23      (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
    3.24 -    case head_of lhs of
    3.25 -      Const (a, _) => member (op =) [@{const_name Orderings.max},
    3.26 -                                    @{const_name Orderings.min},
    3.27 -                                    @{const_name Groups.abs},
    3.28 -                                    @{const_name Groups.minus},
    3.29 -                                    "Int.nat" (*DYNAMIC BINDING!*),
    3.30 -                                    "Divides.div_class.mod" (*DYNAMIC BINDING!*),
    3.31 -                                    "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
    3.32 -    | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
    3.33 -                                 Display.string_of_thm_without_context thm);
    3.34 -                       false))
    3.35 -  | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
    3.36 -                   Display.string_of_thm_without_context thm);
    3.37 -          false);
    3.38 +    (case head_of lhs of
    3.39 +      Const (a, _) =>
    3.40 +        member (op =)
    3.41 +         [@{const_name Orderings.max},
    3.42 +          @{const_name Orderings.min},
    3.43 +          @{const_name Groups.abs},
    3.44 +          @{const_name Groups.minus},
    3.45 +          "Int.nat" (*DYNAMIC BINDING!*),
    3.46 +          "Divides.div_class.mod" (*DYNAMIC BINDING!*),
    3.47 +          "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
    3.48 +    | _ =>
    3.49 +      (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
    3.50 +        false))
    3.51 +  | _ =>
    3.52 +    (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm);
    3.53 +      false));
    3.54  
    3.55  (* substitute new for occurrences of old in a term, incrementing bound       *)
    3.56  (* variables as needed when substituting inside an abstraction               *)
    3.57 @@ -343,7 +345,7 @@
    3.58    fun REPEAT_DETERM_etac_rev_mp tms =
    3.59      fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
    3.60        HOLogic.false_const
    3.61 -  val split_thms  = filter is_split_thm (#splits (get_arith_data ctxt))
    3.62 +  val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
    3.63    val cmap        = Splitter.cmap_of_split_thms split_thms
    3.64    val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
    3.65    val splits      = Splitter.split_posns cmap thy Ts goal_tm
    3.66 @@ -645,13 +647,13 @@
    3.67  (* terms in the same way as filter_prems_tac does                            *)
    3.68  
    3.69  fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
    3.70 -let
    3.71 -  fun filter_prems t (left, right) =
    3.72 -    if p t then (left, right @ [t]) else (left @ right, [])
    3.73 -  val (left, right) = fold filter_prems terms ([], [])
    3.74 -in
    3.75 -  right @ left
    3.76 -end;
    3.77 +  let
    3.78 +    fun filter_prems t (left, right) =
    3.79 +      if p t then (left, right @ [t]) else (left @ right, [])
    3.80 +    val (left, right) = fold filter_prems terms ([], [])
    3.81 +  in
    3.82 +    right @ left
    3.83 +  end;
    3.84  
    3.85  (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
    3.86  (* subgoal that has 'terms' as premises                                      *)
    3.87 @@ -664,29 +666,27 @@
    3.88      terms;
    3.89  
    3.90  fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
    3.91 -let
    3.92 -  (* repeatedly split (including newly emerging subgoals) until no further   *)
    3.93 -  (* splitting is possible                                                   *)
    3.94 -  fun split_loop ([] : (typ list * term list) list) =
    3.95 -      ([] : (typ list * term list) list)
    3.96 -    | split_loop (subgoal::subgoals) =
    3.97 -      (case split_once_items ctxt subgoal of
    3.98 -        SOME new_subgoals => split_loop (new_subgoals @ subgoals)
    3.99 -      | NONE              => subgoal :: split_loop subgoals)
   3.100 -  fun is_relevant t  = is_some (decomp ctxt t)
   3.101 -  (* filter_prems_tac is_relevant: *)
   3.102 -  val relevant_terms = filter_prems_tac_items is_relevant terms
   3.103 -  (* split_tac, NNF normalization: *)
   3.104 -  val split_goals    = split_loop [(Ts, relevant_terms)]
   3.105 -  (* necessary because split_once_tac may normalize terms: *)
   3.106 -  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
   3.107 -    split_goals
   3.108 -  (* TRY (etac notE) THEN eq_assume_tac: *)
   3.109 -  val result         = filter_out (negated_term_occurs_positively o snd)
   3.110 -    beta_eta_norm
   3.111 -in
   3.112 -  result
   3.113 -end;
   3.114 +  let
   3.115 +    (* repeatedly split (including newly emerging subgoals) until no further   *)
   3.116 +    (* splitting is possible                                                   *)
   3.117 +    fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
   3.118 +      | split_loop (subgoal::subgoals) =
   3.119 +          (case split_once_items ctxt subgoal of
   3.120 +            SOME new_subgoals => split_loop (new_subgoals @ subgoals)
   3.121 +          | NONE => subgoal :: split_loop subgoals)
   3.122 +    fun is_relevant t  = is_some (decomp ctxt t)
   3.123 +    (* filter_prems_tac is_relevant: *)
   3.124 +    val relevant_terms = filter_prems_tac_items is_relevant terms
   3.125 +    (* split_tac, NNF normalization: *)
   3.126 +    val split_goals = split_loop [(Ts, relevant_terms)]
   3.127 +    (* necessary because split_once_tac may normalize terms: *)
   3.128 +    val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
   3.129 +      split_goals
   3.130 +    (* TRY (etac notE) THEN eq_assume_tac: *)
   3.131 +    val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm
   3.132 +  in
   3.133 +    result
   3.134 +  end;
   3.135  
   3.136  (* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
   3.137  (* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
   3.138 @@ -744,22 +744,22 @@
   3.139  (* contradiction (i.e., a term and its negation) in their premises.          *)
   3.140  
   3.141  fun pre_tac ss i =
   3.142 -let
   3.143 -  val ctxt = Simplifier.the_context ss;
   3.144 -  val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   3.145 -  fun is_relevant t = is_some (decomp ctxt t)
   3.146 -in
   3.147 -  DETERM (
   3.148 -    TRY (filter_prems_tac is_relevant i)
   3.149 -      THEN (
   3.150 -        (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
   3.151 -          THEN_ALL_NEW
   3.152 -            (CONVERSION Drule.beta_eta_conversion
   3.153 -              THEN'
   3.154 -            (TRY o (etac notE THEN' eq_assume_tac)))
   3.155 -      ) i
   3.156 -  )
   3.157 -end;
   3.158 +  let
   3.159 +    val ctxt = Simplifier.the_context ss;
   3.160 +    val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
   3.161 +    fun is_relevant t = is_some (decomp ctxt t)
   3.162 +  in
   3.163 +    DETERM (
   3.164 +      TRY (filter_prems_tac is_relevant i)
   3.165 +        THEN (
   3.166 +          (TRY o REPEAT_ALL_NEW (split_once_tac ss split_thms))
   3.167 +            THEN_ALL_NEW
   3.168 +              (CONVERSION Drule.beta_eta_conversion
   3.169 +                THEN'
   3.170 +              (TRY o (etac notE THEN' eq_assume_tac)))
   3.171 +        ) i
   3.172 +    )
   3.173 +  end;
   3.174  
   3.175  end;  (* LA_Data *)
   3.176  
   3.177 @@ -783,7 +783,8 @@
   3.178  
   3.179  val init_arith_data =
   3.180    Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
   3.181 -   {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @ @{thms add_mono_thms_linordered_field} @ add_mono_thms,
   3.182 +   {add_mono_thms = @{thms add_mono_thms_linordered_semiring} @
   3.183 +      @{thms add_mono_thms_linordered_field} @ add_mono_thms,
   3.184      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
   3.185        @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
   3.186      inj_thms = inj_thms,
   3.187 @@ -840,6 +841,7 @@
   3.188    fun prem_nnf_tac i st =
   3.189      full_simp_tac (Simplifier.global_context (Thm.theory_of_thm st) nnf_simpset) i st;
   3.190  in
   3.191 +
   3.192  fun refute_tac test prep_tac ref_tac =
   3.193    let val refute_prems_tac =
   3.194          REPEAT_DETERM
   3.195 @@ -852,6 +854,7 @@
   3.196              REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,
   3.197              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   3.198    end;
   3.199 +
   3.200  end;
   3.201  
   3.202  
     4.1 --- a/src/Provers/classical.ML	Wed Apr 20 17:17:01 2011 +0200
     4.2 +++ b/src/Provers/classical.ML	Wed Apr 20 22:57:29 2011 +0200
     4.3 @@ -37,7 +37,7 @@
     4.4  sig
     4.5    type claset
     4.6    val empty_cs: claset
     4.7 -  val print_cs: claset -> unit
     4.8 +  val print_cs: Proof.context -> claset -> unit
     4.9    val rep_cs:
    4.10      claset -> {safeIs: thm list, safeEs: thm list,
    4.11                   hazIs: thm list, hazEs: thm list,
    4.12 @@ -258,8 +258,8 @@
    4.13       dup_netpair   = empty_netpair,
    4.14       xtra_netpair  = empty_netpair};
    4.15  
    4.16 -fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    4.17 -  let val pretty_thms = map Display.pretty_thm_without_context in
    4.18 +fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    4.19 +  let val pretty_thms = map (Display.pretty_thm ctxt) in
    4.20      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
    4.21        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
    4.22        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
    4.23 @@ -1018,6 +1018,8 @@
    4.24    Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
    4.25      Keyword.diag
    4.26      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    4.27 -      Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
    4.28 +      Toplevel.keep (fn state =>
    4.29 +        let val ctxt = Toplevel.context_of state
    4.30 +        in print_cs ctxt (claset_of ctxt) end)));
    4.31  
    4.32  end;
     5.1 --- a/src/ZF/Tools/typechk.ML	Wed Apr 20 17:17:01 2011 +0200
     5.2 +++ b/src/ZF/Tools/typechk.ML	Wed Apr 20 22:57:29 2011 +0200
     5.3 @@ -25,20 +25,17 @@
     5.4   {rules: thm list,     (*the type-checking rules*)
     5.5    net: thm Net.net};   (*discrimination net of the same rules*)
     5.6  
     5.7 -fun add_rule th (tcs as TC {rules, net}) =
     5.8 +fun add_rule ctxt th (tcs as TC {rules, net}) =
     5.9    if member Thm.eq_thm_prop rules th then
    5.10 -    (warning ("Ignoring duplicate type-checking rule\n" ^
    5.11 -        Display.string_of_thm_without_context th); tcs)
    5.12 +    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
    5.13    else
    5.14 -    TC {rules = th :: rules,
    5.15 -        net = Net.insert_term (K false) (Thm.concl_of th, th) net};
    5.16 +    TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
    5.17  
    5.18 -fun del_rule th (tcs as TC {rules, net}) =
    5.19 +fun del_rule ctxt th (tcs as TC {rules, net}) =
    5.20    if member Thm.eq_thm_prop rules th then
    5.21      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
    5.22 -        rules = remove Thm.eq_thm_prop th rules}
    5.23 -  else (warning ("No such type-checking rule\n" ^
    5.24 -    Display.string_of_thm_without_context th); tcs);
    5.25 +      rules = remove Thm.eq_thm_prop th rules}
    5.26 +  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
    5.27  
    5.28  
    5.29  (* generic data *)
    5.30 @@ -52,8 +49,13 @@
    5.31      TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
    5.32  );
    5.33  
    5.34 -val TC_add = Thm.declaration_attribute (Data.map o add_rule);
    5.35 -val TC_del = Thm.declaration_attribute (Data.map o del_rule);
    5.36 +val TC_add =
    5.37 +  Thm.declaration_attribute (fn thm => fn context =>
    5.38 +    Data.map (add_rule (Context.proof_of context) thm) context);
    5.39 +
    5.40 +val TC_del =
    5.41 +  Thm.declaration_attribute (fn thm => fn context =>
    5.42 +    Data.map (del_rule (Context.proof_of context) thm) context);
    5.43  
    5.44  val tcset_of = Data.get o Context.Proof;
    5.45