src/HOL/Tools/inductive_package.ML
changeset 7710 bf8cb3fc5d64
parent 7349 228b711ad68c
child 7798 42e94b618f34
--- a/src/HOL/Tools/inductive_package.ML	Tue Oct 05 14:11:34 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 05 15:23:22 1999 +0200
@@ -36,6 +36,9 @@
     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
   val print_inductives: theory -> unit
+  val mono_add_global: theory attribute
+  val mono_del_global: theory attribute
+  val get_monos: theory -> thm list
   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     theory attribute list -> ((bstring * term) * theory attribute list) list ->
       thm list -> thm list -> theory -> theory *
@@ -56,6 +59,102 @@
 structure InductivePackage: INDUCTIVE_PACKAGE =
 struct
 
+(*** theory data ***)
+
+(* data kind 'HOL/inductive' *)
+
+type inductive_info =
+  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
+    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
+
+structure InductiveArgs =
+struct
+  val name = "HOL/inductive";
+  type T = inductive_info Symtab.table * thm list;
+
+  val empty = (Symtab.empty, []);
+  val copy = I;
+  val prep_ext = I;
+  fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
+    Library.generic_merge Thm.eq_thm I I monos1 monos2);
+
+  fun print sg (tab, monos) =
+    (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
+       map #1 (Sign.cond_extern_table sg Sign.constK tab)));
+     Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
+end;
+
+structure InductiveData = TheoryDataFun(InductiveArgs);
+val print_inductives = InductiveData.print;
+
+
+(* get and put data *)
+
+fun get_inductive thy name =
+  (case Symtab.lookup (fst (InductiveData.get thy), name) of
+    Some info => info
+  | None => error ("Unknown (co)inductive set " ^ quote name));
+
+fun put_inductives names info thy =
+  let
+    fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
+    val tab_monos = foldl upd (InductiveData.get thy, names)
+      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
+  in InductiveData.put tab_monos thy end;
+
+val get_monos = snd o InductiveData.get;
+
+fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
+
+(** monotonicity rules **)
+
+fun mk_mono thm =
+  let
+    fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
+      (case concl_of thm of
+          (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
+        | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
+    val concl = concl_of thm
+  in
+    if Logic.is_equals concl then
+      eq2mono (thm RS meta_eq_to_obj_eq)
+    else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
+      eq2mono thm
+    else [thm]
+  end;
+
+(* mono add/del *)
+
+local
+
+fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
+
+fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
+fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
+
+fun mk_att f g (x, thm) = (f (g thm) x, thm);
+
+in
+
+val mono_add_global = mk_att map_rules_global add_mono;
+val mono_del_global = mk_att map_rules_global del_mono;
+
+end;
+
+
+(* concrete syntax *)
+
+val monoN = "mono";
+val addN = "add";
+val delN = "del";
+
+fun mono_att add del =
+  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
+
+val mono_attr =
+  (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
+
+
 
 (** utilities **)
 
@@ -101,9 +200,6 @@
 
 (* misc *)
 
-(*for proving monotonicity of recursion operator*)
-val default_monos = basic_monos @ [vimage_mono];
-
 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
 
 (*Delete needless equality assumptions*)
@@ -157,24 +253,21 @@
 
 val msg1 = "Conclusion of introduction rule must have form\
           \ ' t : S_i '";
-val msg2 = "Premises mentioning recursive sets must have form\
-          \ ' t : M S_i '";
+val msg2 = "Non-atomic premise";
 val msg3 = "Recursion term on left of member symbol";
 
 fun check_rule sign cs r =
   let
-    fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then
-         (case prem of
-           (Const ("op :", _) $ t $ u) =>
-             if exists (Logic.occs o (rpair t)) cs then
-               err_in_prem sign r prem msg3 else ()
-         | _ => err_in_prem sign r prem msg2)
-        else ()
+    fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
+      else err_in_prem sign r prem msg2;
 
-  in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of
-        (Const ("op :", _) $ _ $ u) =>
-          if u mem cs then seq (check_prem o HOLogic.dest_Trueprop)
-            (Logic.strip_imp_prems r)
+  in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
+        (Const ("op :", _) $ t $ u) =>
+          if u mem cs then
+            if exists (Logic.occs o (rpair t)) cs then
+              err_in_rule sign r msg3
+            else
+              seq check_prem (Logic.strip_imp_prems r)
           else err_in_rule sign r msg1
       | _ => err_in_rule sign r msg1)
   end;
@@ -185,49 +278,6 @@
 
 
 
-(*** theory data ***)
-
-(* data kind 'HOL/inductive' *)
-
-type inductive_info =
-  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
-    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
-
-structure InductiveArgs =
-struct
-  val name = "HOL/inductive";
-  type T = inductive_info Symtab.table;
-
-  val empty = Symtab.empty;
-  val copy = I;
-  val prep_ext = I;
-  val merge: T * T -> T = Symtab.merge (K true);
-
-  fun print sg tab =
-    Pretty.writeln (Pretty.strs ("(co)inductives:" ::
-      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
-end;
-
-structure InductiveData = TheoryDataFun(InductiveArgs);
-val print_inductives = InductiveData.print;
-
-
-(* get and put data *)
-
-fun get_inductive thy name =
-  (case Symtab.lookup (InductiveData.get thy, name) of
-    Some info => info
-  | None => error ("Unknown (co)inductive set " ^ quote name));
-
-fun put_inductives names info thy =
-  let
-    fun upd (tab, name) = Symtab.update_new ((name, info), tab);
-    val tab = foldl upd (InductiveData.get thy, names)
-      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
-  in InductiveData.put tab thy end;
-
-
-
 (*** properties of (co)inductive sets ***)
 
 (** elimination rules **)
@@ -280,22 +330,33 @@
       let
         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
 
-        fun subst (prem as (Const ("op :", T) $ t $ u), prems) =
-              let val n = find_index_eq u cs in
-                if n >= 0 then prem :: (nth_elem (n, preds)) $ t :: prems else
-                  (subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int"
-                    (c, HOLogic.Collect_const (HOLogic.dest_setT
-                      (fastype_of c)) $ P))) (cs ~~ preds)) prem)::prems
-              end
-          | subst (prem, prems) = prem::prems;
+        val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
 
+        fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
+              (case pred_of u of
+                  None => (m $ fst (subst t) $ fst (subst u), None)
+                | Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t)))
+          | subst s =
+              (case pred_of s of
+                  Some P => (HOLogic.mk_binop "op Int"
+                    (s, HOLogic.Collect_const (HOLogic.dest_setT
+                      (fastype_of s)) $ P), None)
+                | None => (case s of
+                     (t $ u) => (fst (subst t) $ fst (subst u), None)
+                   | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
+                   | _ => (s, None)));
+
+        fun mk_prem (s, prems) = (case subst s of
+              (_, Some (t, u)) => t :: u :: prems
+            | (t, _) => t :: prems);
+          
         val Const ("op :", _) $ t $ u =
           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
 
       in list_all_free (frees,
-           Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst
+           Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
-               HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) $ t)))
+               HOLogic.mk_Trueprop (the (pred_of u) $ t)))
       end;
 
     val ind_prems = map mk_ind_prem intr_ts;
@@ -312,7 +373,7 @@
         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
       end;
 
-    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
+    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
 
   in (preds, ind_prems, mutual_ind_concl)
@@ -330,7 +391,7 @@
 
     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
-        (fn _ => [rtac monoI 1, REPEAT (ares_tac (default_monos @ monos) 1)])
+        (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
 
   in mono end;
 
@@ -374,8 +435,8 @@
   let
     val _ = message "  Proving the elimination rules ...";
 
-    val rules1 = [CollectE, disjE, make_elim vimageD];
-    val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
+    val rules1 = [CollectE, disjE, make_elim vimageD, exE];
+    val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
       map make_elim [Inl_inject, Inr_inject];
 
     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
@@ -493,14 +554,13 @@
       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
         [rtac (impI RS allI) 1,
          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
-         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
+         rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
          fold_goals_tac rec_sets_defs,
          (*This CollectE and disjE separates out the introduction rules*)
-         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
+         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
-                     ORELSE' hyp_subst_tac)),
+         REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
          rewrite_goals_tac sum_case_rewrites,
          EVERY (map (fn prem =>
            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
@@ -554,7 +614,7 @@
           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
 
       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
-        (frees, foldr1 (app HOLogic.conj)
+        (frees, foldr1 HOLogic.mk_conj
           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
             (map (subst o HOLogic.dest_Trueprop)
               (Logic.strip_imp_prems r))))
@@ -563,7 +623,7 @@
     (* make a disjunction of all introduction rules *)
 
     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
-      absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
+      absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
 
     (* add definiton of recursive sets to theory *)
 
@@ -651,12 +711,12 @@
          else I)
       |> Theory.add_path rec_name
       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
-      |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
+      |> (if coind then I else
+            PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
 
     val intrs = PureThy.get_thms thy' "intrs";
     val elims = PureThy.get_thms thy' "elims";
-    val raw_induct = if coind then TrueI else
-      standard (split_rule (PureThy.get_thm thy' "internal_induct"));
+    val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct";
     val induct = if coind orelse length cs > 1 then raw_induct
       else standard (raw_induct RSN (2, rev_mp));
 
@@ -698,8 +758,6 @@
       "Recursive set not previously declared as constant: " sign) cs;
     val cnames = map Sign.base_name full_cnames;
 
-    val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
-       (fn a => "Base name of recursive set not an identifier: " ^ a);
     val _ = seq (check_rule sign cs o snd o fst) intros;
 
     val (thy1, result) =
@@ -716,11 +774,11 @@
 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   let
     val sign = Theory.sign_of thy;
-    val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
+    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termTVar) c_strings;
 
     val atts = map (Attrib.global_attribute thy) srcs;
     val intr_names = map (fst o fst) intro_srcs;
-    val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs;
+    val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
     val (cs', intr_ts') = unify_consts sign cs intr_ts;
 
@@ -738,7 +796,8 @@
 
 (* setup theory *)
 
-val setup = [InductiveData.init];
+val setup = [InductiveData.init,
+             Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
 
 
 (* outer syntax *)