src/HOL/Tools/inductive.ML
 changeset 42361 23f352990944 parent 42358 b47d41d9f4b5 child 42364 8c674b3b8e44
```     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Apr 16 15:47:52 2011 +0200
1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Apr 16 16:15:37 2011 +0200
1.3 @@ -149,7 +149,7 @@
1.4  fun print_inductives ctxt =
1.5    let
1.6      val (tab, monos) = get_inductives ctxt;
1.7 -    val space = Consts.space_of (ProofContext.consts_of ctxt);
1.8 +    val space = Consts.space_of (Proof_Context.consts_of ctxt);
1.9    in
1.10      [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
1.11       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
1.12 @@ -294,7 +294,7 @@
1.13      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
1.14      val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
1.15      val rule' = Logic.list_implies (prems, concl);
1.16 -    val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems;
1.17 +    val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
1.18      val arule = list_all_free (params', Logic.list_implies (aprems, concl));
1.19
1.20      fun check_ind err t = case dest_predicate cs params t of
1.21 @@ -375,7 +375,7 @@
1.22          (*Not ares_tac, since refl must be tried before any equality assumptions;
1.23            backtracking may occur if the premises have extra variables!*)
1.24          DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
1.25 -       |> singleton (ProofContext.export ctxt ctxt')) intr_ts
1.26 +       |> singleton (Proof_Context.export ctxt ctxt')) intr_ts
1.27
1.28    in (intrs, unfold) end;
1.29
1.30 @@ -421,7 +421,7 @@
1.31               REPEAT (FIRSTGOAL (eresolve_tac rules2)),
1.32               EVERY (map (fn prem =>
1.33                 DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
1.34 -          |> singleton (ProofContext.export ctxt'' ctxt'''),
1.35 +          |> singleton (Proof_Context.export ctxt'' ctxt'''),
1.36           map #2 c_intrs, length Ts)
1.37        end
1.38
1.39 @@ -487,7 +487,7 @@
1.40                THEN prove_intr2 last_c_intr
1.41              end))
1.42          |> rulify
1.43 -        |> singleton (ProofContext.export ctxt' ctxt'')
1.44 +        |> singleton (Proof_Context.export ctxt' ctxt'')
1.45        end;
1.46    in
1.47      map2 prove_eq cs elims
1.48 @@ -510,7 +510,7 @@
1.49
1.50  fun mk_cases ctxt prop =
1.51    let
1.52 -    val thy = ProofContext.theory_of ctxt;
1.53 +    val thy = Proof_Context.theory_of ctxt;
1.54      val ss = simpset_of ctxt;
1.55
1.56      fun err msg =
1.57 @@ -536,7 +536,7 @@
1.58
1.59  fun gen_inductive_cases prep_att prep_prop args lthy =
1.60    let
1.61 -    val thy = ProofContext.theory_of lthy;
1.62 +    val thy = Proof_Context.theory_of lthy;
1.63      val facts = args |> Par_List.map (fn ((a, atts), props) =>
1.64        ((a, map (prep_att thy) atts),
1.65          Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
1.66 @@ -555,7 +555,7 @@
1.67            val (_, ctxt') = Variable.add_fixes fixes ctxt;
1.68            val props = Syntax.read_props ctxt' raw_props;
1.69            val ctxt'' = fold Variable.declare_term props ctxt';
1.70 -          val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
1.71 +          val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
1.72          in Method.erule 0 rules end))
1.73      "dynamic case analysis on predicates";
1.74
1.75 @@ -563,7 +563,7 @@
1.76
1.77  fun mk_simp_eq ctxt prop =
1.78    let
1.79 -    val thy = ProofContext.theory_of ctxt
1.80 +    val thy = Proof_Context.theory_of ctxt
1.81      val ctxt' = Variable.auto_fixes prop ctxt
1.82      val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
1.83      val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop)
1.84 @@ -588,7 +588,7 @@
1.85
1.86  fun gen_inductive_simps prep_att prep_prop args lthy =
1.87    let
1.88 -    val thy = ProofContext.theory_of lthy;
1.89 +    val thy = Proof_Context.theory_of lthy;
1.90      val facts = args |> map (fn ((a, atts), props) =>
1.91        ((a, map (prep_att thy) atts),
1.92          map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
1.93 @@ -603,7 +603,7 @@
1.94      fp_def rec_preds_defs ctxt ctxt''' =
1.95    let
1.96      val _ = clean_message quiet_mode "  Proving the induction rule ...";
1.97 -    val thy = ProofContext.theory_of ctxt;
1.98 +    val thy = Proof_Context.theory_of ctxt;
1.99
1.100      (* predicates for induction rule *)
1.101
1.102 @@ -702,7 +702,7 @@
1.103              rewrite_goals_tac simp_thms',
1.104              atac 1])])
1.105
1.106 -  in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end;
1.107 +  in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
1.108
1.109
1.110
1.111 @@ -779,7 +779,7 @@
1.112             (Const (fp_name, (predT --> predT) --> predT) \$ fp_fun)))
1.113        ||> Local_Theory.restore_naming lthy;
1.114      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
1.115 -      (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
1.116 +      (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
1.117      val specs =
1.118        if length cs < 2 then []
1.119        else
1.120 @@ -801,7 +801,7 @@
1.121      val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
1.122      val (_, lthy'''') =
1.123        Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
1.124 -        ProofContext.export lthy''' lthy'' [mono]) lthy'';
1.125 +        Proof_Context.export lthy''' lthy'' [mono]) lthy'';
1.126
1.127    in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
1.128      list_comb (rec_const, params), preds, argTs, bs, xs)
1.129 @@ -903,7 +903,7 @@
1.130      val raw_induct = zero_var_indexes
1.131        (if no_ind then Drule.asm_rl
1.132         else if coind then
1.133 -         singleton (ProofContext.export lthy2 lthy1)
1.134 +         singleton (Proof_Context.export lthy2 lthy1)
1.135             (rotate_prems ~1 (Object_Logic.rulify
1.136               (fold_rule rec_preds_defs
1.137                 (rewrite_rule simp_thms'''
1.138 @@ -942,7 +942,7 @@
1.139      (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
1.140      cnames_syn pnames spec monos lthy =
1.141    let
1.142 -    val thy = ProofContext.theory_of lthy;
1.143 +    val thy = Proof_Context.theory_of lthy;
1.144      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
1.145
1.146
1.147 @@ -979,7 +979,7 @@
1.148      val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
1.149      val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
1.150      val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
1.151 -    val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
1.152 +    val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
1.153
1.154      fun close_rule r = list_all_free (rev (fold_aterms
1.155        (fn t as Free (v as (s, _)) =>
1.156 @@ -998,7 +998,7 @@
1.157  fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
1.158    let
1.159      val ((vars, intrs), _) = lthy
1.160 -      |> ProofContext.set_mode ProofContext.mode_abbrev
1.161 +      |> Proof_Context.set_mode Proof_Context.mode_abbrev
1.162        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
1.163      val (cs, ps) = chop (length cnames_syn) vars;
1.164      val monos = Attrib.eval_thms lthy raw_monos;
1.165 @@ -1020,7 +1020,7 @@
1.166        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
1.167        |> Local_Theory.exit;
1.168      val info = #2 (the_inductive ctxt' name);
1.169 -  in (info, ProofContext.theory_of ctxt') end;
1.170 +  in (info, Proof_Context.theory_of ctxt') end;
1.171
1.172
1.173  (* read off arities of inductive predicates from raw induction rule *)
```