ProjectRule now context dependent;
authorwenzelm
Tue Jun 13 23:41:34 2006 +0200 (2006-06-13)
changeset 19874cc4b2b882e4c
parent 19873 588329441a78
child 19875 7405ce9d4f25
ProjectRule now context dependent;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/Provers/project_rule.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:31 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:34 2006 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  val meta_spec = thm "meta_spec";
     1.5  
     1.6  fun projections rule =
     1.7 -  ProjectRule.projections rule
     1.8 +  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     1.9    |> map (standard #> RuleCases.save rule);
    1.10  
    1.11  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:31 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:34 2006 +0200
     2.3 @@ -316,22 +316,20 @@
     2.4  
     2.5  (* add_cases_induct *)
     2.6  
     2.7 -fun add_cases_induct infos induction =
     2.8 +fun add_cases_induct infos induction thy =
     2.9    let
    2.10 -    val n = length (HOLogic.dest_concls (Thm.concl_of induction));
    2.11 -    fun proj i = ProjectRule.project induction (i + 1);
    2.12 +    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
    2.13  
    2.14      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    2.15 -      [(("", proj index), [InductAttrib.induct_type name]),
    2.16 +      [(("", nth inducts index), [InductAttrib.induct_type name]),
    2.17         (("", exhaustion), [InductAttrib.cases_type name])];
    2.18      fun unnamed_rule i =
    2.19 -      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
    2.20 +      (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
    2.21    in
    2.22 -    PureThy.add_thms
    2.23 +    thy |> PureThy.add_thms
    2.24        (List.concat (map named_rules infos) @
    2.25 -        map unnamed_rule (length infos upto n - 1)) #> snd #>
    2.26 -    PureThy.add_thmss [(("inducts",
    2.27 -      map (proj #> standard #> RuleCases.save induction) (0 upto n - 1)), [])] #> snd
    2.28 +        map unnamed_rule (length infos upto length inducts - 1)) |> snd
    2.29 +    |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
    2.30    end;
    2.31  
    2.32  
    2.33 @@ -801,7 +799,7 @@
    2.34        ||>> apply_theorems [raw_induction];
    2.35      val sign = Theory.sign_of thy1;
    2.36  
    2.37 -    val induction' = freezeT induction;
    2.38 +    val induction' = Thm.freezeT induction;
    2.39  
    2.40      fun err t = error ("Ill-formed predicate in induction rule: " ^
    2.41        Sign.string_of_term sign t);
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jun 13 23:41:31 2006 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jun 13 23:41:34 2006 +0200
     3.3 @@ -436,17 +436,19 @@
     3.4      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
     3.5  
     3.6      val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
     3.7 -    val induct_specs =
     3.8 -      if no_induct then I
     3.9 +    fun induct_specs thy =
    3.10 +      if no_induct then thy
    3.11        else
    3.12          let
    3.13 -          val rules = names ~~ map (ProjectRule.project induct) (1 upto length names);
    3.14 +          val ctxt = ProofContext.init thy;
    3.15 +          val rules = names ~~ ProjectRule.projects ctxt (1 upto length names) induct;
    3.16            val inducts = map (RuleCases.save induct o standard o #2) rules;
    3.17          in
    3.18 -          PureThy.add_thms (rules |> map (fn (name, th) =>
    3.19 -            (("", th), [RuleCases.consumes 1, induct_att name]))) #> snd #>
    3.20 -          PureThy.add_thmss
    3.21 -            [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] #> snd
    3.22 +          thy
    3.23 +          |> PureThy.add_thms (rules |> map (fn (name, th) =>
    3.24 +            (("", th), [RuleCases.consumes 1, induct_att name]))) |> snd
    3.25 +          |> PureThy.add_thmss
    3.26 +            [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] |> snd
    3.27          end;
    3.28    in Library.apply cases_specs #> induct_specs end;
    3.29  
     4.1 --- a/src/Provers/project_rule.ML	Tue Jun 13 23:41:31 2006 +0200
     4.2 +++ b/src/Provers/project_rule.ML	Tue Jun 13 23:41:34 2006 +0200
     4.3 @@ -17,8 +17,9 @@
     4.4  
     4.5  signature PROJECT_RULE =
     4.6  sig
     4.7 -  val project: thm -> int -> thm
     4.8 -  val projections: thm -> thm list
     4.9 +  val project: Proof.context -> int -> thm -> thm
    4.10 +  val projects: Proof.context -> int list -> thm -> thm list
    4.11 +  val projections: Proof.context -> thm -> thm list
    4.12  end;
    4.13  
    4.14  functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
    4.15 @@ -28,9 +29,7 @@
    4.16  fun conj2 th = th RS Data.conjunct2;
    4.17  fun imp th = th RS Data.mp;
    4.18  
    4.19 -val freeze = Drule.zero_var_indexes #> Drule.freeze_all;
    4.20 -
    4.21 -fun project rule i =
    4.22 +fun projects ctxt is raw_rule =
    4.23    let
    4.24      fun proj 1 th = the_default th (try conj1 th)
    4.25        | proj k th = proj (k - 1) (conj2 th);
    4.26 @@ -38,24 +37,27 @@
    4.27        (case try imp th of
    4.28          NONE => (k, th)
    4.29        | SOME th' => prems (k + 1) th');
    4.30 -  in
    4.31 -    rule
    4.32 -    |> freeze
    4.33 -    |> proj i
    4.34 -    |> prems 0 |-> (fn k =>
    4.35 -      Thm.permute_prems 0 (~ k)
    4.36 -      #> Drule.standard'
    4.37 -      #> RuleCases.save rule
    4.38 -      #> RuleCases.add_consumes k)
    4.39 -  end;
    4.40 +    val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
    4.41 +    fun result i =
    4.42 +      rule
    4.43 +      |> proj i
    4.44 +      |> prems 0 |-> (fn k =>
    4.45 +        Thm.permute_prems 0 (~ k)
    4.46 +        #> ProofContext.export ctxt' ctxt
    4.47 +        #> Drule.zero_var_indexes
    4.48 +        #> RuleCases.save raw_rule
    4.49 +        #> RuleCases.add_consumes k);
    4.50 +  in map result is end;
    4.51  
    4.52 -fun projections rule =
    4.53 +fun project ctxt i th = hd (projects ctxt [i] th);
    4.54 +
    4.55 +fun projections ctxt raw_rule =
    4.56    let
    4.57      fun projs k th =
    4.58        (case try conj2 th of
    4.59          NONE => k
    4.60        | SOME th' => projs (k + 1) th');
    4.61 -    val n = projs 1 (freeze rule);
    4.62 -  in map (project rule) (1 upto n) end;
    4.63 +    val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
    4.64 +  in projects ctxt (1 upto projs 1 rule) raw_rule end;
    4.65  
    4.66  end;