src/FOLP/simp.ML
changeset 60646 441e268564c7
parent 60645 2affe7e97a34
child 60754 02924903a6fd
     1.1 --- a/src/FOLP/simp.ML	Sun Jul 05 16:44:59 2015 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sun Jul 05 19:08:40 2015 +0200
     1.3 @@ -37,13 +37,13 @@
     1.4    val dest_ss   : simpset -> thm list * thm list
     1.5    val print_ss  : Proof.context -> simpset -> unit
     1.6    val setauto   : simpset * (int -> tactic) -> simpset
     1.7 -  val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
     1.8 -  val ASM_SIMP_TAC      : simpset -> int -> tactic
     1.9 +  val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
    1.10 +  val ASM_SIMP_TAC      : Proof.context -> simpset -> int -> tactic
    1.11    val CASE_TAC          : simpset -> int -> tactic
    1.12 -  val SIMP_CASE2_TAC    : simpset -> int -> tactic
    1.13 -  val SIMP_THM          : simpset -> thm -> thm
    1.14 -  val SIMP_TAC          : simpset -> int -> tactic
    1.15 -  val SIMP_CASE_TAC     : simpset -> int -> tactic
    1.16 +  val SIMP_CASE2_TAC    : Proof.context -> simpset -> int -> tactic
    1.17 +  val SIMP_THM          : Proof.context -> simpset -> thm -> thm
    1.18 +  val SIMP_TAC          : Proof.context -> simpset -> int -> tactic
    1.19 +  val SIMP_CASE_TAC     : Proof.context -> simpset -> int -> tactic
    1.20    val mk_congs          : theory -> string list -> thm list
    1.21    val mk_typed_congs    : theory -> (string * string) list -> thm list
    1.22  (* temporarily disabled:
    1.23 @@ -375,26 +375,25 @@
    1.24      in variants_abs (params, Logic.strip_assums_concl subgi) end;
    1.25  
    1.26  (*print lhs of conclusion of subgoal i*)
    1.27 -fun pr_goal_lhs i st =
    1.28 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
    1.29 -             (lhs_of (prepare_goal i st)));
    1.30 +fun pr_goal_lhs ctxt i st =
    1.31 +    writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st)));
    1.32  
    1.33  (*print conclusion of subgoal i*)
    1.34 -fun pr_goal_concl i st =
    1.35 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
    1.36 +fun pr_goal_concl ctxt i st =
    1.37 +    writeln (Syntax.string_of_term ctxt (prepare_goal i st))
    1.38  
    1.39  (*print subgoals i to j (inclusive)*)
    1.40 -fun pr_goals (i,j) st =
    1.41 +fun pr_goals ctxt (i,j) st =
    1.42      if i>j then ()
    1.43 -    else (pr_goal_concl i st;  pr_goals (i+1,j) st);
    1.44 +    else (pr_goal_concl ctxt i st;  pr_goals ctxt (i+1,j) st);
    1.45  
    1.46  (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals,
    1.47    thm=old state, thm'=new state *)
    1.48 -fun pr_rew (i,n,thm,thm',not_asms) =
    1.49 +fun pr_rew ctxt (i,n,thm,thm',not_asms) =
    1.50      if !tracing
    1.51      then (if not_asms then () else writeln"Assumption used in";
    1.52 -          pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
    1.53 -          if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
    1.54 +          pr_goal_lhs ctxt i thm; writeln"->"; pr_goal_lhs ctxt (i+n) thm';
    1.55 +          if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n-1) thm')
    1.56            else ();
    1.57            writeln"" )
    1.58      else ();
    1.59 @@ -407,7 +406,8 @@
    1.60          strip_varify(t,n,Var(("?",length vs),T)::vs)
    1.61    | strip_varify  _  = [];
    1.62  
    1.63 -fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let
    1.64 +fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) =
    1.65 +let
    1.66  
    1.67  fun simp_lhs(thm,ss,anet,ats,cs) =
    1.68      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    1.69 @@ -426,7 +426,7 @@
    1.70        are represented by rules, generalized over their parameters*)
    1.71  fun add_asms(ss,thm,a,anet,ats,cs) =
    1.72      let val As = strip_varify(nth_subgoal i thm, a, []);
    1.73 -        val thms = map (Thm.trivial o Thm.global_cterm_of(Thm.theory_of_thm thm)) As;
    1.74 +        val thms = map (Thm.trivial o Thm.cterm_of ctxt) As;
    1.75          val new_rws = maps mk_rew_rules thms;
    1.76          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.77          val anet' = fold_rev lhs_insert_thm rwrls anet;
    1.78 @@ -435,7 +435,7 @@
    1.79  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    1.80        SOME(thm',seq') =>
    1.81              let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm)
    1.82 -            in pr_rew(i,n,thm,thm',more);
    1.83 +            in pr_rew ctxt (i,n,thm,thm',more);
    1.84                 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
    1.85                 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
    1.86                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    1.87 @@ -451,7 +451,7 @@
    1.88      | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    1.89                in if !tracing
    1.90                   then (writeln"*** Failed to prove precondition. Normal form:";
    1.91 -                       pr_goal_concl i thm;  writeln"")
    1.92 +                       pr_goal_concl ctxt i thm;  writeln"")
    1.93                   else ();
    1.94                   rew(seq,thm0,ss0,anet0,ats0,cs0,more)
    1.95                end;
    1.96 @@ -480,30 +480,30 @@
    1.97  in exec(ss, thm, Net.empty, [], []) end;
    1.98  
    1.99  
   1.100 -fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.101 +fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.102  let val cong_tac = net_tac cong_net
   1.103  in fn i =>
   1.104      (fn thm =>
   1.105       if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
   1.106 -     else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   1.107 +     else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   1.108      THEN TRY(auto_tac i)
   1.109  end;
   1.110  
   1.111 -val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
   1.112 -val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   1.113 +fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false);
   1.114 +fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   1.115  
   1.116 -val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
   1.117 -val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   1.118 +fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
   1.119 +fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   1.120  
   1.121 -val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
   1.122 +fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
   1.123  
   1.124 -fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.125 +fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.126  let val cong_tac = net_tac cong_net
   1.127  in fn thm => let val state = thm RSN (2,red1)
   1.128 -             in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
   1.129 +             in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end
   1.130  end;
   1.131  
   1.132 -val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
   1.133 +fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
   1.134  
   1.135  
   1.136  (* Compute Congruence rules for individual constants using the substition