author | berghofe |
Sat, 02 Feb 2002 13:26:51 +0100 | |
changeset 12866 | c00df7765656 |
parent 12237 | 39aeccee9e1c |
child 12906 | 165f4e1937f4 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proof_rewrite_rules.ML |
2 |
ID: $Id$ |
|
11539 | 3 |
Author: Stefan Berghofer, TU Muenchen |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
11522 | 5 |
|
6 |
Simplification function for partial proof terms involving |
|
7 |
meta level rules. |
|
8 |
*) |
|
9 |
||
10 |
signature PROOF_REWRITE_RULES = |
|
11 |
sig |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
12 |
val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
13 |
val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list |
12237 | 14 |
val setup : (theory -> theory) list |
11522 | 15 |
end; |
16 |
||
17 |
structure ProofRewriteRules : PROOF_REWRITE_RULES = |
|
18 |
struct |
|
19 |
||
20 |
open Proofterm; |
|
21 |
||
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
22 |
fun rew b = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
23 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
24 |
fun ? x = if b then Some x else None; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
25 |
fun ax (prf as PAxm (s, prop, _)) Ts = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
26 |
if b then PAxm (s, prop, Some Ts) else prf; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
27 |
fun ty T = if b then |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
28 |
let val Type (_, [Type (_, [U, _]), _]) = T |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
29 |
in Some T end |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
30 |
else None; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
31 |
val equal_intr_axm = ax equal_intr_axm []; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
32 |
val equal_elim_axm = ax equal_elim_axm []; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
33 |
val symmetric_axm = ax symmetric_axm [propT]; |
11522 | 34 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
35 |
fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
36 |
(PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
37 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
38 |
(PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
39 |
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
40 |
(PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
41 |
Some (equal_intr_axm % B % A %% prf2 %% prf1) |
12002 | 42 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
43 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %% |
12002 | 44 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) % |
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
45 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
46 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
47 |
Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) |
12002 | 48 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
49 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
50 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
51 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) % |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
52 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
53 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
54 |
Some (tg %> B %% (equal_elim_axm %> A %> B %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
55 |
(symmetric_axm % ? B % ? A %% prf1) %% prf2)) |
11522 | 56 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
57 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
11612 | 58 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
59 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %% |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
60 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
61 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
62 |
val _ $ A $ C = Envir.beta_norm X; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
63 |
val _ $ B $ D = Envir.beta_norm Y |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
64 |
in Some (AbsP ("H1", ? X, AbsP ("H2", ? B, |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
65 |
equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
66 |
(PBound 1 %% (equal_elim_axm %> B %> A %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
67 |
(symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0))))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
68 |
end |
11522 | 69 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
70 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
71 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
72 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
73 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
74 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
75 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
76 |
val _ $ A $ C = Envir.beta_norm Y; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
77 |
val _ $ B $ D = Envir.beta_norm X |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
78 |
in Some (AbsP ("H1", ? X, AbsP ("H2", ? A, |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
79 |
equal_elim_axm %> D %> C %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
80 |
(symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
81 |
%% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0))))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
82 |
end |
11522 | 83 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
84 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
11612 | 85 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %% |
86 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
87 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
88 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
89 |
val Const (_, T) $ P = Envir.beta_norm X; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
90 |
val _ $ Q = Envir.beta_norm Y; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
91 |
in Some (AbsP ("H", ? X, Abst ("x", ty T, |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
92 |
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
93 |
(incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
94 |
end |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
95 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
96 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
97 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
98 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
99 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
100 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
101 |
let |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
102 |
val Const (_, T) $ P = Envir.beta_norm X; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
103 |
val _ $ Q = Envir.beta_norm Y; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
104 |
val t = incr_boundvars 1 P $ Bound 0; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
105 |
val u = incr_boundvars 1 Q $ Bound 0 |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
106 |
in Some (AbsP ("H", ? X, Abst ("x", ty T, |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
107 |
equal_elim_axm %> t %> u %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
108 |
(symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0)) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
109 |
%% (PBound 0 %> Bound 0)))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
110 |
end |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
111 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
112 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
113 |
(PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
114 |
Some (equal_elim_axm %> B %> C %% prf2 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
115 |
(equal_elim_axm %> A %> B %% prf1 %% prf3)) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
116 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
117 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
118 |
(PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
119 |
Some (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
120 |
(equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3)) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
121 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
122 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
123 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
124 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
125 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
126 |
(PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
127 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
128 |
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
129 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = Some prf |
11522 | 130 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
131 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
132 |
(PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
133 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
134 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
135 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
136 |
Some (equal_elim_axm %> C %> D %% prf2 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
137 |
(equal_elim_axm %> A %> C %% prf3 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
138 |
(equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4))) |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
139 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
140 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
141 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
142 |
(PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A $ C) % Some (_ $ B $ D) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
143 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
144 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
145 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
146 |
Some (equal_elim_axm %> A %> B %% prf1 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
147 |
(equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
148 |
(equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4))) |
11522 | 149 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
150 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
151 |
(PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
152 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
153 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
154 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
155 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
156 |
Some (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
157 |
(equal_elim_axm %> B %> D %% prf3 %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
158 |
(equal_elim_axm %> A %> B %% prf1 %% prf4))) |
11522 | 159 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
160 |
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
161 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
162 |
(PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ B $ D) % Some (_ $ A $ C) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
163 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
164 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
165 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==", _)) % _ % _ % _ %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
166 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) = |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
167 |
Some (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
168 |
(equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %% |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
169 |
(equal_elim_axm %> C %> D %% prf2 %% prf4))) |
11522 | 170 |
|
12866
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
171 |
| rew' _ _ = None; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
172 |
in rew' end; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
173 |
|
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
174 |
fun rprocs b = [("Pure/meta_equality", rew b)]; |
c00df7765656
Rewrite procedure now works for both compact and full proof objects.
berghofe
parents:
12237
diff
changeset
|
175 |
val setup = [Proofterm.add_prf_rprocs (rprocs false)]; |
11522 | 176 |
|
177 |
end; |