clarified context;
authorwenzelm
Sun Jul 05 19:08:40 2015 +0200 (2015-07-05)
changeset 60646441e268564c7
parent 60645 2affe7e97a34
child 60647 54bc3517161e
clarified context;
src/FOLP/ex/Nat.thy
src/FOLP/simp.ML
     1.1 --- a/src/FOLP/ex/Nat.thy	Sun Jul 05 16:44:59 2015 +0200
     1.2 +++ b/src/FOLP/ex/Nat.thy	Sun Jul 05 19:08:40 2015 +0200
     1.3 @@ -89,19 +89,19 @@
     1.4  
     1.5  schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
     1.6  apply (rule_tac n = k in induct)
     1.7 -apply (tactic {* SIMP_TAC add_ss 1 *})
     1.8 -apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
     1.9 +apply (tactic {* SIMP_TAC @{context} add_ss 1 *})
    1.10 +apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *})
    1.11  done
    1.12  
    1.13  schematic_lemma add_0_right: "?p : m+0 = m"
    1.14  apply (rule_tac n = m in induct)
    1.15 -apply (tactic {* SIMP_TAC add_ss 1 *})
    1.16 -apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
    1.17 +apply (tactic {* SIMP_TAC @{context} add_ss 1 *})
    1.18 +apply (tactic {* ASM_SIMP_TAC @{context} add_ss 1 *})
    1.19  done
    1.20  
    1.21  schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
    1.22  apply (rule_tac n = m in induct)
    1.23 -apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
    1.24 +apply (tactic {* ALLGOALS (ASM_SIMP_TAC @{context} add_ss) *})
    1.25  done
    1.26  
    1.27  (*mk_typed_congs appears not to work with FOLP's version of subst*)
     2.1 --- a/src/FOLP/simp.ML	Sun Jul 05 16:44:59 2015 +0200
     2.2 +++ b/src/FOLP/simp.ML	Sun Jul 05 19:08:40 2015 +0200
     2.3 @@ -37,13 +37,13 @@
     2.4    val dest_ss   : simpset -> thm list * thm list
     2.5    val print_ss  : Proof.context -> simpset -> unit
     2.6    val setauto   : simpset * (int -> tactic) -> simpset
     2.7 -  val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
     2.8 -  val ASM_SIMP_TAC      : simpset -> int -> tactic
     2.9 +  val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
    2.10 +  val ASM_SIMP_TAC      : Proof.context -> simpset -> int -> tactic
    2.11    val CASE_TAC          : simpset -> int -> tactic
    2.12 -  val SIMP_CASE2_TAC    : simpset -> int -> tactic
    2.13 -  val SIMP_THM          : simpset -> thm -> thm
    2.14 -  val SIMP_TAC          : simpset -> int -> tactic
    2.15 -  val SIMP_CASE_TAC     : simpset -> int -> tactic
    2.16 +  val SIMP_CASE2_TAC    : Proof.context -> simpset -> int -> tactic
    2.17 +  val SIMP_THM          : Proof.context -> simpset -> thm -> thm
    2.18 +  val SIMP_TAC          : Proof.context -> simpset -> int -> tactic
    2.19 +  val SIMP_CASE_TAC     : Proof.context -> simpset -> int -> tactic
    2.20    val mk_congs          : theory -> string list -> thm list
    2.21    val mk_typed_congs    : theory -> (string * string) list -> thm list
    2.22  (* temporarily disabled:
    2.23 @@ -375,26 +375,25 @@
    2.24      in variants_abs (params, Logic.strip_assums_concl subgi) end;
    2.25  
    2.26  (*print lhs of conclusion of subgoal i*)
    2.27 -fun pr_goal_lhs i st =
    2.28 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
    2.29 -             (lhs_of (prepare_goal i st)));
    2.30 +fun pr_goal_lhs ctxt i st =
    2.31 +    writeln (Syntax.string_of_term ctxt (lhs_of (prepare_goal i st)));
    2.32  
    2.33  (*print conclusion of subgoal i*)
    2.34 -fun pr_goal_concl i st =
    2.35 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
    2.36 +fun pr_goal_concl ctxt i st =
    2.37 +    writeln (Syntax.string_of_term ctxt (prepare_goal i st))
    2.38  
    2.39  (*print subgoals i to j (inclusive)*)
    2.40 -fun pr_goals (i,j) st =
    2.41 +fun pr_goals ctxt (i,j) st =
    2.42      if i>j then ()
    2.43 -    else (pr_goal_concl i st;  pr_goals (i+1,j) st);
    2.44 +    else (pr_goal_concl ctxt i st;  pr_goals ctxt (i+1,j) st);
    2.45  
    2.46  (*Print rewrite for tracing; i=subgoal#, n=number of new subgoals,
    2.47    thm=old state, thm'=new state *)
    2.48 -fun pr_rew (i,n,thm,thm',not_asms) =
    2.49 +fun pr_rew ctxt (i,n,thm,thm',not_asms) =
    2.50      if !tracing
    2.51      then (if not_asms then () else writeln"Assumption used in";
    2.52 -          pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
    2.53 -          if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
    2.54 +          pr_goal_lhs ctxt i thm; writeln"->"; pr_goal_lhs ctxt (i+n) thm';
    2.55 +          if n>0 then (writeln"Conditions:"; pr_goals ctxt (i, i+n-1) thm')
    2.56            else ();
    2.57            writeln"" )
    2.58      else ();
    2.59 @@ -407,7 +406,8 @@
    2.60          strip_varify(t,n,Var(("?",length vs),T)::vs)
    2.61    | strip_varify  _  = [];
    2.62  
    2.63 -fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let
    2.64 +fun execute ctxt (ss,if_fl,auto_tac,cong_tac,net,i,thm) =
    2.65 +let
    2.66  
    2.67  fun simp_lhs(thm,ss,anet,ats,cs) =
    2.68      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    2.69 @@ -426,7 +426,7 @@
    2.70        are represented by rules, generalized over their parameters*)
    2.71  fun add_asms(ss,thm,a,anet,ats,cs) =
    2.72      let val As = strip_varify(nth_subgoal i thm, a, []);
    2.73 -        val thms = map (Thm.trivial o Thm.global_cterm_of(Thm.theory_of_thm thm)) As;
    2.74 +        val thms = map (Thm.trivial o Thm.cterm_of ctxt) As;
    2.75          val new_rws = maps mk_rew_rules thms;
    2.76          val rwrls = map mk_trans (maps mk_rew_rules thms);
    2.77          val anet' = fold_rev lhs_insert_thm rwrls anet;
    2.78 @@ -435,7 +435,7 @@
    2.79  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    2.80        SOME(thm',seq') =>
    2.81              let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm)
    2.82 -            in pr_rew(i,n,thm,thm',more);
    2.83 +            in pr_rew ctxt (i,n,thm,thm',more);
    2.84                 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
    2.85                 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
    2.86                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    2.87 @@ -451,7 +451,7 @@
    2.88      | NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    2.89                in if !tracing
    2.90                   then (writeln"*** Failed to prove precondition. Normal form:";
    2.91 -                       pr_goal_concl i thm;  writeln"")
    2.92 +                       pr_goal_concl ctxt i thm;  writeln"")
    2.93                   else ();
    2.94                   rew(seq,thm0,ss0,anet0,ats0,cs0,more)
    2.95                end;
    2.96 @@ -480,30 +480,30 @@
    2.97  in exec(ss, thm, Net.empty, [], []) end;
    2.98  
    2.99  
   2.100 -fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   2.101 +fun EXEC_TAC ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   2.102  let val cong_tac = net_tac cong_net
   2.103  in fn i =>
   2.104      (fn thm =>
   2.105       if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
   2.106 -     else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   2.107 +     else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   2.108      THEN TRY(auto_tac i)
   2.109  end;
   2.110  
   2.111 -val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
   2.112 -val SIMP_CASE_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   2.113 +fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false);
   2.114 +fun SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   2.115  
   2.116 -val ASM_SIMP_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
   2.117 -val ASM_SIMP_CASE_TAC = EXEC_TAC([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   2.118 +fun ASM_SIMP_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,REFL,STOP],false);
   2.119 +fun ASM_SIMP_CASE_TAC ctxt = EXEC_TAC ctxt ([ASMS(0),MK_EQ,SIMP_LHS,IF,REFL,STOP],false);
   2.120  
   2.121 -val SIMP_CASE2_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
   2.122 +fun SIMP_CASE2_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,IF,REFL,STOP],true);
   2.123  
   2.124 -fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   2.125 +fun REWRITE ctxt (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   2.126  let val cong_tac = net_tac cong_net
   2.127  in fn thm => let val state = thm RSN (2,red1)
   2.128 -             in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
   2.129 +             in execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,1,state) end
   2.130  end;
   2.131  
   2.132 -val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
   2.133 +fun SIMP_THM ctxt = REWRITE ctxt ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
   2.134  
   2.135  
   2.136  (* Compute Congruence rules for individual constants using the substition