src/FOLP/simp.ML
changeset 60756 f122140b7195
parent 60754 02924903a6fd
child 60774 6c28d8ed2488
     1.1 --- a/src/FOLP/simp.ML	Sat Jul 18 20:59:51 2015 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Jul 18 21:25:55 2015 +0200
     1.3 @@ -73,14 +73,14 @@
     1.4  (*match subgoal i against possible theorems in the net.
     1.5    Similar to match_from_nat_tac, but the net does not contain numbers;
     1.6    rewrite rules are not ordered.*)
     1.7 -fun net_tac net =
     1.8 -  SUBGOAL(fn (prem,i) =>
     1.9 -          resolve0_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
    1.10 +fun net_tac ctxt net =
    1.11 +  SUBGOAL(fn (prem, i) =>
    1.12 +    resolve_tac ctxt (Net.unify_term net (Logic.strip_assums_concl prem)) i);
    1.13  
    1.14  (*match subgoal i against possible theorems indexed by lhs in the net*)
    1.15 -fun lhs_net_tac net =
    1.16 +fun lhs_net_tac ctxt net =
    1.17    SUBGOAL(fn (prem,i) =>
    1.18 -          biresolve0_tac (Net.unify_term net
    1.19 +          biresolve_tac ctxt (Net.unify_term net
    1.20                         (lhs_of (Logic.strip_assums_concl prem))) i);
    1.21  
    1.22  fun nth_subgoal i thm = nth (Thm.prems_of thm) (i - 1);
    1.23 @@ -119,7 +119,7 @@
    1.24  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    1.25          Const(s,_)$_ => member (op =) norms s | _ => false;
    1.26  
    1.27 -val refl_tac = resolve0_tac refl_thms;
    1.28 +fun refl_tac ctxt = resolve_tac ctxt refl_thms;
    1.29  
    1.30  fun find_res thms thm =
    1.31      let fun find [] = error "Check Simp_Data"
    1.32 @@ -138,7 +138,7 @@
    1.33          SOME(thm',_) => thm'
    1.34        | NONE => raise THM("Simplifier: could not continue", 0, [thm]);
    1.35  
    1.36 -fun res1(thm,thms,i) = one_result(resolve0_tac thms i,thm);
    1.37 +fun res1 ctxt (thm,thms,i) = one_result (resolve_tac ctxt thms i,thm);
    1.38  
    1.39  
    1.40  (**** Adding "NORM" tags ****)
    1.41 @@ -186,7 +186,7 @@
    1.42      in add_vars end;
    1.43  
    1.44  
    1.45 -fun add_norms(congs,ccs,new_asms) thm =
    1.46 +fun add_norms ctxt (congs,ccs,new_asms) thm =
    1.47  let val thm' = mk_trans2 thm;
    1.48  (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *)
    1.49      val nops = Thm.nprems_of thm'
    1.50 @@ -200,35 +200,34 @@
    1.51          else Misc_Legacy.add_term_frees(asm,hvars)
    1.52      val hvars = fold_rev it_asms asms hvars
    1.53      val hvs = map (#1 o dest_Var) hvars
    1.54 -    val refl1_tac = refl_tac 1
    1.55      fun norm_step_tac st = st |>
    1.56           (case head_of(rhs_of_eq 1 st) of
    1.57 -            Var(ixn,_) => if member (op =) hvs ixn then refl1_tac
    1.58 -                          else resolve0_tac normI_thms 1 ORELSE refl1_tac
    1.59 -          | Const _ => resolve0_tac normI_thms 1 ORELSE
    1.60 -                       resolve0_tac congs 1 ORELSE refl1_tac
    1.61 -          | Free _ => resolve0_tac congs 1 ORELSE refl1_tac
    1.62 -          | _ => refl1_tac)
    1.63 +            Var(ixn,_) => if member (op =) hvs ixn then refl_tac ctxt 1
    1.64 +                          else resolve_tac ctxt normI_thms 1 ORELSE refl_tac ctxt 1
    1.65 +          | Const _ => resolve_tac ctxt normI_thms 1 ORELSE
    1.66 +                       resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1
    1.67 +          | Free _ => resolve_tac ctxt congs 1 ORELSE refl_tac ctxt 1
    1.68 +          | _ => refl_tac ctxt 1)
    1.69      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    1.70      val SOME(thm'',_) = Seq.pull(add_norm_tac thm')
    1.71  in thm'' end;
    1.72  
    1.73 -fun add_norm_tags congs =
    1.74 +fun add_norm_tags ctxt congs =
    1.75      let val ccs = map cong_const congs
    1.76          val new_asms = filter (exists not o #2)
    1.77                  (ccs ~~ (map (map atomic o Thm.prems_of) congs));
    1.78 -    in add_norms(congs,ccs,new_asms) end;
    1.79 +    in add_norms ctxt (congs,ccs,new_asms) end;
    1.80  
    1.81 -fun normed_rews congs =
    1.82 +fun normed_rews ctxt congs =
    1.83    let
    1.84 -    val add_norms = add_norm_tags congs
    1.85 -    fun normed ctxt thm =
    1.86 +    val add_norms = add_norm_tags ctxt congs
    1.87 +    fun normed thm =
    1.88        let
    1.89          val ctxt' = Variable.declare_thm thm ctxt;
    1.90        in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end
    1.91    in normed end;
    1.92  
    1.93 -fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac];
    1.94 +fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac ctxt];
    1.95  
    1.96  val trans_norms = map mk_trans normE_thms;
    1.97  
    1.98 @@ -244,7 +243,7 @@
    1.99                 simp_net: thm Net.net}
   1.100  
   1.101  val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty,
   1.102 -                  mk_simps=normed_rews[], simps=[], simp_net=Net.empty};
   1.103 +                  mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty};
   1.104  
   1.105  (** Insertion of congruences and rewrites **)
   1.106  
   1.107 @@ -265,7 +264,7 @@
   1.108  let val congs' = thms @ congs;
   1.109  in SS{auto_tac=auto_tac, congs= congs',
   1.110        cong_net= insert_thms (map mk_trans thms) cong_net,
   1.111 -      mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   1.112 +      mk_simps = fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net}
   1.113  end;
   1.114  
   1.115  (** Deletion of congruences and rewrites **)
   1.116 @@ -281,7 +280,7 @@
   1.117  let val congs' = fold (remove Thm.eq_thm_prop) thms congs
   1.118  in SS{auto_tac=auto_tac, congs= congs',
   1.119        cong_net= delete_thms (map mk_trans thms) cong_net,
   1.120 -      mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   1.121 +      mk_simps= fn ctxt => normed_rews ctxt congs', simps=simps, simp_net=simp_net}
   1.122  end;
   1.123  
   1.124  fun delrew thm (SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}) =
   1.125 @@ -341,14 +340,15 @@
   1.126                  let val test = has_fewer_prems (Thm.nprems_of thm + 1)
   1.127                      fun loop thm =
   1.128                          COND test no_tac
   1.129 -                          ((try_rew THEN DEPTH_FIRST test (refl_tac i))
   1.130 -                           ORELSE (refl_tac i THEN loop)) thm
   1.131 +                          ((try_rew THEN DEPTH_FIRST test (refl_tac ctxt i))
   1.132 +                           ORELSE (refl_tac ctxt i THEN loop)) thm
   1.133                  in (cong_tac THEN loop) thm end
   1.134      in COND (may_match(case_consts,i)) try_rew no_tac end;
   1.135  
   1.136  fun CASE_TAC ctxt (SS{cong_net,...}) i =
   1.137 -let val cong_tac = net_tac cong_net i
   1.138 -in NORM ctxt (IF1_TAC ctxt cong_tac) i end;
   1.139 +  let val cong_tac = net_tac ctxt cong_net i
   1.140 +  in NORM ctxt (IF1_TAC ctxt cong_tac) i end;
   1.141 +
   1.142  
   1.143  (* Rewriting Automaton *)
   1.144  
   1.145 @@ -411,7 +411,7 @@
   1.146  
   1.147  fun simp_lhs(thm,ss,anet,ats,cs) =
   1.148      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
   1.149 -    if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
   1.150 +    if lhs_is_NORM(thm,i) then (ss, res1 ctxt (thm,trans_norms,i), anet,ats,cs)
   1.151      else case Seq.pull(cong_tac i thm) of
   1.152              SOME(thm',_) =>
   1.153                      let val ps = Thm.prems_of thm
   1.154 @@ -441,7 +441,7 @@
   1.155                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
   1.156              end
   1.157      | NONE => if more
   1.158 -            then rew((lhs_net_tac anet i THEN assume_tac ctxt i) thm,
   1.159 +            then rew((lhs_net_tac ctxt anet i THEN assume_tac ctxt i) thm,
   1.160                       thm,ss,anet,ats,cs,false)
   1.161              else (ss,thm,anet,ats,cs);
   1.162  
   1.163 @@ -462,12 +462,12 @@
   1.164                | NONE => (ss,thm,anet,ats,cs);
   1.165  
   1.166  fun step(s::ss, thm, anet, ats, cs) = case s of
   1.167 -          MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
   1.168 +          MK_EQ => (ss, res1 ctxt (thm,[red2],i), anet, ats, cs)
   1.169          | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
   1.170          | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
   1.171 -        | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
   1.172 -        | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
   1.173 -        | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
   1.174 +        | REW => rew(net_tac ctxt net i thm,thm,ss,anet,ats,cs,true)
   1.175 +        | REFL => (ss, res1 ctxt (thm,refl_thms,i), anet, ats, cs)
   1.176 +        | TRUE => try_true(res1 ctxt (thm,refl_thms,i),ss,anet,ats,cs)
   1.177          | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
   1.178                      else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
   1.179          | POP_ARTR => (ss,thm,hd ats,tl ats,cs)
   1.180 @@ -481,7 +481,7 @@
   1.181  
   1.182  
   1.183  fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.184 -let val cong_tac = net_tac cong_net
   1.185 +let val cong_tac = net_tac ctxt cong_net
   1.186  in fn i =>
   1.187      (fn thm =>
   1.188       if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
   1.189 @@ -498,7 +498,7 @@
   1.190  fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
   1.191  
   1.192  fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.193 -let val cong_tac = net_tac cong_net
   1.194 +let val cong_tac = net_tac ctxt cong_net
   1.195  in fn thm => let val state = thm RSN (2,red1)
   1.196               in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end
   1.197  end;