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 *)