--- a/src/Provers/induct_method.ML Fri Oct 12 12:11:39 2001 +0200
+++ b/src/Provers/induct_method.ML Fri Oct 12 12:13:31 2001 +0200
@@ -3,7 +3,7 @@
Author: Markus Wenzel, TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
-Proof by cases and induction on types and sets.
+Proof by cases and induction on sets and types.
*)
signature INDUCT_METHOD_DATA =
@@ -18,8 +18,6 @@
signature INDUCT_METHOD =
sig
- val vars_of: term -> term list
- val concls_of: thm -> term list
val setup: (theory -> theory) list
end;
@@ -33,116 +31,100 @@
fun align_left msg xs ys =
let val m = length xs and n = length ys
- in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
+ in if m < n then raise ERROR_MESSAGE msg else (Library.take (n, xs) ~~ ys) end;
fun align_right msg xs ys =
let val m = length xs and n = length ys
- in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
+ in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end;
-(* thms and terms *)
-
-val concls_of = Data.dest_concls o Thm.concl_of;
+(* prep_inst *)
-fun vars_of tm = (*ordered left-to-right, preferring right!*)
- Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
- |> Library.distinct |> rev;
-
-fun type_name t =
- #1 (Term.dest_Type (Term.type_of t))
- handle TYPE _ => raise TERM ("Type of term argument is too general", [t]);
-
-fun prep_inst align cert f (tm, ts) =
+fun prep_inst align cert tune (tm, ts) =
let
fun prep_var (x, Some t) =
let
val cx = cert x;
val {T = xT, sign, ...} = Thm.rep_cterm cx;
val orig_ct = cert t;
- val ct = f orig_ct;
+ val ct = tune orig_ct;
in
if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct)
- else error (Pretty.string_of (Pretty.block
- [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
- Display.pretty_cterm orig_ct, Pretty.str " ::", Pretty.brk 1,
- Display.pretty_ctyp (#T (Thm.crep_cterm orig_ct))]))
+ else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block
+ [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
+ Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
+ Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
end
| prep_var (_, None) = None;
+ val xs = InductAttrib.vars_of tm;
in
- align "Rule has fewer variables than instantiations given" (vars_of tm) ts
+ align "Rule has fewer variables than instantiations given" xs ts
|> mapfilter prep_var
end;
-(* resolution and cases *)
-
-local
-
-fun gen_resolveq_tac tac rules i st =
- Seq.flat (Seq.map (fn rule => tac rule i st) rules);
+(* tactics with cases *)
-in
+fun resolveq_cases_tac make tac ruleq i st =
+ ruleq |> Seq.map (fn (rule, (cases, facts)) =>
+ (Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st
+ |> Seq.map (rpair (make rule cases)))
+ |> Seq.flat;
-fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st =>
- Seq.map (rpair (make rule cases))
- ((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st));
+
+infix 1 THEN_ALL_NEW_CASES;
-end;
+fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
+ st |> Seq.THEN (tac1 i, (fn (st', cases) =>
+ Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
(** cases method **)
(*
- rule selection:
- cases - classical case split
- cases t - datatype exhaustion
- <x:A> cases ... - set elimination
- ... cases ... R - explicit rule
+ rule selection scheme:
+ cases - classical case split
+ <x:A> cases ... - set cases
+ cases t - type cases
+ ... cases ... R - explicit rule
*)
local
-fun cases_tac (ctxt, (open_parms, args)) facts =
+fun find_casesT ctxt ((Some t :: _) :: _) = InductAttrib.find_casesT ctxt (fastype_of t)
+ | find_casesT _ _ = [];
+
+fun find_casesS ctxt (fact :: _) = InductAttrib.find_casesS ctxt fact
+ | find_casesS _ _ = [];
+
+fun cases_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
let
val sg = ProofContext.sign_of ctxt;
val cert = Thm.cterm_of sg;
- fun inst_rule insts thm =
- (align_left "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts
+ fun inst_rule r =
+ if null insts then RuleCases.add r
+ else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
|> (flat o map (prep_inst align_left cert I))
- |> Drule.cterm_instantiate) thm;
-
- fun find_cases th =
- NetRules.may_unify (#2 (InductAttrib.get_cases ctxt))
- (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
+ |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
- val rules =
- (case (fst args, facts) of
- (([], None), []) => [RuleCases.add Data.cases_default]
- | ((insts, None), []) =>
- let
- val name = type_name (hd (flat (map (mapfilter I) insts)))
- handle Library.LIST _ => error "Unable to figure out type cases rule"
- in
- (case InductAttrib.lookup_casesT ctxt name of
- None => error ("No cases rule for type: " ^ quote name)
- | Some thm => [(inst_rule insts thm, RuleCases.get thm)])
+ val ruleq =
+ (case (facts, insts, opt_rule) of
+ ([], [], None) => Seq.single (RuleCases.add Data.cases_default)
+ | (_, _, None) =>
+ let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
+ if null rules then error "Unable to figure out cases rule" else ();
+ Method.trace rules;
+ Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
end
- | (([], None), th :: _) => map (RuleCases.add o #2) (find_cases th)
- | ((insts, None), th :: _) =>
- (case find_cases th of (*may instantiate first rule only!*)
- (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
- | [] => [])
- | (([], Some thm), _) => [RuleCases.add thm]
- | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
- |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
+ | (_, _, Some r) => Seq.single (inst_rule r));
- fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
- (Method.multi_resolves (take (n, facts)) [thm]);
+ fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
+ (Method.multi_resolves (take (n, facts)) [th]);
in
resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
- (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
+ (Seq.flat (Seq.map prep_rule ruleq))
end;
in
@@ -156,10 +138,10 @@
(** induct method **)
(*
- rule selection:
- induct x - datatype induction
- <x:A> induct ... - set induction
- ... induct ... R - explicit rule
+ rule selection scheme:
+ <x:A> induct ... - set induction
+ induct x - type induction
+ ... induct ... R - explicit rule
*)
local
@@ -182,77 +164,60 @@
in map (apsnd ruly_case) ooo RuleCases.make_raw end;
-infix 1 THEN_ALL_NEW_CASES;
-
-fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
- st |> Seq.THEN (tac1 i, (fn (st', cases) =>
- Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
-
-
-fun induct_rule ctxt t =
- let val name = type_name t in
- (case InductAttrib.lookup_inductT ctxt name of
- None => error ("No induct rule for type: " ^ quote name)
- | Some thm => (name, thm))
- end;
+val eq_prems = curry (Term.aconvs o pairself Thm.prems_of);
-fun join_rules [(_, thm)] = thm
- | join_rules raw_thms =
- let
- val thms = (map (apsnd Drule.freeze_all) raw_thms);
- fun eq_prems ((_, th1), (_, th2)) =
- Term.aconvs (Thm.prems_of th1, Thm.prems_of th2);
- in
- (case Library.gen_distinct eq_prems thms of
- [(_, thm)] =>
- let
- val cprems = Drule.cprems_of thm;
- val asms = map Thm.assume cprems;
- fun strip (_, th) = Drule.implies_elim_list th asms;
- in
- foldr1 (fn (th, th') => [th, th'] MRS Data.conjI) (map strip thms)
- |> Drule.implies_intr_list cprems
- |> Drule.standard
- end
- | [] => error "No rule given"
- | bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads)))
- end;
+fun join_rules [] = []
+ | join_rules [th] = [th]
+ | join_rules (rules as r :: rs) =
+ if not (forall (eq_prems r) rs) then []
+ else
+ let
+ val th :: ths = map Drule.freeze_all rules;
+ val cprems = Drule.cprems_of th;
+ val asms = map Thm.assume cprems;
+ in
+ [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
+ (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
+ |> Drule.implies_intr_list cprems
+ |> Drule.standard']
+ end;
+fun find_inductT ctxt insts =
+ foldr multiply (insts |> mapfilter (fn [] => None | ts => last_elem ts)
+ |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
+ |> map join_rules |> flat;
-fun induct_tac (ctxt, (open_parms, args)) facts =
+fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
+ | find_inductS _ _ = [];
+
+fun induct_tac (ctxt, (open_parms, (insts, opt_rule))) facts =
let
val sg = ProofContext.sign_of ctxt;
val cert = Thm.cterm_of sg;
- fun inst_rule insts thm =
- (align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts
+ fun inst_rule r =
+ if null insts then RuleCases.add r
+ else (align_right "Rule has fewer conclusions than arguments given"
+ (Data.dest_concls (Thm.concl_of r)) insts
|> (flat o map (prep_inst align_right cert atomize_cterm))
- |> Drule.cterm_instantiate) thm;
-
- fun find_induct th =
- NetRules.may_unify (#2 (InductAttrib.get_induct ctxt))
- (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
+ |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
- val rules =
- (case (fst args, facts) of
- (([], None), []) => []
- | ((insts, None), []) =>
- let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts
- handle Library.LIST _ => error "Unable to figure out type induction rule"
- in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end
- | (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th)
- | ((insts, None), th :: _) =>
- (case find_induct th of (*may instantiate first rule only!*)
- (_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)]
- | [] => [])
- | (([], Some thm), _) => [RuleCases.add thm]
- | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)])
- |> map (Library.apfst (Attrib.read_inst' (snd args) ctxt));
+ val ruleq =
+ (case opt_rule of
+ None =>
+ let val rules = find_inductS ctxt facts @ find_inductT ctxt insts in
+ if null rules then error "Unable to figure out induct rule" else ();
+ Method.trace rules;
+ Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
+ end
+ | Some r => Seq.single (inst_rule r));
- fun prep_rule (thm, (cases, n)) =
- Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]);
+ (* FIXME divinate rule_inst *)
+
+ fun prep_rule (th, (cases, n)) =
+ Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [th]);
val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
- (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
+ (Seq.flat (Seq.map prep_rule ruleq));
in tac THEN_ALL_NEW_CASES rulify_tac end;
in
@@ -271,7 +236,7 @@
local
-fun err k get name =
+fun check k get name =
(case get name of Some x => x
| None => error ("No rule for " ^ k ^ " " ^ quote name));
@@ -280,8 +245,10 @@
fun rule get_type get_set =
Scan.depend (fn ctxt =>
let val sg = ProofContext.sign_of ctxt in
- spec InductAttrib.typeN >> (err InductAttrib.typeN (get_type ctxt) o Sign.intern_tycon sg) ||
- spec InductAttrib.setN >> (err InductAttrib.setN (get_set ctxt) o Sign.intern_const sg)
+ spec InductAttrib.typeN >> (check InductAttrib.typeN (get_type ctxt) o
+ Sign.certify_tyname sg o Sign.intern_tycon sg) ||
+ spec InductAttrib.setN >> (check InductAttrib.setN (get_set ctxt) o
+ Sign.certify_const sg o Sign.intern_const sg)
end >> pair ctxt) ||
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
@@ -297,17 +264,10 @@
val instss = Args.and_list (Scan.repeat1 term_dummy);
-(* FIXME Attrib.insts': better use actual term args *)
-val rule_insts =
- Scan.lift (Scan.optional ((Args.$$$ ofN -- Args.colon) |-- Args.!!! Attrib.insts') ([], []));
-
in
-val cases_args =
- Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule -- rule_insts));
-
-val induct_args =
- Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule -- rule_insts));
+val cases_args = Method.syntax (Args.mode openN -- (instss -- Scan.option cases_rule));
+val induct_args = Method.syntax (Args.mode openN -- (instss -- Scan.option induct_rule));
end;