1.1 --- a/src/ZF/Tools/inductive_package.ML Sat Aug 05 14:52:55 2006 +0200
1.2 +++ b/src/ZF/Tools/inductive_package.ML Sat Aug 05 14:52:57 2006 +0200
1.3 @@ -65,7 +65,6 @@
1.4 intr_specs (monos, con_defs, type_intrs, type_elims) thy =
1.5 let
1.6 val _ = Theory.requires thy "Inductive" "(co)inductive definitions";
1.7 - val sign = sign_of thy;
1.8
1.9 val (intr_names, intr_tms) = split_list (map fst intr_specs);
1.10 val case_names = RuleCases.case_names intr_names;
1.11 @@ -75,7 +74,7 @@
1.12
1.13 val dummy = assert_all is_Const rec_hds
1.14 (fn t => "Recursive set not previously declared as constant: " ^
1.15 - Sign.string_of_term sign t);
1.16 + Sign.string_of_term thy t);
1.17
1.18 (*Now we know they are all Consts, so get their names, type and params*)
1.19 val rec_names = map (#1 o dest_Const) rec_hds
1.20 @@ -86,18 +85,18 @@
1.21 (fn a => "Base name of recursive set not an identifier: " ^ a);
1.22
1.23 local (*Checking the introduction rules*)
1.24 - val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
1.25 + val intr_sets = map (#2 o rule_concl_msg thy) intr_tms;
1.26 fun intr_ok set =
1.27 case head_of set of Const(a,recT) => a mem rec_names | _ => false;
1.28 in
1.29 val dummy = assert_all intr_ok intr_sets
1.30 (fn t => "Conclusion of rule does not name a recursive set: " ^
1.31 - Sign.string_of_term sign t);
1.32 + Sign.string_of_term thy t);
1.33 end;
1.34
1.35 val dummy = assert_all is_Free rec_params
1.36 (fn t => "Param in recursion term not a free variable: " ^
1.37 - Sign.string_of_term sign t);
1.38 + Sign.string_of_term thy t);
1.39
1.40 (*** Construct the fixedpoint definition ***)
1.41 val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
1.42 @@ -106,7 +105,7 @@
1.43
1.44 fun dest_tprop (Const("Trueprop",_) $ P) = P
1.45 | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
1.46 - Sign.string_of_term sign Q);
1.47 + Sign.string_of_term thy Q);
1.48
1.49 (*Makes a disjunct from an introduction rule*)
1.50 fun fp_part intr = (*quantify over rule's free vars except parameters*)
1.51 @@ -146,7 +145,7 @@
1.52 If no mutual recursion then it equals the one recursive set.
1.53 If mutual recursion then it differs from all the recursive sets. *)
1.54 val big_rec_base_name = space_implode "_" rec_base_names;
1.55 - val big_rec_name = Sign.intern_const sign big_rec_base_name;
1.56 + val big_rec_name = Sign.intern_const thy big_rec_base_name;
1.57
1.58
1.59 val dummy = conditional verbose (fn () =>
1.60 @@ -154,7 +153,7 @@
1.61
1.62 (*Forbid the inductive definition structure from clashing with a theory
1.63 name. This restriction may become obsolete as ML is de-emphasized.*)
1.64 - val dummy = deny (big_rec_base_name mem (Context.names_of sign))
1.65 + val dummy = deny (big_rec_base_name mem (Context.names_of thy))
1.66 ("Definition " ^ big_rec_base_name ^
1.67 " would clash with the theory of the same name!");
1.68
1.69 @@ -171,7 +170,7 @@
1.70
1.71 (*tracing: print the fixedpoint definition*)
1.72 val dummy = if !Ind_Syntax.trace then
1.73 - List.app (writeln o Sign.string_of_term sign o #2) axpairs
1.74 + List.app (writeln o Sign.string_of_term thy o #2) axpairs
1.75 else ()
1.76
1.77 (*add definitions of the inductive sets*)
1.78 @@ -188,13 +187,11 @@
1.79 | _ => big_rec_base_name::rec_names);
1.80
1.81
1.82 - val sign1 = sign_of thy1;
1.83 -
1.84 (********)
1.85 val dummy = writeln " Proving monotonicity...";
1.86
1.87 val bnd_mono =
1.88 - Goal.prove_global sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
1.89 + Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
1.90 (fn _ => EVERY
1.91 [rtac (Collect_subset RS bnd_monoI) 1,
1.92 REPEAT (ares_tac (basic_monos @ monos) 1)]);
1.93 @@ -252,7 +249,7 @@
1.94 val intrs =
1.95 (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
1.96 |> ListPair.map (fn (t, tacs) =>
1.97 - Goal.prove_global sign1 [] [] t
1.98 + Goal.prove_global thy1 [] [] t
1.99 (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
1.100 handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
1.101
1.102 @@ -281,7 +278,7 @@
1.103 (Thm.assume A RS elim)
1.104 |> Drule.standard';
1.105 fun mk_cases a = make_cases (*delayed evaluation of body!*)
1.106 - (simpset ()) (read_cterm (Thm.sign_of_thm elim) (a, propT));
1.107 + (simpset ()) (read_cterm (Thm.theory_of_thm elim) (a, propT));
1.108
1.109 fun induction_rules raw_induct thy =
1.110 let
1.111 @@ -328,7 +325,7 @@
1.112
1.113 val dummy = if !Ind_Syntax.trace then
1.114 (writeln "ind_prems = ";
1.115 - List.app (writeln o Sign.string_of_term sign1) ind_prems;
1.116 + List.app (writeln o Sign.string_of_term thy1) ind_prems;
1.117 writeln "raw_induct = "; print_thm raw_induct)
1.118 else ();
1.119
1.120 @@ -343,7 +340,7 @@
1.121 ORELSE' etac FalseE));
1.122
1.123 val quant_induct =
1.124 - Goal.prove_global sign1 [] ind_prems
1.125 + Goal.prove_global thy1 [] ind_prems
1.126 (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
1.127 (fn prems => EVERY
1.128 [rewrite_goals_tac part_rec_defs,
1.129 @@ -412,9 +409,9 @@
1.130
1.131 val dummy = if !Ind_Syntax.trace then
1.132 (writeln ("induct_concl = " ^
1.133 - Sign.string_of_term sign1 induct_concl);
1.134 + Sign.string_of_term thy1 induct_concl);
1.135 writeln ("mutual_induct_concl = " ^
1.136 - Sign.string_of_term sign1 mutual_induct_concl))
1.137 + Sign.string_of_term thy1 mutual_induct_concl))
1.138 else ();
1.139
1.140
1.141 @@ -427,7 +424,7 @@
1.142 val lemma = (*makes the link between the two induction rules*)
1.143 if need_mutual then
1.144 (writeln " Proving the mutual induction rule...";
1.145 - Goal.prove_global sign1 [] []
1.146 + Goal.prove_global thy1 [] []
1.147 (Logic.mk_implies (induct_concl, mutual_induct_concl))
1.148 (fn _ => EVERY
1.149 [rewrite_goals_tac part_rec_defs,
1.150 @@ -486,7 +483,7 @@
1.151
1.152 val mutual_induct_fsplit =
1.153 if need_mutual then
1.154 - Goal.prove_global sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
1.155 + Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
1.156 mutual_induct_concl
1.157 (fn prems => EVERY
1.158 [rtac (quant_induct RS lemma) 1,
1.159 @@ -500,8 +497,8 @@
1.160 The name "x.1" comes from the "RS spec" !*)
1.161 val inst =
1.162 case elem_frees of [_] => I
1.163 - | _ => instantiate ([], [(cterm_of sign1 (Var(("x",1), Ind_Syntax.iT)),
1.164 - cterm_of sign1 elem_tuple)]);
1.165 + | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
1.166 + cterm_of thy1 elem_tuple)]);
1.167
1.168 (*strip quantifier and the implication*)
1.169 val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));