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
|
|
12 |
val rprocs : (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
|
12237
|
13 |
val setup : (theory -> theory) list
|
11522
|
14 |
end;
|
|
15 |
|
|
16 |
structure ProofRewriteRules : PROOF_REWRITE_RULES =
|
|
17 |
struct
|
|
18 |
|
|
19 |
open Proofterm;
|
|
20 |
|
11612
|
21 |
fun rew _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
|
|
22 |
(PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = Some prf
|
|
23 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
|
|
24 |
(PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = Some prf
|
|
25 |
| rew _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
26 |
(PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
|
|
27 |
Some (equal_intr_axm % B % A %% prf2 %% prf1)
|
11522
|
28 |
|
12002
|
29 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
|
|
30 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
|
|
31 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
|
|
32 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
|
|
33 |
Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
|
|
34 |
|
|
35 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
|
|
36 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
37 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
|
|
38 |
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
|
|
39 |
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
|
|
40 |
Some (tg %> B %% (equal_elim_axm %> A %> B %%
|
|
41 |
(symmetric_axm % None % None %% prf1) %% prf2))
|
|
42 |
|
11612
|
43 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
|
|
44 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
|
|
45 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
|
|
46 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
|
11522
|
47 |
let
|
|
48 |
val _ $ A $ C = Envir.beta_norm X;
|
|
49 |
val _ $ B $ D = Envir.beta_norm Y
|
|
50 |
in Some (AbsP ("H1", None, AbsP ("H2", None,
|
11612
|
51 |
equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
|
|
52 |
(PBound 1 %% (equal_elim_axm %> B %> A %%
|
|
53 |
(symmetric_axm % None % None %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
|
11522
|
54 |
end
|
|
55 |
|
11612
|
56 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
|
|
57 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
58 |
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
|
|
59 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%
|
|
60 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
|
11522
|
61 |
let
|
|
62 |
val _ $ A $ C = Envir.beta_norm Y;
|
|
63 |
val _ $ B $ D = Envir.beta_norm X
|
|
64 |
in Some (AbsP ("H1", None, AbsP ("H2", None,
|
11612
|
65 |
equal_elim_axm %> D %> C %%
|
|
66 |
(symmetric_axm % None % None %% incr_pboundvars 2 0 prf2)
|
|
67 |
%% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
|
11522
|
68 |
end
|
|
69 |
|
11612
|
70 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
|
|
71 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
|
|
72 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %%
|
|
73 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
|
11522
|
74 |
let
|
|
75 |
val _ $ P = Envir.beta_norm X;
|
|
76 |
val _ $ Q = Envir.beta_norm Y;
|
|
77 |
in Some (AbsP ("H", None, Abst ("x", None,
|
11612
|
78 |
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
|
|
79 |
(incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
|
11522
|
80 |
end
|
|
81 |
|
11612
|
82 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
|
|
83 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
84 |
(PAxm ("ProtoPure.combination", _, _) % Some (Const ("all", _)) % _ % _ % _ %%
|
|
85 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %%
|
|
86 |
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
|
11522
|
87 |
let
|
|
88 |
val _ $ P = Envir.beta_norm X;
|
|
89 |
val _ $ Q = Envir.beta_norm Y;
|
|
90 |
in Some (AbsP ("H", None, Abst ("x", None,
|
11612
|
91 |
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
|
|
92 |
(symmetric_axm % None % None %% (incr_pboundvars 1 1 prf %> Bound 0))
|
|
93 |
%% (PBound 0 %> Bound 0))))
|
11522
|
94 |
end
|
|
95 |
|
11612
|
96 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
|
|
97 |
(PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2) %% prf3) =
|
|
98 |
Some (equal_elim_axm %> B %> C %% prf2 %%
|
|
99 |
(equal_elim_axm %> A %> B %% prf1 %% prf3))
|
|
100 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some A % Some C %%
|
|
101 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
102 |
(PAxm ("ProtoPure.transitive", _, _) % _ % Some B % _ %% prf1 %% prf2)) %% prf3) =
|
|
103 |
Some (equal_elim_axm %> B %> C %% (symmetric_axm % None % None %% prf1) %%
|
|
104 |
(equal_elim_axm %> A %> B %% (symmetric_axm % None % None %% prf2) %% prf3))
|
11522
|
105 |
|
11612
|
106 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
|
|
107 |
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = Some prf
|
|
108 |
| rew _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
|
|
109 |
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
|
|
110 |
(PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = Some prf
|
11522
|
111 |
|
|
112 |
| rew _ _ = None;
|
|
113 |
|
|
114 |
val rprocs = [("Pure/meta_equality", rew)];
|
12237
|
115 |
val setup = [Proofterm.add_prf_rprocs rprocs];
|
11522
|
116 |
|
|
117 |
end;
|