diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /proofs/signatures/core_rewrites.plf | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'proofs/signatures/core_rewrites.plf')
-rw-r--r-- | proofs/signatures/core_rewrites.plf | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf new file mode 100644 index 000000000..ca2c1fa03 --- /dev/null +++ b/proofs/signatures/core_rewrites.plf @@ -0,0 +1,123 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;; Rewrite rules +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; t rewrites to t' +(declare rw_term + (! s sort + (! t (term s) + (! t' (term s) + type)))) + +(declare rw_formula + (! f formula + (! f' formula + type))) + + +(declare apply_rw_formula + (! f formula + (! f' formula + (! rw (rw_formula f f') + (! fh (th_holds f) + (th_holds f')))))) + + +;; Identity rewrite rules +(declare rw_term_id + (! s sort + (! t (term s) + (rw_term s t t)))) + +(declare rw_term_trans + (! s sort + (! t1 (term s) + (! t2 (term s) + (! t3 (term s) + (! rw12 (rw_term _ t1 t2) + (! rw23 (rw_term _ t2 t3) + (rw_term s t1 t3)))))))) + +;; rw_symmetry + +(declare rw_formula_trans + (! f1 formula + (! f2 formula + (! f3 formula + (! rw1 (rw_formula f1 f2) + (! rw2 (rw_formula f2 f3) + (rw_formula f1 f3))))))) + + +(declare rw_op1_id + (! s sort + (! a (term s) + (! a' (term s) + (! rw (rw_term _ a a') + (! op term_op1 + (rw_term _ (op _ a) (op _ a')))))))) + +(declare rw_op2_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (! op term_op2 + (rw_term _ (op _ a b) (op _ a' b'))))))))))) + +(declare rw_pred1_id + (! s sort + (! a (term s) + (! a' (term s) + (! rw (rw_term _ a a') + (! op op_pred1 + (rw_formula (op _ a) (op _ a')))))))) + +(declare rw_pred2_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (! op op_pred2 + (rw_formula (op _ a b) (op _ a' b'))))))))))) + +(declare rw_eq_id + (! s sort + (! a (term s) + (! a' (term s) + (! b (term s) + (! b' (term s) + (! rw (rw_term _ a a') + (! rw (rw_term _ b b') + (rw_formula (= s a b) (= s a' b')))))))))) + +(declare rw_formula_op1_id + (! f formula + (! f' formula + (! frw (rw_formula f f') + (! op formula_op1 + (rw_formula (op f) (op f'))))))) + +(declare rw_formula_op2_id + (! f1 formula + (! f1' formula + (! f2 formula + (! f2' formula + (! frw1 (rw_formula f1 f1') + (! frw2 (rw_formula f2 f2') + (! op formula_op2 + (rw_formula (op f1 f2) (op f1' f2')))))))))) + + +(apply_rw_formula + (! f formula + (! f' formula + (! r (rw_formula f f') + (! h (th_holds f) + (th_holds f'))))))
\ No newline at end of file |