# HG changeset patch
# User wenzelm
# Date 1002881611 -7200
# Node ID 60c0fa10bfc2cd929aea95b3f1fd36a85293b6d8
# Parent  7a21bf539412bf3b48cea7d7c9c53f97be3f6346
removed vars_of, concls_of;
removed additional rule instantiation argument;
proper enumeration of type rules;
append possibilities of set and type rules (analogous to elim-intro in 'rule');

diff -r 7a21bf539412 -r 60c0fa10bfc2 src/Provers/induct_method.ML
--- 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;