src/Tools/project_rule.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 33368 b1cf34f1855c
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 22568
diff changeset
     1
(*  Title:      Tools/project_rule.ML
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
     3
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
     4
Transform mutual rule:
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 22568
diff changeset
     5
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
     6
  HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 22568
diff changeset
     7
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
     8
into projection:
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 22568
diff changeset
     9
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    10
  xi:Ai ==> HH ==> Pi xi
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    11
*)
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    12
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    13
signature PROJECT_RULE_DATA =
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    14
sig
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    15
  val conjunct1: thm
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    16
  val conjunct2: thm
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    17
  val mp: thm
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    18
end;
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    19
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    20
signature PROJECT_RULE =
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    21
sig
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    22
  val project: Proof.context -> int -> thm -> thm
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    23
  val projects: Proof.context -> int list -> thm -> thm list
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    24
  val projections: Proof.context -> thm -> thm list
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    25
end;
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    26
32172
c4e55f30d527 renamed functor ProjectRuleFun to Project_Rule;
wenzelm
parents: 31794
diff changeset
    27
functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE =
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    28
struct
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    29
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    30
fun conj1 th = th RS Data.conjunct1;
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    31
fun conj2 th = th RS Data.conjunct2;
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    32
fun imp th = th RS Data.mp;
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    33
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    34
fun projects ctxt is raw_rule =
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    35
  let
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    36
    fun proj 1 th = the_default th (try conj1 th)
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    37
      | proj k th = proj (k - 1) (conj2 th);
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    38
    fun prems k th =
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    39
      (case try imp th of
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    40
        NONE => (k, th)
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    41
      | SOME th' => prems (k + 1) th');
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30160
diff changeset
    42
    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    43
    fun result i =
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    44
      rule
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    45
      |> proj i
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    46
      |> prems 0 |-> (fn k =>
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    47
        Thm.permute_prems 0 (~ k)
19905
7f480338b66e ProofContext.export: singleton;
wenzelm
parents: 19897
diff changeset
    48
        #> singleton (Variable.export ctxt' ctxt)
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    49
        #> Drule.zero_var_indexes
33368
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32172
diff changeset
    50
        #> Rule_Cases.save raw_rule
b1cf34f1855c modernized structure Rule_Cases;
wenzelm
parents: 32172
diff changeset
    51
        #> Rule_Cases.add_consumes k);
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    52
  in map result is end;
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    53
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    54
fun project ctxt i th = hd (projects ctxt [i] th);
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    55
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    56
fun projections ctxt raw_rule =
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    57
  let
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    58
    fun projs k th =
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    59
      (case try conj2 th of
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    60
        NONE => k
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    61
      | SOME th' => projs (k + 1) th');
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30160
diff changeset
    62
    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
19874
cc4b2b882e4c ProjectRule now context dependent;
wenzelm
parents: 18483
diff changeset
    63
  in projects ctxt (1 upto projs 1 rule) raw_rule end;
18483
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    64
c3027c8df1bf Transform mutual rule into projection.
wenzelm
parents:
diff changeset
    65
end;