src/HOL/Tools/inductive_set.ML
changeset 33458 ae1f5d89b082
parent 33368 b1cf34f1855c
child 33459 a4a38ed813f7
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Nov 05 22:08:47 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Nov 05 22:59:57 2009 +0100
     1.3 @@ -406,11 +406,11 @@
     1.4  
     1.5  fun add_ind_set_def
     1.6      {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     1.7 -    cs intros monos params cnames_syn ctxt =
     1.8 -  let (* FIXME proper naming convention: lthy *)
     1.9 -    val thy = ProofContext.theory_of ctxt;
    1.10 +    cs intros monos params cnames_syn lthy =
    1.11 +  let
    1.12 +    val thy = ProofContext.theory_of lthy;
    1.13      val {set_arities, pred_arities, to_pred_simps, ...} =
    1.14 -      PredSetConvData.get (Context.Proof ctxt);
    1.15 +      PredSetConvData.get (Context.Proof lthy);
    1.16      fun infer (Abs (_, _, t)) = infer t
    1.17        | infer (Const ("op :", _) $ t $ u) =
    1.18            infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
    1.19 @@ -446,9 +446,9 @@
    1.20          val (Us, U) = split_last (binder_types T);
    1.21          val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
    1.22            [Pretty.str "Argument types",
    1.23 -           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) Us)),
    1.24 +           Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) Us)),
    1.25             Pretty.str ("of " ^ s ^ " do not agree with types"),
    1.26 -           Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
    1.27 +           Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) paramTs)),
    1.28             Pretty.str "of declared parameters"]));
    1.29          val Ts = HOLogic.strip_ptupleT fs U;
    1.30          val c' = Free (s ^ "p",
    1.31 @@ -474,29 +474,29 @@
    1.32          Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
    1.33          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
    1.34      val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
    1.35 -    val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    1.36 -    val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    1.37 +    val monos' = map (to_pred [] (Context.Proof lthy)) monos;
    1.38 +    val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
    1.39        Inductive.add_ind_def
    1.40          {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
    1.41            coind = coind, no_elim = no_elim, no_ind = no_ind,
    1.42            skip_mono = skip_mono, fork_mono = fork_mono}
    1.43 -        cs' intros' monos' params1 cnames_syn' ctxt;
    1.44 +        cs' intros' monos' params1 cnames_syn' lthy;
    1.45  
    1.46      (* define inductive sets using previously defined predicates *)
    1.47 -    val (defs, ctxt2) = ctxt1
    1.48 +    val (defs, lthy2) = lthy1
    1.49        |> LocalTheory.conceal  (* FIXME ?? *)
    1.50        |> fold_map (LocalTheory.define Thm.internalK)
    1.51          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    1.52             fold_rev lambda params (HOLogic.Collect_const U $
    1.53               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    1.54             (cnames_syn ~~ cs_info ~~ preds))
    1.55 -      ||> LocalTheory.restore_naming ctxt1;
    1.56 +      ||> LocalTheory.restore_naming lthy1;
    1.57  
    1.58      (* prove theorems for converting predicate to set notation *)
    1.59 -    val ctxt3 = fold
    1.60 -      (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn ctxt =>
    1.61 +    val lthy3 = fold
    1.62 +      (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy =>
    1.63          let val conv_thm =
    1.64 -          Goal.prove ctxt (map (fst o dest_Free) params) []
    1.65 +          Goal.prove lthy (map (fst o dest_Free) params) []
    1.66              (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.67                (list_comb (p, params3),
    1.68                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
    1.69 @@ -505,29 +505,29 @@
    1.70              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    1.71                [def, mem_Collect_eq, split_conv]) 1))
    1.72          in
    1.73 -          ctxt |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.74 +          lthy |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.75              [Attrib.internal (K pred_set_conv_att)]),
    1.76                [conv_thm]) |> snd
    1.77 -        end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
    1.78 +        end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
    1.79  
    1.80      (* convert theorems to set notation *)
    1.81      val rec_name =
    1.82        if Binding.is_empty alt_name then
    1.83          Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
    1.84        else alt_name;
    1.85 -    val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn;  (* FIXME *)
    1.86 +    val cnames = map (LocalTheory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
    1.87      val (intr_names, intr_atts) = split_list (map fst intros);
    1.88 -    val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    1.89 -    val (intrs', elims', induct, ctxt4) =
    1.90 +    val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
    1.91 +    val (intrs', elims', induct, lthy4) =
    1.92        Inductive.declare_rules kind rec_name coind no_ind cnames
    1.93 -      (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
    1.94 -      (map (fn th => (to_set [] (Context.Proof ctxt3) th,
    1.95 +      (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
    1.96 +      (map (fn th => (to_set [] (Context.Proof lthy3) th,
    1.97           map fst (fst (Rule_Cases.get th)))) elims)
    1.98 -      raw_induct' ctxt3
    1.99 +      raw_induct' lthy3
   1.100    in
   1.101      ({intrs = intrs', elims = elims', induct = induct,
   1.102        raw_induct = raw_induct', preds = map fst defs},
   1.103 -     ctxt4)
   1.104 +     lthy4)
   1.105    end;
   1.106  
   1.107  val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;
   1.108 @@ -544,8 +544,10 @@
   1.109  val setup =
   1.110    Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
   1.111      "declare rules for converting between predicate and set notation" #>
   1.112 -  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
   1.113 -  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
   1.114 +  Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att)
   1.115 +    "convert rule to set notation" #>
   1.116 +  Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att)
   1.117 +    "convert rule to predicate notation" #>
   1.118    Attrib.setup @{binding code_ind_set}
   1.119      (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
   1.120      "introduction rules for executable predicates" #>
   1.121 @@ -562,10 +564,12 @@
   1.122  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
   1.123  
   1.124  val _ =
   1.125 -  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
   1.126 +  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
   1.127 +    (ind_set_decl false);
   1.128  
   1.129  val _ =
   1.130 -  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
   1.131 +  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
   1.132 +    (ind_set_decl true);
   1.133  
   1.134  end;
   1.135