removing deprecated rewriting signature / example (#2906)

diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf
deleted file mode 100644 (file)
index ca2c1fa..0000000
--- a/proofs/signatures/core_rewrites.plf
+++ /dev/null
@@ -1,123 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;;;;;;;;;;; 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

diff --git a/proofs/signatures/ex_bv_rewrite.plf b/proofs/signatures/ex_bv_rewrite.plf
deleted file mode 100644 (file)
index fbe5935..0000000
--- a/proofs/signatures/ex_bv_rewrite.plf
+++ /dev/null
@@ -1,41 +0,0 @@
-(check
-(% x var_bv
-(% y var_bv
-(% a var_bv
-(% A0 (th_holds true)
-(% A1 (th_holds
-      (= (BitVec 1) (a_var_bv 1 x)
-                   (bvnot 1  (bvxnor 1 (bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b1 bvn)))
-                                       (bvxor 1 (a_var_bv 1 a) (a_bv 1 (bvc b0 bvn))) ))))
-(: (th_holds
-      (= (BitVec 1) (a_var_bv 1 x)
-                   (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a))))
-
-;; print rewritten assertions
-
-(@ ones (a_bv 1 (bvc b1 bvn))
-(@ zero (a_bv 1 (bvc b0 bvn))
-(@ xorone (bvxor 1 (a_var_bv 1 a) ones)
-(@ xorzero (bvxor 1 (a_var_bv 1 a) zero)
-(@ t1 (bvxor 1 xorone xorzero)
-(@ t2 (bvxnor 1 xorone xorzero)
-(@ t3 (bvnot 1 t2)
-(@ t4 (bvnot 1 t1)
-(@ t5 (bvxor 1 (bvnot 1 (a_var_bv 1 a)) (a_var_bv 1 a))
-;; adding identity rewrite proofs
-(@ xor_onerw (rw_term_id 1 xorone)
-(@ xor_zerorw (rw_term_id 1 xorzero)
-(@ rw1 (xnor_elim 1 _ _ _ _ xor_onerw xor_zerorw) ;; bvxnor t1 t2 -> bvnot (bvxor t1 t2)
-(@ rw2 (xor_zero 1 _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 zero))
-(@ rw3 (xor_one 1  _ _ _ _ (rw_term_id 1 (a_var_bv 1 a)) (rw_term_id 1 ones))
-(@ rw4 (rw_bvop2_id 1 _ _ _ _ rw3 rw2 bvxor) ;; bvxor t1 t2 -> bvxor t1' t2'
-(@ rw5 (rw_bvop1_id 1 _ _ rw4 bvnot) ;; bvnot (bvxor t1 t2) -> bvnot (bvxor t1' t2')
-(@ rw6 (rw_term_trans 1  _ _ _ rw1 rw5) ;; bvxnor t1 t2 -> bvnot (bvxor t1' t2')
-(@ rw7 (rw_bvop1_id 1 _ _ rw6 bvnot) ;; (bvnot (bvxnor t1 t2)) ->(bvnot (bvnot (bvxor t1' t2')))
-(@ rw8 (not_idemp 1 _ _ (rw_term_id 1 t5)) ;; (bvnot (bvnot (bvxor t1' t2'))) -> bvxor t1' t2'
-(@ rw9 (rw_term_trans 1 _ _ _ rw7 rw8) ;; (bvnot (bvxnor t1 t2)) -> (bvxor t1' t2')
-(@ rw10 (rw_term_id 1 (a_var_bv 1 x))
-(@ rw11 (rw_eq_id 1 _ _ _ _ rw10 rw9) ;;  x = t1 => x = t'
-(apply_rw_formula _ _ rw11 A1)
-
-)))))))))))))))))))))))))))))
\ No newline at end of file