Support for type variables

IsaRARE.thy

@@ -244,7 +244,6 @@ val _ =  Outer_Syntax.local_theory \<^command_keyword>\<open>parse_rare_file\<cl
 
 declare[[IsaRARE_debug=false]]
 
-
 (*parse_rare_file "~/Downloads/int2.smt2" "HOL.Real" "TestKey2"*)
 
 
@@ -279,6 +278,8 @@ parse_rare_file "Tests/level2a_rewrites" "HOL.Real" "Level2a_Rewrites"
 parse_rare_file "Tests/level2b_rewrites" "HOL.Real" "Level2b_Rewrites"
 parse_rare_file "Tests/level2_rewrites" "HOL.Real" "Level2_Rewrites"
 parse_rare_file "Tests/level3a_rewrites" "HOL.Real" "Level3a_Rewrites"
+parse_rare_file "Tests/level3b_rewrites" "HOL.Real" "Level3b_Rewrites"
+parse_rare_file "Tests/level3c_rewrites" "HOL.Real" "Level3c_Rewrites"
 
 
 

Tests/RareAsEunoiaTests/level0_rewrites.eo

@@ -0,0 +1,360 @@
+;;;;;;;;;;;;;;;;;
+;; Arith
+;;;;;;;;;;;;;;;;;
+
+(declare-rule arith-int-div-total ((t1 Int) (s1 Int))
+  :premises ((= (= s1 0) false))
+  :args (t1 s1)
+  :conclusion (= (div t1 s1) (div_total t1 s1))
+)
+(declare-rule arith-int-div-total-one ((t1 Int))
+  :args (t1)
+  :conclusion (= (div_total t1 1) t1)
+)
+(declare-rule arith-int-div-total-zero ((t1 Int))
+  :args (t1)
+  :conclusion (= (div_total t1 0) 0)
+)
+(declare-rule arith-int-div-total-neg ((t1 Int) (s1 Int))
+  :premises ((= (< s1 0) true))
+  :args (t1 s1)
+  :conclusion (= (div_total t1 s1) (- (div_total t1 (- s1))))
+)
+(declare-rule arith-int-mod-total ((t1 Int) (s1 Int))
+  :premises ((= (= s1 0) false))
+  :args (t1 s1)
+  :conclusion (= (mod t1 s1) (mod_total t1 s1))
+)
+(declare-rule arith-int-mod-total-one ((t1 Int))
+  :args (t1)
+  :conclusion (= (mod_total t1 1) 0)
+)
+(declare-rule arith-int-mod-total-zero ((t1 Int))
+  :args (t1)
+  :conclusion (= (mod_total t1 0) t1)
+)
+(declare-rule arith-int-mod-total-neg ((t1 Int) (s1 Int))
+  :premises ((= (< s1 0) true))
+  :args (t1 s1)
+  :conclusion (= (mod_total t1 s1) (mod_total t1 (- s1)))
+)
+(declare-rule arith-elim-int-gt ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (> t1 s1) (>= t1 (+ s1 1)))
+)
+(declare-rule arith-elim-int-lt ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (< t1 s1) (>= s1 (+ t1 1)))
+)
+(declare-rule arith-leq-norm ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (<= t1 s1) (not (>= t1 (+ s1 1))))
+)
+(declare-rule arith-geq-tighten ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (not (>= t1 s1)) (>= s1 (+ t1 1)))
+)
+(declare-rule arith-geq-norm1-int ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (>= t1 s1) (>= (- t1 s1) 0))
+)
+(declare-rule arith-geq-norm1-real ((t1 Real) (s1 Real))
+  :args (t1 s1)
+  :conclusion (= (>= t1 s1) (>= (- t1 s1) 0/1))
+)
+(declare-rule arith-eq-elim-real ((t1 Real) (s1 Real))
+  :args (t1 s1)
+  :conclusion (= (= t1 s1) (and (>= t1 s1) (<= t1 s1)))
+)
+(declare-rule arith-eq-elim-int ((t1 Int) (s1 Int))
+  :args (t1 s1)
+  :conclusion (= (= t1 s1) (and (>= t1 s1) (<= t1 s1)))
+)
+(declare-rule arith-int-eq-conflict ((t1 Int) (c1 Real))
+  :premises ((= (= (to_real (to_int c1)) c1) false))
+  :args (t1 c1)
+  :conclusion (= (= (to_real t1) c1) false)
+)
+(declare-rule arith-int-geq-tighten ((t1 Int) (c1 Real) (cc1 Int))
+  :premises ((= (= (to_real (to_int c1)) c1) false) (= cc1 (+ (to_int c1) 1)))
+  :args (t1 c1 cc1)
+  :conclusion (= (>= (to_real t1) c1) (>= t1 cc1))
+)
+(declare-rule arith-divisible-elim ((n1 Int) (t1 Int))
+  :premises ((= (= n1 0) false))
+  :args (n1 t1)
+  :conclusion (= (divisible n1 t1) (= (mod_total t1 n1) 0))
+)
+
+;;;;;;;;;;;;;;;;;
+;; Boolean
+;;;;;;;;;;;;;;;;;
+
+(declare-rule bool-double-not-elim ((t1 Bool))
+  :args (t1)
+  :conclusion (= (not (not t1)) t1)
+)
+(declare-rule bool-not-true ((t1 Bool))
+  :premises ((= t1 false))
+  :args (t1)
+  :conclusion (= (not t1) true)
+)
+(declare-rule bool-not-false ((t1 Bool))
+  :premises ((= t1 true))
+  :args (t1)
+  :conclusion (= (not t1) false)
+)
+(declare-rule bool-eq-true ((t1 Bool))
+  :args (t1)
+  :conclusion (= (= t1 true) t1)
+)
+(declare-rule bool-eq-false ((t1 Bool))
+  :args (t1)
+  :conclusion (= (= t1 false) (not t1))
+)
+(declare-rule bool-eq-nrefl ((x1 Bool))
+  :args (x1)
+  :conclusion (= (= x1 (not x1)) false)
+)
+(declare-rule bool-impl-false1 ((t1 Bool))
+  :args (t1)
+  :conclusion (= (=> t1 false) (not t1))
+)
+(declare-rule bool-impl-false2 ((t1 Bool))
+  :args (t1)
+  :conclusion (= (=> false t1) true)
+)
+(declare-rule bool-impl-true1 ((t1 Bool))
+  :args (t1)
+  :conclusion (= (=> t1 true) true)
+)
+(declare-rule bool-impl-true2 ((t1 Bool))
+  :args (t1)
+  :conclusion (= (=> true t1) t1)
+)
+(declare-rule bool-impl-elim ((t1 Bool) (s1 Bool))
+  :args (t1 s1)
+  :conclusion (= (=> t1 s1) (or (not t1) s1))
+)
+(declare-rule bool-dual-impl-eq ((t1 Bool) (s1 Bool))
+  :args (t1 s1)
+  :conclusion (= (and (=> t1 s1) (=> s1 t1)) (= t1 s1))
+)
+(declare-rule bool-implies-de-morgan ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (=> x1 y1)) (and x1 (not y1)))
+)
+(declare-rule bool-xor-refl ((x1 Bool))
+  :args (x1)
+  :conclusion (= (xor x1 x1) false)
+)
+(declare-rule bool-xor-nrefl ((x1 Bool))
+  :args (x1)
+  :conclusion (= (xor x1 (not x1)) true)
+)
+(declare-rule bool-xor-false ((x1 Bool))
+  :args (x1)
+  :conclusion (= (xor x1 false) x1)
+)
+(declare-rule bool-xor-true ((x1 Bool))
+  :args (x1)
+  :conclusion (= (xor x1 true) (not x1))
+)
+(declare-rule bool-xor-comm ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (xor x1 y1) (xor y1 x1))
+)
+(declare-rule bool-xor-elim ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (xor x1 y1) (= (not x1) y1))
+)
+(declare-rule bool-not-xor-elim ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (xor x1 y1)) (= x1 y1))
+)
+(declare-rule bool-not-eq-elim1 ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (= x1 y1)) (= (not x1) y1))
+)
+(declare-rule bool-not-eq-elim2 ((x1 Bool) (y1 Bool))
+  :args (x1 y1)
+  :conclusion (= (not (= x1 y1)) (= x1 (not y1)))
+)
+
+;;;;;;;;;;;;;;;;;
+;; Ite
+;;;;;;;;;;;;;;;;;
+
+(declare-rule ite-neg-branch ((c1 Bool) (x1 Bool) (y1 Bool))
+  :premises ((= (not y1) x1))
+  :args (c1 x1 y1)
+  :conclusion (= (ite c1 x1 y1) (= c1 x1))
+)
+(declare-rule ite-then-true ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 true x1) (or c1 x1))
+)
+(declare-rule ite-else-false ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 x1 false) (and c1 x1))
+)
+(declare-rule ite-then-false ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 false x1) (and (not c1) x1))
+)
+(declare-rule ite-else-true ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 x1 true) (or (not c1) x1))
+)
+(declare-rule ite-then-lookahead-self ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 c1 x1) (ite c1 true x1))
+)
+(declare-rule ite-else-lookahead-self ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 x1 c1) (ite c1 x1 false))
+)
+(declare-rule ite-then-lookahead-not-self ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 (not c1) x1) (ite c1 false x1))
+)
+(declare-rule ite-else-lookahead-not-self ((c1 Bool) (x1 Bool))
+  :args (c1 x1)
+  :conclusion (= (ite c1 x1 (not c1)) (ite c1 x1 true))
+)
+(declare-rule ite-expand ((c1 Bool) (x1 Bool) (y1 Bool))
+  :args (c1 x1 y1)
+  :conclusion (= (ite c1 x1 y1) (and (or (not c1) x1) (or c1 y1)))
+)
+(declare-rule bool-not-ite-elim ((c1 Bool) (x1 Bool) (y1 Bool))
+  :args (c1 x1 y1)
+  :conclusion (= (not (ite c1 x1 y1)) (ite c1 (not x1) (not y1)))
+)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Strings and regular expressions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare-rule str-eq-len-false ((x1 String) (y1 String))
+  :premises ((= (= (str.len x1) (str.len y1)) false))
+  :args (x1 y1)
+  :conclusion (= (= x1 y1) false)
+)
+(declare-rule str-indexof-re-none ((t1 String) (n1 Int))
+  :args (t1 n1)
+  :conclusion (= (str.indexof_re t1 re.none n1) -1)
+)
+(declare-rule str-indexof-re-emp-re ((t1 String) (r1 RegLan) (n1 Int))
+  :premises ((= (str.in_re "" r1) true) (= (>= (str.len t1) n1) true))
+  :args (t1 r1 n1)
+  :conclusion (= (str.indexof_re t1 r1 n1) n1)
+)
+(declare-rule str-to-lower-upper ((s1 String))
+  :args (s1)
+  :conclusion (= (str.to_lower (str.to_upper s1)) (str.to_lower s1))
+)
+(declare-rule str-to-upper-lower ((s1 String))
+  :args (s1)
+  :conclusion (= (str.to_upper (str.to_lower s1)) (str.to_upper s1))
+)
+(declare-rule str-to-lower-len ((s1 String))
+  :args (s1)
+  :conclusion (= (str.len (str.to_lower s1)) (str.len s1))
+)
+(declare-rule str-to-upper-len ((s1 String))
+  :args (s1)
+  :conclusion (= (str.len (str.to_upper s1)) (str.len s1))
+)
+(declare-rule str-to-lower-from-int ((n1 Int))
+  :args (n1)
+  :conclusion (= (str.to_lower (str.from_int n1)) (str.from_int n1))
+)
+(declare-rule str-to-upper-from-int ((n1 Int))
+  :args (n1)
+  :conclusion (= (str.to_upper (str.from_int n1)) (str.from_int n1))
+)
+(declare-rule str-leq-empty ((s1 String))
+  :args (s1)
+  :conclusion (= (str.<= "" s1) true)
+)
+(declare-rule str-leq-empty-eq ((s1 String))
+  :args (s1)
+  :conclusion (= (str.<= s1 "") (= s1 ""))
+)
+(declare-rule str-lt-elim ((s1 String) (t1 String))
+  :args (s1 t1)
+  :conclusion (= (str.< s1 t1) (and (not (= s1 t1)) (str.<= s1 t1)))
+)
+(declare-rule str-from-int-no-ctn-nondigit ((n1 Int) (s1 String))
+  :premises ((= (= s1 "") false) (= (str.to_int s1) -1))
+  :args (n1 s1)
+  :conclusion (= (str.contains (str.from_int n1) s1) false)
+)
+(declare-rule re-all-elim ()
+  :args ()
+  :conclusion (= re.all (re.* re.allchar))
+)
+(declare-rule re-opt-elim ((x1 RegLan))
+  :args (x1)
+  :conclusion (= (re.opt x1) (re.union (str.to_re "") x1))
+)
+(declare-rule re-diff-elim ((x1 RegLan) (y1 RegLan))
+  :args (x1 y1)
+  :conclusion (= (re.diff x1 y1) (re.inter x1 (re.comp y1)))
+)
+(declare-rule re-plus-elim ((x1 RegLan))
+  :args (x1)
+  :conclusion (= (re.+ x1) (re.++ x1 (re.* x1)))
+)
+(declare-rule re-repeat-elim ((n1 Int) (x1 RegLan))
+  :args (n1 x1)
+  :conclusion (= (re.^ n1 x1) (re.loop n1 n1 x1))
+)
+(declare-rule re-union-const-elim ((r1 RegLan) (s1 String))
+  :premises ((= (str.in_re s1 r1) true))
+  :args (r1 s1)
+  :conclusion (= (re.union (str.to_re s1) r1) r1)
+)
+(declare-rule re-star-none ()
+  :args ()
+  :conclusion (= (re.* re.none) (str.to_re ""))
+)
+(declare-rule re-star-emp ()
+  :args ()
+  :conclusion (= (re.* (str.to_re "")) (str.to_re ""))
+)
+(declare-rule re-star-star ((x1 RegLan))
+  :args (x1)
+  :conclusion (= (re.* (re.* x1)) (re.* x1))
+)
+(declare-rule re-loop-neg ((n1 Int) (m1 Int) (r1 RegLan))
+  :premises ((= (> n1 m1) true))
+  :args (n1 m1 r1)
+  :conclusion (= (re.loop n1 m1 r1) re.none)
+)
+(declare-rule re-in-empty ((t1 String))
+  :args (t1)
+  :conclusion (= (str.in_re t1 re.none) false)
+)
+(declare-rule re-in-sigma ((t1 String))
+  :args (t1)
+  :conclusion (= (str.in_re t1 re.allchar) (= (str.len t1) 1))
+)
+(declare-rule re-in-sigma-star ((t1 String))
+  :args (t1)
+  :conclusion (= (str.in_re t1 (re.* re.allchar)) true)
+)
+(declare-rule re-in-cstring ((t1 String) (s1 String))
+  :args (t1 s1)
+  :conclusion (= (str.in_re t1 (str.to_re s1)) (= t1 s1))
+)
+(declare-rule re-in-comp ((t1 String) (r1 RegLan))
+  :args (t1 r1)
+  :conclusion (= (str.in_re t1 (re.comp r1)) (not (str.in_re t1 r1)))
+)
+
+(declare-rule str-in-re-from-int-dig-range ((n1 Int))
+  :args (n1)
+  :conclusion (= (str.in_re (str.from_int n1) (re.* (re.range "0" "9"))) true)
+)