src/CCL/Wfd.thy
changeset 27221 31328dc30196
parent 27208 5fe899199f85
child 27239 f2f42f9fa09d
     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  *}