# HG changeset patch # User wenzelm # Date 1213480371 -7200 # Node ID 31328dc3019689ecf53d949b981a4bdb29c51014 # Parent 31adee1f467a47e196fc310e7a19338e723bf151 proper context for tactics derived from res_inst_tac; diff -r 31adee1f467a -r 31328dc30196 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Sat Jun 14 23:33:43 2008 +0200 +++ b/src/CCL/Wfd.thy Sat Jun 14 23:52:51 2008 +0200 @@ -421,18 +421,8 @@ local val type_rls = - thms "canTs" @ thms "icanTs" @ thms "applyT2" @ thms "ncanTs" @ thms "incanTs" @ - thms "precTs" @ thms "letrecTs" @ thms "letT" @ thms "Subtype_canTs"; - -val rcallT = thm "rcallT"; -val rcall2T = thm "rcall2T"; -val rcall3T = thm "rcall3T"; -val rcallTs = thms "rcallTs"; -val rcall_lemmas = thms "rcall_lemmas"; -val SubtypeE = thm "SubtypeE"; -val SubtypeI = thm "SubtypeI"; -val rmIHs = thms "rmIHs"; -val hyprcallTs = thms "hyprcallTs"; + @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @ + @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs}; fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) | bvars _ l = l @@ -445,9 +435,9 @@ | get_bno l n (Bound m) = (m-length(l),n) (* Not a great way of identifying induction hypothesis! *) -fun could_IH x = could_unify(x,hd (prems_of rcallT)) orelse - could_unify(x,hd (prems_of rcall2T)) orelse - could_unify(x,hd (prems_of rcall3T)) +fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse + could_unify(x,hd (prems_of @{thm rcall2T})) orelse + could_unify(x,hd (prems_of @{thm rcall3T})) fun IHinst tac rls = SUBGOAL (fn (Bi,i) => let val bvs = bvars Bi [] @@ -456,7 +446,7 @@ let val (a,b) = get_bno [] 0 x in (List.nth(bvs,a),b) end) ihs fun try_IHs [] = no_tac - | try_IHs ((x,y)::xs) = tac [("g",x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) + | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) in try_IHs rnames end) fun is_rigid_prog t = @@ -465,35 +455,37 @@ | _ => false in -fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i - in IHinst tac rcallTs i end THEN - eresolve_tac rcall_lemmas i +fun rcall_tac ctxt i = + let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i + in IHinst tac @{thms rcallTs} i end + THEN eresolve_tac @{thms rcall_lemmas} i -fun raw_step_tac prems i = ares_tac (prems@type_rls) i ORELSE - rcall_tac i ORELSE - ematch_tac [SubtypeE] i ORELSE - match_tac [SubtypeI] i +fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE + rcall_tac ctxt i ORELSE + ematch_tac [@{thm SubtypeE}] i ORELSE + match_tac [@{thm SubtypeI}] i -fun tc_step_tac prems = SUBGOAL (fn (Bi,i) => - if is_rigid_prog Bi then raw_step_tac prems i else no_tac) +fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) => + if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) -fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i +fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i -val tac = typechk_tac [] 1 +fun tac ctxt = typechk_tac ctxt [] 1 (*** Clean up Correctness Condictions ***) -val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' +val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' hyp_subst_tac) -val clean_ccs_tac = - let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i - in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' - eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' - hyp_subst_tac)) end +fun clean_ccs_tac ctxt = + let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in + TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' + eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' + hyp_subst_tac)) + end -fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN - clean_ccs_tac) i +fun gen_ccs_tac ctxt rls i = + SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i end *} diff -r 31adee1f467a -r 31328dc30196 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Sat Jun 14 23:33:43 2008 +0200 +++ b/src/CCL/ex/Flag.thy Sat Jun 14 23:52:51 2008 +0200 @@ -64,15 +64,17 @@ lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" apply (unfold flag_def) - apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) - apply (tactic clean_ccs_tac) + apply (tactic {* typechk_tac @{context} + [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) + apply (tactic "clean_ccs_tac @{context}") apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) apply assumption done lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}" apply (unfold flag_def) - apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) + apply (tactic {* gen_ccs_tac @{context} + [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) oops end diff -r 31adee1f467a -r 31328dc30196 src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Sat Jun 14 23:33:43 2008 +0200 +++ b/src/CCL/ex/List.thy Sat Jun 14 23:52:51 2008 +0200 @@ -75,13 +75,13 @@ lemma mapT: "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)" apply (unfold map_def) - apply (tactic "typechk_tac [] 1") + apply (tactic "typechk_tac @{context} [] 1") apply blast done lemma appendT: "[| l : List(A); m : List(A) |] ==> l @ m : List(A)" apply (unfold append_def) - apply (tactic "typechk_tac [] 1") + apply (tactic "typechk_tac @{context} [] 1") done lemma appendTS: @@ -90,17 +90,17 @@ lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)" apply (unfold filter_def) - apply (tactic "typechk_tac [] 1") + apply (tactic "typechk_tac @{context} [] 1") done lemma flatT: "l : List(List(A)) ==> flat(l) : List(A)" apply (unfold flat_def) - apply (tactic {* typechk_tac [thm "appendT"] 1 *}) + apply (tactic {* typechk_tac @{context} @{thms appendT} 1 *}) done lemma insertT: "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)" apply (unfold insert_def) - apply (tactic "typechk_tac [] 1") + apply (tactic "typechk_tac @{context} [] 1") done lemma insertTS: @@ -111,8 +111,8 @@ lemma partitionT: "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)" apply (unfold partition_def) - apply (tactic "typechk_tac [] 1") - apply (tactic clean_ccs_tac) + apply (tactic "typechk_tac @{context} [] 1") + apply (tactic "clean_ccs_tac @{context}") apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) apply assumption+ apply (rule ListPRI [THEN wfstI, THEN ListPR_wf [THEN wmap_wf, THEN wfI]]) diff -r 31adee1f467a -r 31328dc30196 src/CCL/ex/Nat.thy --- a/src/CCL/ex/Nat.thy Sat Jun 14 23:33:43 2008 +0200 +++ b/src/CCL/ex/Nat.thy Sat Jun 14 23:52:51 2008 +0200 @@ -61,32 +61,32 @@ lemma addT: "[| a:Nat; b:Nat |] ==> a #+ b : Nat" apply (unfold add_def) - apply (tactic {* typechk_tac [] 1 *}) + apply (tactic {* typechk_tac @{context} [] 1 *}) done lemma multT: "[| a:Nat; b:Nat |] ==> a #* b : Nat" apply (unfold add_def mult_def) - apply (tactic {* typechk_tac [] 1 *}) + apply (tactic {* typechk_tac @{context} [] 1 *}) done (* Defined to return zero if a a #- b : Nat" apply (unfold sub_def) - apply (tactic {* typechk_tac [] 1 *}) - apply (tactic clean_ccs_tac) + apply (tactic {* typechk_tac @{context} [] 1 *}) + apply (tactic {* clean_ccs_tac @{context} *}) apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) done lemma leT: "[| a:Nat; b:Nat |] ==> a #<= b : Bool" apply (unfold le_def) - apply (tactic {* typechk_tac [] 1 *}) - apply (tactic clean_ccs_tac) + apply (tactic {* typechk_tac @{context} [] 1 *}) + apply (tactic {* clean_ccs_tac @{context} *}) apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) done lemma ltT: "[| a:Nat; b:Nat |] ==> a #< b : Bool" apply (unfold not_def lt_def) - apply (tactic {* typechk_tac [thm "leT"] 1 *}) + apply (tactic {* typechk_tac @{context} @{thms leT} 1 *}) done @@ -96,9 +96,8 @@ lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat" apply (unfold ack_def) - apply (tactic "gen_ccs_tac [] 1") + apply (tactic {* gen_ccs_tac @{context} [] 1 *}) apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ done end -