proper context for tactics derived from res_inst_tac;
authorwenzelm
Sat Jun 14 23:52:51 2008 +0200 (2008-06-14)
changeset 2722131328dc30196
parent 27220 31adee1f467a
child 27222 b08abdb8f499
proper context for tactics derived from res_inst_tac;
src/CCL/Wfd.thy
src/CCL/ex/Flag.thy
src/CCL/ex/List.thy
src/CCL/ex/Nat.thy
     1.1 --- a/src/CCL/Wfd.thy	Sat Jun 14 23:33:43 2008 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Sat Jun 14 23:52:51 2008 +0200
     1.3 @@ -421,18 +421,8 @@
     1.4  local
     1.5  
     1.6  val type_rls =
     1.7 -  thms "canTs" @ thms "icanTs" @ thms "applyT2" @ thms "ncanTs" @ thms "incanTs" @
     1.8 -  thms "precTs" @ thms "letrecTs" @ thms "letT" @ thms "Subtype_canTs";
     1.9 -
    1.10 -val rcallT = thm "rcallT";
    1.11 -val rcall2T = thm "rcall2T";
    1.12 -val rcall3T = thm "rcall3T";
    1.13 -val rcallTs = thms "rcallTs";
    1.14 -val rcall_lemmas = thms "rcall_lemmas";
    1.15 -val SubtypeE = thm "SubtypeE";
    1.16 -val SubtypeI = thm "SubtypeI";
    1.17 -val rmIHs = thms "rmIHs";
    1.18 -val hyprcallTs = thms "hyprcallTs";
    1.19 +  @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
    1.20 +  @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
    1.21  
    1.22  fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
    1.23    | bvars _ l = l
    1.24 @@ -445,9 +435,9 @@
    1.25    | get_bno l n (Bound m) = (m-length(l),n)
    1.26  
    1.27  (* Not a great way of identifying induction hypothesis! *)
    1.28 -fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse
    1.29 -                 could_unify(x,hd (prems_of rcall2T)) orelse
    1.30 -                 could_unify(x,hd (prems_of rcall3T))
    1.31 +fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
    1.32 +                 could_unify(x,hd (prems_of @{thm rcall2T})) orelse
    1.33 +                 could_unify(x,hd (prems_of @{thm rcall3T}))
    1.34  
    1.35  fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
    1.36    let val bvs = bvars Bi []
    1.37 @@ -456,7 +446,7 @@
    1.38                      let val (a,b) = get_bno [] 0 x
    1.39                      in (List.nth(bvs,a),b) end) ihs
    1.40        fun try_IHs [] = no_tac
    1.41 -        | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
    1.42 +        | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
    1.43    in try_IHs rnames end)
    1.44  
    1.45  fun is_rigid_prog t =
    1.46 @@ -465,35 +455,37 @@
    1.47         | _ => false
    1.48  in
    1.49  
    1.50 -fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i
    1.51 -                       in IHinst tac rcallTs i end THEN
    1.52 -                  eresolve_tac rcall_lemmas i
    1.53 +fun rcall_tac ctxt i =
    1.54 +  let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
    1.55 +  in IHinst tac @{thms rcallTs} i end
    1.56 +  THEN eresolve_tac @{thms rcall_lemmas} i
    1.57  
    1.58 -fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE
    1.59 -                           rcall_tac i ORELSE
    1.60 -                           ematch_tac [SubtypeE] i ORELSE
    1.61 -                           match_tac [SubtypeI] i
    1.62 +fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
    1.63 +                           rcall_tac ctxt i ORELSE
    1.64 +                           ematch_tac [@{thm SubtypeE}] i ORELSE
    1.65 +                           match_tac [@{thm SubtypeI}] i
    1.66  
    1.67 -fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
    1.68 -          if is_rigid_prog Bi then raw_step_tac prems i else no_tac)
    1.69 +fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
    1.70 +          if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
    1.71  
    1.72 -fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i
    1.73 +fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
    1.74  
    1.75 -val tac = typechk_tac [] 1
    1.76 +fun tac ctxt = typechk_tac ctxt [] 1
    1.77  
    1.78  (*** Clean up Correctness Condictions ***)
    1.79  
    1.80 -val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE'
    1.81 +val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    1.82                                   hyp_subst_tac)
    1.83  
    1.84 -val clean_ccs_tac =
    1.85 -       let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i
    1.86 -       in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
    1.87 -                       eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
    1.88 -                       hyp_subst_tac)) end
    1.89 +fun clean_ccs_tac ctxt =
    1.90 +  let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
    1.91 +    TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
    1.92 +    eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    1.93 +    hyp_subst_tac))
    1.94 +  end
    1.95  
    1.96 -fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN
    1.97 -                                     clean_ccs_tac) i
    1.98 +fun gen_ccs_tac ctxt rls i =
    1.99 +  SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i
   1.100  
   1.101  end
   1.102  *}
     2.1 --- a/src/CCL/ex/Flag.thy	Sat Jun 14 23:33:43 2008 +0200
     2.2 +++ b/src/CCL/ex/Flag.thy	Sat Jun 14 23:52:51 2008 +0200
     2.3 @@ -64,15 +64,17 @@
     2.4  
     2.5  lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
     2.6    apply (unfold flag_def)
     2.7 -  apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
     2.8 -  apply (tactic clean_ccs_tac)
     2.9 +  apply (tactic {* typechk_tac @{context}
    2.10 +    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    2.11 +  apply (tactic "clean_ccs_tac @{context}")
    2.12    apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
    2.13    apply assumption
    2.14    done
    2.15  
    2.16  lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
    2.17    apply (unfold flag_def)
    2.18 -  apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
    2.19 +  apply (tactic {* gen_ccs_tac @{context}
    2.20 +    [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    2.21    oops
    2.22  
    2.23  end
     3.1 --- a/src/CCL/ex/List.thy	Sat Jun 14 23:33:43 2008 +0200
     3.2 +++ b/src/CCL/ex/List.thy	Sat Jun 14 23:52:51 2008 +0200
     3.3 @@ -75,13 +75,13 @@
     3.4  
     3.5  lemma mapT: "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)"
     3.6    apply (unfold map_def)
     3.7 -  apply (tactic "typechk_tac [] 1")
     3.8 +  apply (tactic "typechk_tac @{context} [] 1")
     3.9    apply blast
    3.10    done
    3.11  
    3.12  lemma appendT: "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)"
    3.13    apply (unfold append_def)
    3.14 -  apply (tactic "typechk_tac [] 1")
    3.15 +  apply (tactic "typechk_tac @{context} [] 1")
    3.16    done
    3.17  
    3.18  lemma appendTS:
    3.19 @@ -90,17 +90,17 @@
    3.20  
    3.21  lemma filterT: "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)"
    3.22    apply (unfold filter_def)
    3.23 -  apply (tactic "typechk_tac [] 1")
    3.24 +  apply (tactic "typechk_tac @{context} [] 1")
    3.25    done
    3.26  
    3.27  lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)"
    3.28    apply (unfold flat_def)
    3.29 -  apply (tactic {* typechk_tac [thm "appendT"] 1 *})
    3.30 +  apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *})
    3.31    done
    3.32  
    3.33  lemma insertT: "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"
    3.34    apply (unfold insert_def)
    3.35 -  apply (tactic "typechk_tac [] 1")
    3.36 +  apply (tactic "typechk_tac @{context} [] 1")
    3.37    done
    3.38  
    3.39  lemma insertTS:
    3.40 @@ -111,8 +111,8 @@
    3.41  lemma partitionT:
    3.42    "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)"
    3.43    apply (unfold partition_def)
    3.44 -  apply (tactic "typechk_tac [] 1")
    3.45 -  apply (tactic clean_ccs_tac)
    3.46 +  apply (tactic "typechk_tac @{context} [] 1")
    3.47 +  apply (tactic "clean_ccs_tac @{context}")
    3.48    apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
    3.49      apply assumption+
    3.50    apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]])
     4.1 --- a/src/CCL/ex/Nat.thy	Sat Jun 14 23:33:43 2008 +0200
     4.2 +++ b/src/CCL/ex/Nat.thy	Sat Jun 14 23:52:51 2008 +0200
     4.3 @@ -61,32 +61,32 @@
     4.4  
     4.5  lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
     4.6    apply (unfold add_def)
     4.7 -  apply (tactic {* typechk_tac [] 1 *})
     4.8 +  apply (tactic {* typechk_tac @{context} [] 1 *})
     4.9    done
    4.10  
    4.11  lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    4.12    apply (unfold add_def mult_def)
    4.13 -  apply (tactic {* typechk_tac [] 1 *})
    4.14 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    4.15    done
    4.16  
    4.17  (* Defined to return zero if a<b *)
    4.18  lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    4.19    apply (unfold sub_def)
    4.20 -  apply (tactic {* typechk_tac [] 1 *})
    4.21 -  apply (tactic clean_ccs_tac)
    4.22 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    4.23 +  apply (tactic {* clean_ccs_tac @{context} *})
    4.24    apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    4.25    done
    4.26  
    4.27  lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    4.28    apply (unfold le_def)
    4.29 -  apply (tactic {* typechk_tac [] 1 *})
    4.30 -  apply (tactic clean_ccs_tac)
    4.31 +  apply (tactic {* typechk_tac @{context} [] 1 *})
    4.32 +  apply (tactic {* clean_ccs_tac @{context} *})
    4.33    apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    4.34    done
    4.35  
    4.36  lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    4.37    apply (unfold not_def lt_def)
    4.38 -  apply (tactic {* typechk_tac [thm "leT"] 1 *})
    4.39 +  apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
    4.40    done
    4.41  
    4.42  
    4.43 @@ -96,9 +96,8 @@
    4.44  
    4.45  lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
    4.46    apply (unfold ack_def)
    4.47 -  apply (tactic "gen_ccs_tac [] 1")
    4.48 +  apply (tactic {* gen_ccs_tac @{context} [] 1 *})
    4.49    apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
    4.50    done
    4.51  
    4.52  end
    4.53 -