src/Provers/classical.ML
changeset 54742 7a86358a3c0b
parent 52732 b4da1f2ec73f
child 56334 6b3739fee456
     1.1 --- a/src/Provers/classical.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -166,7 +166,13 @@
     1.4    else rule;
     1.5  
     1.6  (*flatten nested meta connectives in prems*)
     1.7 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
     1.8 +fun flat_rule opt_context th =
     1.9 +  let
    1.10 +    val ctxt =
    1.11 +      (case opt_context of
    1.12 +        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
    1.13 +      | SOME context => Context.proof_of context);
    1.14 +  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
    1.15  
    1.16  
    1.17  (*** Useful tactics for classical reasoning ***)
    1.18 @@ -325,7 +331,7 @@
    1.19    if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
    1.20    else
    1.21      let
    1.22 -      val th' = flat_rule th;
    1.23 +      val th' = flat_rule context th;
    1.24        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.25          List.partition Thm.no_prems [th'];
    1.26        val nI = Item_Net.length safeIs + 1;
    1.27 @@ -354,7 +360,7 @@
    1.28      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
    1.29    else
    1.30      let
    1.31 -      val th' = classical_rule (flat_rule th);
    1.32 +      val th' = classical_rule (flat_rule context th);
    1.33        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.34          List.partition (fn rl => nprems_of rl=1) [th'];
    1.35        val nI = Item_Net.length safeIs;
    1.36 @@ -386,7 +392,7 @@
    1.37    if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
    1.38    else
    1.39      let
    1.40 -      val th' = flat_rule th;
    1.41 +      val th' = flat_rule context th;
    1.42        val nI = Item_Net.length hazIs + 1;
    1.43        val nE = Item_Net.length hazEs;
    1.44        val _ = warn_claset context th cs;
    1.45 @@ -415,7 +421,7 @@
    1.46      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
    1.47    else
    1.48      let
    1.49 -      val th' = classical_rule (flat_rule th);
    1.50 +      val th' = classical_rule (flat_rule context th);
    1.51        val nI = Item_Net.length hazIs;
    1.52        val nE = Item_Net.length hazEs + 1;
    1.53        val _ = warn_claset context th cs;
    1.54 @@ -443,12 +449,12 @@
    1.55          to insert.
    1.56  ***)
    1.57  
    1.58 -fun delSI th
    1.59 +fun delSI context th
    1.60      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.61        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.62    if Item_Net.member safeIs th then
    1.63      let
    1.64 -      val th' = flat_rule th;
    1.65 +      val th' = flat_rule context th;
    1.66        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
    1.67      in
    1.68        CS
    1.69 @@ -466,12 +472,12 @@
    1.70      end
    1.71    else cs;
    1.72  
    1.73 -fun delSE th
    1.74 +fun delSE context th
    1.75      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.76        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.77    if Item_Net.member safeEs th then
    1.78      let
    1.79 -      val th' = classical_rule (flat_rule th);
    1.80 +      val th' = classical_rule (flat_rule context th);
    1.81        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
    1.82      in
    1.83        CS
    1.84 @@ -493,7 +499,7 @@
    1.85      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.86        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.87    if Item_Net.member hazIs th then
    1.88 -    let val th' = flat_rule th in
    1.89 +    let val th' = flat_rule context th in
    1.90        CS
    1.91         {haz_netpair = delete ([th'], []) haz_netpair,
    1.92          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
    1.93 @@ -511,11 +517,11 @@
    1.94    handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
    1.95      error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
    1.96  
    1.97 -fun delE th
    1.98 +fun delE context th
    1.99      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.100        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.101    if Item_Net.member hazEs th then
   1.102 -    let val th' = classical_rule (flat_rule th) in
   1.103 +    let val th' = classical_rule (flat_rule context th) in
   1.104        CS
   1.105         {haz_netpair = delete ([], [th']) haz_netpair,
   1.106          dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   1.107 @@ -537,7 +543,11 @@
   1.108      if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
   1.109        Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
   1.110        Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
   1.111 -    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   1.112 +    then
   1.113 +      delSI context th
   1.114 +        (delSE context th
   1.115 +          (delI context th
   1.116 +            (delE context th (delSE context th' (delE context th' cs)))))
   1.117      else (warn_thm context "Undeclared classical rule\n" th; cs)
   1.118    end;
   1.119  
   1.120 @@ -774,24 +784,24 @@
   1.121  
   1.122  (*Dumb but fast*)
   1.123  fun fast_tac ctxt =
   1.124 -  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   1.125 +  Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   1.126  
   1.127  (*Slower but smarter than fast_tac*)
   1.128  fun best_tac ctxt =
   1.129 -  Object_Logic.atomize_prems_tac THEN'
   1.130 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.131    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
   1.132  
   1.133  (*even a bit smarter than best_tac*)
   1.134  fun first_best_tac ctxt =
   1.135 -  Object_Logic.atomize_prems_tac THEN'
   1.136 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.137    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
   1.138  
   1.139  fun slow_tac ctxt =
   1.140 -  Object_Logic.atomize_prems_tac THEN'
   1.141 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.142    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
   1.143  
   1.144  fun slow_best_tac ctxt =
   1.145 -  Object_Logic.atomize_prems_tac THEN'
   1.146 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.147    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
   1.148  
   1.149  
   1.150 @@ -800,13 +810,13 @@
   1.151  val weight_ASTAR = 5;
   1.152  
   1.153  fun astar_tac ctxt =
   1.154 -  Object_Logic.atomize_prems_tac THEN'
   1.155 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.156    SELECT_GOAL
   1.157      (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
   1.158        (step_tac ctxt 1));
   1.159  
   1.160  fun slow_astar_tac ctxt =
   1.161 -  Object_Logic.atomize_prems_tac THEN'
   1.162 +  Object_Logic.atomize_prems_tac ctxt THEN'
   1.163    SELECT_GOAL
   1.164      (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
   1.165        (slow_step_tac ctxt 1));
   1.166 @@ -901,12 +911,12 @@
   1.167    in
   1.168      fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   1.169    end)
   1.170 -  THEN_ALL_NEW Goal.norm_hhf_tac;
   1.171 +  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
   1.172  
   1.173  in
   1.174  
   1.175  fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   1.176 -  | rule_tac _ rules facts = Method.rule_tac rules facts;
   1.177 +  | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
   1.178  
   1.179  fun default_tac ctxt rules facts =
   1.180    HEADGOAL (rule_tac ctxt rules facts) ORELSE
   1.181 @@ -941,7 +951,7 @@
   1.182      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   1.183      "apply some intro/elim rule (potentially classical)" #>
   1.184    Method.setup @{binding contradiction}
   1.185 -    (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
   1.186 +    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
   1.187      "proof by contradiction" #>
   1.188    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
   1.189      "repeatedly apply safe steps" #>