equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/rewrite_hol_proof.ML |
1 (* Title: HOL/Tools/rewrite_hol_proof.ML |
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
2 Author: Stefan Berghofer, TU Muenchen |
4 |
3 |
5 Rewrite rules for HOL proofs |
4 Rewrite rules for HOL proofs |
6 *) |
5 *) |
7 |
6 |
69 \ (cong % TYPE('T=>bool) % TYPE('T) % \ |
68 \ (cong % TYPE('T=>bool) % TYPE('T) % \ |
70 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ |
69 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ |
71 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
70 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
72 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
71 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
73 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
72 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
74 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", |
73 \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))", |
75 |
74 |
76 "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ |
75 "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ |
77 \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ |
76 \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ |
78 \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ |
77 \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ |
79 \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ |
78 \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ |
83 \ (cong % TYPE('T=>bool) % TYPE('T) % \ |
82 \ (cong % TYPE('T=>bool) % TYPE('T) % \ |
84 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ |
83 \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ |
85 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
84 \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ |
86 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
85 \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ |
87 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
86 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ |
88 \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf3))", |
87 \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))", |
89 |
88 |
90 (** rewriting on bool: insert proper congruence rules for logical connectives **) |
89 (** rewriting on bool: insert proper congruence rules for logical connectives **) |
91 |
90 |
92 (* All *) |
91 (* All *) |
93 |
92 |