removing deprecated rewriting signature / example (#2906)

2 files changed, 0 insertions, 164 deletions

diff --git a/proofs/signatures/core_rewrites.plf b/proofs/signatures/core_rewrites.plf
deleted file mode 100644
index ca2c1fa03..000000000
--- 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
index fbe593502..000000000
--- 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