modernized structure Context_Rules;
authorwenzelm
Sun Nov 01 15:44:26 2009 +0100 (2009-11-01)
changeset 33369470a7b233ee5
parent 33368 b1cf34f1855c
child 33370 69531a7b55b6
modernized structure Context_Rules;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/HOL/Tools/Function/function.ML
src/HOL/Tools/inductive.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/specification.ML
src/Tools/intuitionistic.ML
     1.1 --- a/src/FOL/IFOL.thy	Sun Nov 01 15:24:45 2009 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Sun Nov 01 15:44:26 2009 +0100
     1.3 @@ -646,7 +646,7 @@
     1.4    and [Pure.elim 2] = allE notE' impE'
     1.5    and [Pure.intro] = exI disjI2 disjI1
     1.6  
     1.7 -setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
     1.8 +setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
     1.9  
    1.10  
    1.11  lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
     2.1 --- a/src/HOL/HOL.thy	Sun Nov 01 15:24:45 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Sun Nov 01 15:44:26 2009 +0100
     2.3 @@ -853,7 +853,7 @@
     2.4        (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
     2.5  in
     2.6    Hypsubst.hypsubst_setup
     2.7 -  #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
     2.8 +  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
     2.9  end
    2.10  *}
    2.11  
     3.1 --- a/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:24:45 2009 +0100
     3.2 +++ b/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:44:26 2009 +0100
     3.3 @@ -159,11 +159,11 @@
     3.4      in
     3.5        lthy
     3.6        |> ProofContext.note_thmss ""
     3.7 -         [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
     3.8 +         [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
     3.9        |> ProofContext.note_thmss ""
    3.10 -         [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    3.11 +         [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    3.12        |> ProofContext.note_thmss ""
    3.13 -         [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
    3.14 +         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
    3.15             [([Goal.norm_result termination], [])])] |> snd
    3.16        |> Proof.theorem_i NONE afterqed [[(goal, [])]]
    3.17      end
     4.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 01 15:24:45 2009 +0100
     4.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 01 15:44:26 2009 +0100
     4.3 @@ -708,7 +708,7 @@
     4.4        LocalTheory.notes kind
     4.5          (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
     4.6            map (fn th => [([th],
     4.7 -           [Attrib.internal (K (ContextRules.intro_query NONE)),
     4.8 +           [Attrib.internal (K (Context_Rules.intro_query NONE)),
     4.9              Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
    4.10        map (hd o snd);
    4.11      val (((_, elims'), (_, [induct'])), ctxt2) =
    4.12 @@ -719,7 +719,7 @@
    4.13            [Attrib.internal (K (Rule_Cases.case_names cases)),
    4.14             Attrib.internal (K (Rule_Cases.consumes 1)),
    4.15             Attrib.internal (K (Induct.cases_pred name)),
    4.16 -           Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    4.17 +           Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
    4.18          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    4.19        LocalTheory.note kind
    4.20          ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
     5.1 --- a/src/Provers/blast.ML	Sun Nov 01 15:24:45 2009 +0100
     5.2 +++ b/src/Provers/blast.ML	Sun Nov 01 15:44:26 2009 +0100
     5.3 @@ -55,7 +55,7 @@
     5.4                   swrappers: (string * wrapper) list,
     5.5                   uwrappers: (string * wrapper) list,
     5.6                   safe0_netpair: netpair, safep_netpair: netpair,
     5.7 -                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
     5.8 +                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
     5.9    val cla_modifiers: Method.modifier parser list
    5.10    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    5.11  end;
     6.1 --- a/src/Provers/clasimp.ML	Sun Nov 01 15:24:45 2009 +0100
     6.2 +++ b/src/Provers/clasimp.ML	Sun Nov 01 15:44:26 2009 +0100
     6.3 @@ -139,9 +139,9 @@
     6.4  fun modifier att (x, ths) =
     6.5    fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
     6.6  
     6.7 -val addXIs = modifier (ContextRules.intro_query NONE);
     6.8 -val addXEs = modifier (ContextRules.elim_query NONE);
     6.9 -val delXs = modifier ContextRules.rule_del;
    6.10 +val addXIs = modifier (Context_Rules.intro_query NONE);
    6.11 +val addXEs = modifier (Context_Rules.elim_query NONE);
    6.12 +val delXs = modifier Context_Rules.rule_del;
    6.13  
    6.14  in
    6.15  
     7.1 --- a/src/Provers/classical.ML	Sun Nov 01 15:24:45 2009 +0100
     7.2 +++ b/src/Provers/classical.ML	Sun Nov 01 15:44:26 2009 +0100
     7.3 @@ -45,7 +45,7 @@
     7.4                   uwrappers: (string * wrapper) list,
     7.5                   safe0_netpair: netpair, safep_netpair: netpair,
     7.6                   haz_netpair: netpair, dup_netpair: netpair,
     7.7 -                 xtra_netpair: ContextRules.netpair}
     7.8 +                 xtra_netpair: Context_Rules.netpair}
     7.9    val merge_cs          : claset * claset -> claset
    7.10    val addDs             : claset * thm list -> claset
    7.11    val addEs             : claset * thm list -> claset
    7.12 @@ -224,7 +224,7 @@
    7.13           safep_netpair  : netpair,                 (*nets for >0 subgoals*)
    7.14           haz_netpair    : netpair,                 (*nets for unsafe rules*)
    7.15           dup_netpair    : netpair,                 (*nets for duplication*)
    7.16 -         xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
    7.17 +         xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
    7.18  
    7.19  (*Desired invariants are
    7.20          safe0_netpair = build safe0_brls,
    7.21 @@ -898,7 +898,7 @@
    7.22  fun haz_dest w = attrib (addE w o make_elim);
    7.23  val haz_elim = attrib o addE;
    7.24  val haz_intro = attrib o addI;
    7.25 -val rule_del = attrib delrule o ContextRules.rule_del;
    7.26 +val rule_del = attrib delrule o Context_Rules.rule_del;
    7.27  
    7.28  
    7.29  end;
    7.30 @@ -914,11 +914,11 @@
    7.31  val setup_attrs =
    7.32    Attrib.setup @{binding swapped} (Scan.succeed swapped)
    7.33      "classical swap of introduction rule" #>
    7.34 -  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
    7.35 +  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
    7.36      "declaration of Classical destruction rule" #>
    7.37 -  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
    7.38 +  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
    7.39      "declaration of Classical elimination rule" #>
    7.40 -  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
    7.41 +  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
    7.42      "declaration of Classical introduction rule" #>
    7.43    Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    7.44      "remove declaration of intro/elim/dest rule";
    7.45 @@ -931,9 +931,9 @@
    7.46  
    7.47  fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
    7.48    let
    7.49 -    val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
    7.50 +    val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
    7.51      val CS {xtra_netpair, ...} = claset_of ctxt;
    7.52 -    val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
    7.53 +    val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
    7.54      val rules = rules1 @ rules2 @ rules3 @ rules4;
    7.55      val ruleq = Drule.multi_resolves facts rules;
    7.56    in
     8.1 --- a/src/Pure/Isar/calculation.ML	Sun Nov 01 15:24:45 2009 +0100
     8.2 +++ b/src/Pure/Isar/calculation.ML	Sun Nov 01 15:44:26 2009 +0100
     8.3 @@ -71,10 +71,11 @@
     8.4  
     8.5  val sym_add =
     8.6    Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
     8.7 -  #> ContextRules.elim_query NONE;
     8.8 +  #> Context_Rules.elim_query NONE;
     8.9 +
    8.10  val sym_del =
    8.11    Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
    8.12 -  #> ContextRules.rule_del;
    8.13 +  #> Context_Rules.rule_del;
    8.14  
    8.15  
    8.16  (* symmetric *)
     9.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:24:45 2009 +0100
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:44:26 2009 +0100
     9.3 @@ -33,7 +33,7 @@
     9.4      attribute context_parser
     9.5  end;
     9.6  
     9.7 -structure ContextRules: CONTEXT_RULES =
     9.8 +structure Context_Rules: CONTEXT_RULES =
     9.9  struct
    9.10  
    9.11  
    10.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 01 15:24:45 2009 +0100
    10.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 01 15:44:26 2009 +0100
    10.3 @@ -371,7 +371,7 @@
    10.4      in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
    10.5  
    10.6  val print_rules = Toplevel.unknown_context o
    10.7 -  Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
    10.8 +  Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
    10.9  
   10.10  val print_trans_rules = Toplevel.unknown_context o
   10.11    Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
    11.1 --- a/src/Pure/Isar/method.ML	Sun Nov 01 15:24:45 2009 +0100
    11.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 01 15:44:26 2009 +0100
    11.3 @@ -240,7 +240,7 @@
    11.4    let
    11.5      val rules =
    11.6        if not (null arg_rules) then arg_rules
    11.7 -      else flat (ContextRules.find_rules false facts goal ctxt)
    11.8 +      else flat (Context_Rules.find_rules false facts goal ctxt)
    11.9    in trace ctxt rules; tac rules facts i end);
   11.10  
   11.11  fun meth tac x = METHOD (HEADGOAL o tac x);
    12.1 --- a/src/Pure/Isar/obtain.ML	Sun Nov 01 15:24:45 2009 +0100
    12.2 +++ b/src/Pure/Isar/obtain.ML	Sun Nov 01 15:44:26 2009 +0100
    12.3 @@ -157,7 +157,7 @@
    12.4      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    12.5      |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
    12.6      |> Proof.assume_i
    12.7 -      [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    12.8 +      [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
    12.9      |> `Proof.the_facts
   12.10      ||> Proof.chain_facts chain_facts
   12.11      ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
    13.1 --- a/src/Pure/Isar/specification.ML	Sun Nov 01 15:24:45 2009 +0100
    13.2 +++ b/src/Pure/Isar/specification.ML	Sun Nov 01 15:44:26 2009 +0100
    13.3 @@ -313,7 +313,7 @@
    13.4              ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
    13.5              ctxt' |> Variable.auto_fixes asm
    13.6              |> ProofContext.add_assms_i Assumption.assume_export
    13.7 -              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    13.8 +              [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
    13.9              |>> (fn [(_, [th])] => th)
   13.10            end;
   13.11  
    14.1 --- a/src/Tools/intuitionistic.ML	Sun Nov 01 15:24:45 2009 +0100
    14.2 +++ b/src/Tools/intuitionistic.ML	Sun Nov 01 15:44:26 2009 +0100
    14.3 @@ -25,18 +25,18 @@
    14.4  
    14.5  fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    14.6  
    14.7 -val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    14.8 +val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
    14.9  
   14.10  fun safe_step_tac ctxt =
   14.11 -  ContextRules.Swrap ctxt
   14.12 +  Context_Rules.Swrap ctxt
   14.13     (eq_assume_tac ORELSE'
   14.14 -    bires_tac true (ContextRules.netpair_bang ctxt));
   14.15 +    bires_tac true (Context_Rules.netpair_bang ctxt));
   14.16  
   14.17  fun unsafe_step_tac ctxt =
   14.18 -  ContextRules.wrap ctxt
   14.19 +  Context_Rules.wrap ctxt
   14.20     (assume_tac APPEND'
   14.21 -    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
   14.22 -    bires_tac false (ContextRules.netpair ctxt));
   14.23 +    bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
   14.24 +    bires_tac false (Context_Rules.netpair ctxt));
   14.25  
   14.26  fun step_tac ctxt i =
   14.27    REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
   14.28 @@ -75,13 +75,13 @@
   14.29      >> (pair (I: Proof.context -> Proof.context) o att);
   14.30  
   14.31  val modifiers =
   14.32 - [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
   14.33 -  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
   14.34 -  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
   14.35 -  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
   14.36 -  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
   14.37 -  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
   14.38 -  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
   14.39 + [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
   14.40 +  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
   14.41 +  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
   14.42 +  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
   14.43 +  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
   14.44 +  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
   14.45 +  Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
   14.46  
   14.47  in
   14.48