simplified resolveq_cases_tac for cases, separate version for induct;
authorwenzelm
Tue Oct 16 00:32:01 2001 +0200 (2001-10-16)
changeset 1179042393a11642d
parent 11789 da81334357ba
child 11791 2c201f3b018e
simplified resolveq_cases_tac for cases, separate version for induct;
divinate instantiation of induct rules;
tuned;
src/Provers/induct_method.ML
     1.1 --- a/src/Provers/induct_method.ML	Tue Oct 16 00:30:53 2001 +0200
     1.2 +++ b/src/Provers/induct_method.ML	Tue Oct 16 00:32:01 2001 +0200
     1.3 @@ -63,22 +63,6 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(* tactics with cases *)
     1.8 -
     1.9 -fun resolveq_cases_tac make tac ruleq i st =
    1.10 -  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
    1.11 -    (Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st
    1.12 -    |> Seq.map (rpair (make rule cases)))
    1.13 -  |> Seq.flat;
    1.14 -
    1.15 -
    1.16 -infix 1 THEN_ALL_NEW_CASES;
    1.17 -
    1.18 -fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
    1.19 -  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
    1.20 -    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
    1.21 -
    1.22 -
    1.23  
    1.24  (** cases method **)
    1.25  
    1.26 @@ -92,6 +76,12 @@
    1.27  
    1.28  local
    1.29  
    1.30 +fun resolveq_cases_tac make ruleq i st =
    1.31 +  ruleq |> Seq.map (fn (rule, (cases, facts)) =>
    1.32 +    (Method.insert_tac facts THEN' Tactic.rtac rule) i st
    1.33 +    |> Seq.map (rpair (make rule cases)))
    1.34 +  |> Seq.flat;
    1.35 +
    1.36  fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
    1.37    | find_casesT _ _ = [];
    1.38  
    1.39 @@ -122,10 +112,7 @@
    1.40  
    1.41      fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
    1.42        (Method.multi_resolves (take (n, facts)) [th]);
    1.43 -  in
    1.44 -    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
    1.45 -      (Seq.flat (Seq.map prep_rule ruleq))
    1.46 -  end;
    1.47 +  in resolveq_cases_tac (RuleCases.make open_parms) (Seq.flat (Seq.map prep_rule ruleq)) end;
    1.48  
    1.49  in
    1.50  
    1.51 @@ -146,6 +133,9 @@
    1.52  
    1.53  local
    1.54  
    1.55 +
    1.56 +(* atomize and rulify *)
    1.57 +
    1.58  fun atomize_cterm ct =
    1.59    Thm.cterm_fun (ObjectLogic.drop_judgment (#sign (Thm.rep_cterm ct)))
    1.60      (Tactic.rewrite_cterm true Data.atomize ct);
    1.61 @@ -167,6 +157,8 @@
    1.62    in map (apsnd ruly_case) ooo RuleCases.make_raw end;
    1.63  
    1.64  
    1.65 +(* join multi-rules *)
    1.66 +
    1.67  val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
    1.68  
    1.69  fun join_rules [] = []
    1.70 @@ -185,6 +177,58 @@
    1.71            |> Drule.standard']
    1.72          end;
    1.73  
    1.74 +
    1.75 +(* divinate rule instantiation (cannot handle pending goal parameters) *)
    1.76 +
    1.77 +fun dest_env sign (Envir.Envir {asol, iTs, ...}) =
    1.78 +  let
    1.79 +    val pairs = Vartab.dest asol;
    1.80 +    val ts = map (Thm.cterm_of sign o #2) pairs;
    1.81 +    val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
    1.82 +  in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
    1.83 +
    1.84 +fun divinate_inst rule i st =
    1.85 +  let
    1.86 +    val {sign, maxidx, ...} = Thm.rep_thm st;
    1.87 +    val goal = List.nth (Thm.prems_of st, i - 1);  (*exception Subscript*)
    1.88 +    val params = rev (rename_wrt_term goal (Logic.strip_params goal));  (*as they are printed :-*)
    1.89 +  in
    1.90 +    if not (null params) then
    1.91 +      (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
    1.92 +        commas (map (Sign.string_of_term sign o Syntax.mark_boundT) params));
    1.93 +      Seq.single rule)
    1.94 +    else
    1.95 +      let
    1.96 +        val rule' = Thm.incr_indexes (maxidx + 1) rule;
    1.97 +        val concl = Logic.strip_assums_concl goal;
    1.98 +      in
    1.99 +        Unify.smash_unifiers (sign, Envir.empty (#maxidx (Thm.rep_thm rule')),
   1.100 +          [(Thm.concl_of rule', concl)])
   1.101 +        |> Seq.map (fn env => Thm.instantiate (dest_env sign env) rule')
   1.102 +      end
   1.103 +  end handle Subscript => Seq.empty;
   1.104 +
   1.105 +
   1.106 +(* compose tactics with cases *)
   1.107 +
   1.108 +fun resolveq_cases_tac' make ruleq i st =
   1.109 +  ruleq |> Seq.map (fn (rule, (cases, facts)) => st
   1.110 +    |> (Method.insert_tac facts THEN' atomize_tac) i
   1.111 +    |> Seq.map (fn st' => divinate_inst rule i st'
   1.112 +      |> Seq.map (fn rule' => st' |> Tactic.rtac rule' i |> Seq.map (rpair (make rule' cases)))
   1.113 +      |> Seq.flat)
   1.114 +    |> Seq.flat)
   1.115 +  |> Seq.flat;
   1.116 +
   1.117 +infix 1 THEN_ALL_NEW_CASES;
   1.118 +
   1.119 +fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   1.120 +  st |> Seq.THEN (tac1 i, (fn (st', cases) =>
   1.121 +    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
   1.122 +
   1.123 +
   1.124 +(* find rules *)
   1.125 +
   1.126  fun find_inductT ctxt insts =
   1.127    foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
   1.128      |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
   1.129 @@ -193,6 +237,9 @@
   1.130  fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
   1.131    | find_inductS _ _ = [];
   1.132  
   1.133 +
   1.134 +(* main tactic *)
   1.135 +
   1.136  fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
   1.137    let
   1.138      val sg = ProofContext.sign_of ctxt;
   1.139 @@ -215,11 +262,9 @@
   1.140            end
   1.141        | Some r => Seq.single (inst_rule r));
   1.142  
   1.143 -    (* FIXME divinate rule_inst *)
   1.144 -
   1.145      fun prep_rule (th, (cases, n)) =
   1.146        Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
   1.147 -    val tac = resolveq_cases_tac (rulify_cases sg cert open_parms) atomize_tac
   1.148 +    val tac = resolveq_cases_tac' (rulify_cases sg cert open_parms)
   1.149        (Seq.flat (Seq.map prep_rule ruleq));
   1.150    in tac THEN_ALL_NEW_CASES rulify_tac end;
   1.151