accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:33:17 2005 +0200 (2005-06-17 ago)
changeset 16432a6e8fb94a8ca
parent 16431 90c9b8bb3b66
child 16433 e6fedd5baf32
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
Context.theory_name;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jun 17 18:33:16 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jun 17 18:33:17 2005 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val trace: bool ref
     1.7 -  val unify_consts: Sign.sg -> term list -> term list -> term list * term list
     1.8 +  val unify_consts: theory -> term list -> term list -> term list * term list
     1.9    val split_rule_vars: term list -> thm -> thm
    1.10    val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    1.11      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.12 @@ -89,25 +89,24 @@
    1.13    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    1.14      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    1.15  
    1.16 -structure InductiveArgs =
    1.17 -struct
    1.18 +structure InductiveData = TheoryDataFun
    1.19 +(struct
    1.20    val name = "HOL/inductive";
    1.21    type T = inductive_info Symtab.table * thm list;
    1.22  
    1.23    val empty = (Symtab.empty, []);
    1.24    val copy = I;
    1.25 -  val prep_ext = I;
    1.26 -  fun merge ((tab1, monos1), (tab2, monos2)) =
    1.27 +  val extend = I;
    1.28 +  fun merge _ ((tab1, monos1), (tab2, monos2)) =
    1.29      (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
    1.30  
    1.31 -  fun print sg (tab, monos) =
    1.32 +  fun print thy (tab, monos) =
    1.33      [Pretty.strs ("(co)inductives:" ::
    1.34 -      map #1 (NameSpace.extern_table (Sign.const_space sg, tab))),
    1.35 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
    1.36 +      map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
    1.37 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
    1.38      |> Pretty.chunks |> Pretty.writeln;
    1.39 -end;
    1.40 +end);
    1.41  
    1.42 -structure InductiveData = TheoryDataFun(InductiveArgs);
    1.43  val print_inductives = InductiveData.print;
    1.44  
    1.45  
    1.46 @@ -176,9 +175,9 @@
    1.47  
    1.48  (*the following code ensures that each recursive set always has the
    1.49    same type in all introduction rules*)
    1.50 -fun unify_consts sign cs intr_ts =
    1.51 +fun unify_consts thy cs intr_ts =
    1.52    (let
    1.53 -    val tsig = Sign.tsig_of sign;
    1.54 +    val tsig = Sign.tsig_of thy;
    1.55      val add_term_consts_2 =
    1.56        foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    1.57      fun varify (t, (i, ts)) =
    1.58 @@ -261,7 +260,7 @@
    1.59  fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
    1.60        let val T' = prodT_factors [] ps T1 ---> T2
    1.61            val newt = ap_split [] ps T1 T2 (Var (v, T'))
    1.62 -          val cterm = Thm.cterm_of (Thm.sign_of_thm rl)
    1.63 +          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    1.64        in
    1.65            instantiate ([], [(cterm t, cterm newt)]) rl
    1.66        end
    1.67 @@ -281,42 +280,43 @@
    1.68  
    1.69  local
    1.70  
    1.71 -fun err_in_rule sg name t msg =
    1.72 -  error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
    1.73 +fun err_in_rule thy name t msg =
    1.74 +  error (cat_lines ["Ill-formed introduction rule " ^ quote name,
    1.75 +    Sign.string_of_term thy t, msg]);
    1.76  
    1.77 -fun err_in_prem sg name t p msg =
    1.78 -  error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
    1.79 -    "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
    1.80 +fun err_in_prem thy name t p msg =
    1.81 +  error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
    1.82 +    "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]);
    1.83  
    1.84  val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
    1.85  
    1.86  val all_not_allowed = 
    1.87      "Introduction rule must not have a leading \"!!\" quantifier";
    1.88  
    1.89 -fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize [];
    1.90 +fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
    1.91  
    1.92  in
    1.93  
    1.94 -fun check_rule sg cs ((name, rule), att) =
    1.95 +fun check_rule thy cs ((name, rule), att) =
    1.96    let
    1.97      val concl = Logic.strip_imp_concl rule;
    1.98      val prems = Logic.strip_imp_prems rule;
    1.99 -    val aprems = map (atomize_term sg) prems;
   1.100 +    val aprems = map (atomize_term thy) prems;
   1.101      val arule = Logic.list_implies (aprems, concl);
   1.102  
   1.103      fun check_prem (prem, aprem) =
   1.104        if can HOLogic.dest_Trueprop aprem then ()
   1.105 -      else err_in_prem sg name rule prem "Non-atomic premise";
   1.106 +      else err_in_prem thy name rule prem "Non-atomic premise";
   1.107    in
   1.108      (case concl of
   1.109        Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
   1.110          if u mem cs then
   1.111            if exists (Logic.occs o rpair t) cs then
   1.112 -            err_in_rule sg name rule "Recursion term on left of member symbol"
   1.113 +            err_in_rule thy name rule "Recursion term on left of member symbol"
   1.114            else List.app check_prem (prems ~~ aprems)
   1.115 -        else err_in_rule sg name rule bad_concl
   1.116 -      | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
   1.117 -      | _ => err_in_rule sg name rule bad_concl);
   1.118 +        else err_in_rule thy name rule bad_concl
   1.119 +      | Const ("all", _) $ _ => err_in_rule thy name rule all_not_allowed
   1.120 +      | _ => err_in_rule thy name rule bad_concl);
   1.121      ((name, arule), att)
   1.122    end;
   1.123  
   1.124 @@ -477,7 +477,7 @@
   1.125  fun prove_mono setT fp_fun monos thy =
   1.126   (message "  Proving monotonicity ...";
   1.127    Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
   1.128 -    (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   1.129 +    (Thm.cterm_of thy (HOLogic.mk_Trueprop
   1.130        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   1.131      (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
   1.132  
   1.133 @@ -496,7 +496,7 @@
   1.134        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   1.135  
   1.136      val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   1.137 -      (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
   1.138 +      (Thm.cterm_of thy intr) (fn prems =>
   1.139         [(*insert prems and underlying sets*)
   1.140         cut_facts_tac prems 1,
   1.141         stac unfold 1,
   1.142 @@ -524,7 +524,7 @@
   1.143    in
   1.144      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
   1.145        quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   1.146 -        (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
   1.147 +        (Thm.cterm_of thy t) (fn prems =>
   1.148            [cut_facts_tac [hd prems] 1,
   1.149             dtac (unfold RS subst) 1,
   1.150             REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   1.151 @@ -566,7 +566,7 @@
   1.152    end;
   1.153  
   1.154  fun mk_cases elims s =
   1.155 -  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   1.156 +  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
   1.157  
   1.158  fun smart_mk_cases thy ss cprop =
   1.159    let
   1.160 @@ -582,7 +582,7 @@
   1.161  
   1.162  fun gen_inductive_cases prep_att prep_prop args thy =
   1.163    let
   1.164 -    val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
   1.165 +    val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
   1.166      val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
   1.167  
   1.168      val facts = args |> map (fn ((a, atts), props) =>
   1.169 @@ -599,7 +599,7 @@
   1.170    let
   1.171      val thy = ProofContext.theory_of ctxt;
   1.172      val ss = local_simpset_of ctxt;
   1.173 -    val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   1.174 +    val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
   1.175    in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   1.176  
   1.177  val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   1.178 @@ -612,21 +612,21 @@
   1.179    let
   1.180      val _ = clean_message "  Proving the induction rule ...";
   1.181  
   1.182 -    val sign = Theory.sign_of thy;
   1.183 -
   1.184      val sum_case_rewrites =
   1.185 -      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy ("sum.cases", NONE)
   1.186 -        else
   1.187 -          (case ThyInfo.lookup_theory "Datatype" of
   1.188 -            NONE => []
   1.189 -          | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE))) |> map mk_meta_eq;
   1.190 +      (if Context.theory_name thy = "Datatype" then
   1.191 +        PureThy.get_thms thy ("sum.cases", NONE)
   1.192 +      else
   1.193 +        (case ThyInfo.lookup_theory "Datatype" of
   1.194 +          NONE => []
   1.195 +        | SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE)))
   1.196 +      |> map mk_meta_eq;
   1.197  
   1.198      val (preds, ind_prems, mutual_ind_concl, factors) =
   1.199        mk_indrule cs cTs params intr_ts;
   1.200  
   1.201      val dummy = if !trace then
   1.202  		(writeln "ind_prems = ";
   1.203 -		 List.app (writeln o Sign.string_of_term sign) ind_prems)
   1.204 +		 List.app (writeln o Sign.string_of_term thy) ind_prems)
   1.205  	    else ();
   1.206  
   1.207      (* make predicate for instantiation of abstract induction rule *)
   1.208 @@ -649,7 +649,7 @@
   1.209      (* simplification rules for vimage and Collect *)
   1.210  
   1.211      val vimage_simps = if length cs < 2 then [] else
   1.212 -      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
   1.213 +      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   1.214          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.215            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   1.216             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   1.217 @@ -662,7 +662,7 @@
   1.218  		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   1.219  	    else ();
   1.220  
   1.221 -    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   1.222 +    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   1.223        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   1.224          [rtac (impI RS allI) 1,
   1.225           DETERM (etac raw_fp_induct 1),
   1.226 @@ -677,7 +677,7 @@
   1.227           EVERY (map (fn prem =>
   1.228     	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   1.229  
   1.230 -    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   1.231 +    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   1.232        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   1.233          [cut_facts_tac prems 1,
   1.234           REPEAT (EVERY
   1.235 @@ -738,7 +738,7 @@
   1.236      val rec_name = if alt_name = "" then
   1.237        space_implode "_" (map Sign.base_name cnames) else alt_name;
   1.238      val full_rec_name = if length cs < 2 then hd cnames
   1.239 -      else Sign.full_name (Theory.sign_of thy) rec_name;
   1.240 +      else Sign.full_name thy rec_name;
   1.241  
   1.242      val rec_const = list_comb
   1.243        (Const (full_rec_name, paramTs ---> setT), params);
   1.244 @@ -813,30 +813,29 @@
   1.245  
   1.246  (* external interfaces *)
   1.247  
   1.248 -fun try_term f msg sign t =
   1.249 +fun try_term f msg thy t =
   1.250    (case Library.try f t of
   1.251      SOME x => x
   1.252 -  | NONE => error (msg ^ Sign.string_of_term sign t));
   1.253 +  | NONE => error (msg ^ Sign.string_of_term thy t));
   1.254  
   1.255  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
   1.256    let
   1.257      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   1.258 -    val sign = Theory.sign_of thy;
   1.259  
   1.260      (*parameters should agree for all mutually recursive components*)
   1.261      val (_, params) = strip_comb (hd cs);
   1.262      val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   1.263 -      \ component is not a free variable: " sign) params;
   1.264 +      \ component is not a free variable: " thy) params;
   1.265  
   1.266      val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   1.267 -      "Recursive component not of type set: " sign) cs;
   1.268 +      "Recursive component not of type set: " thy) cs;
   1.269  
   1.270      val cnames = map (try_term (fst o dest_Const o head_of)
   1.271 -      "Recursive set not previously declared as constant: " sign) cs;
   1.272 +      "Recursive set not previously declared as constant: " thy) cs;
   1.273  
   1.274 -    val save_sign =
   1.275 -      thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   1.276 -    val intros = map (check_rule save_sign cs) pre_intros;
   1.277 +    val save_thy = thy
   1.278 +      |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames;
   1.279 +    val intros = map (check_rule save_thy cs) pre_intros;
   1.280      val induct_cases = map (#1 o #1) intros;
   1.281  
   1.282      val (thy1, result as {elims, induct, ...}) =
   1.283 @@ -850,15 +849,14 @@
   1.284  
   1.285  fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
   1.286    let
   1.287 -    val sign = Theory.sign_of thy;
   1.288 -    val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
   1.289 +    val cs = map (term_of o HOLogic.read_cterm thy) c_strings;
   1.290  
   1.291      val intr_names = map (fst o fst) intro_srcs;
   1.292 -    fun read_rule s = Thm.read_cterm sign (s, propT)
   1.293 +    fun read_rule s = Thm.read_cterm thy (s, propT)
   1.294        handle ERROR => error ("The error(s) above occurred for " ^ s);
   1.295      val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   1.296      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   1.297 -    val (cs', intr_ts') = unify_consts sign cs intr_ts;
   1.298 +    val (cs', intr_ts') = unify_consts thy cs intr_ts;
   1.299  
   1.300      val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
   1.301    in