author  blanchet 
Mon, 05 May 2014 10:03:43 +0200  
changeset 56859  bc50d5e04e90 
parent 56819  ad1bbed53788 
child 57165  7b1bf424ec5f 
permissions  rwrr 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

1 
(* Title: HOL/SMT_Examples/SMT_Tests.thy 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

2 
Author: Sascha Boehme, TU Muenchen 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

3 
*) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

4 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

5 
header {* Tests for the SMT binding *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

6 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

7 
theory SMT_Tests 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

8 
imports Complex_Main 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

9 
begin 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

10 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

11 
smt_status 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

12 
smt2_status 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

13 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

14 
text {* Most examples are taken from various Isabelle theories and from HOL4. *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

15 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

16 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

17 
section {* Propositional logic *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

18 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

19 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

20 
"True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

21 
"\<not>False" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

22 
"\<not>\<not>True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

23 
"True \<and> True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

24 
"True \<or> False" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

25 
"False \<longrightarrow> True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

26 
"\<not>(False \<longleftrightarrow> True)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

27 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

28 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

29 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

30 
"P \<or> \<not>P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

31 
"\<not>(P \<and> \<not>P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

32 
"(True \<and> P) \<or> \<not>P \<or> (False \<and> P) \<or> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

33 
"P \<longrightarrow> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

34 
"P \<and> \<not> P \<longrightarrow> False" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

35 
"P \<and> Q \<longrightarrow> Q \<and> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

36 
"P \<or> Q \<longrightarrow> Q \<or> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

37 
"P \<and> Q \<longrightarrow> P \<or> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

38 
"\<not>(P \<or> Q) \<longrightarrow> \<not>P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

39 
"\<not>(P \<or> Q) \<longrightarrow> \<not>Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

40 
"\<not>P \<longrightarrow> \<not>(P \<and> Q)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

41 
"\<not>Q \<longrightarrow> \<not>(P \<and> Q)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

42 
"(P \<and> Q) \<longleftrightarrow> (\<not>(\<not>P \<or> \<not>Q))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

43 
"(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

44 
"(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

45 
"(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

46 
"(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

47 
"(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

48 
"(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

49 
"((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

50 
"(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

51 
"(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

52 
"((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

53 
"\<not>(P \<longrightarrow> R) \<longrightarrow> \<not>(Q \<longrightarrow> R) \<longrightarrow> \<not>(P \<and> Q \<longrightarrow> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

54 
"(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

55 
"P \<longrightarrow> (Q \<longrightarrow> P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

56 
"(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

57 
"(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

58 
"((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

59 
"(P \<longrightarrow> Q) \<longrightarrow> (\<not>Q \<longrightarrow> \<not>P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

60 
"(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

61 
"(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

62 
"(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

63 
"\<not>(P \<longleftrightarrow> \<not>P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

64 
"(P \<longrightarrow> Q) \<longleftrightarrow> (\<not>Q \<longrightarrow> \<not>P)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

65 
"P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

66 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

67 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

68 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

69 
"(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not>P \<longrightarrow> Q2))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

70 
"if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

71 
"(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

72 
"(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

73 
"(P1 \<longrightarrow> (if P2 then Q1 else Q2)) \<longleftrightarrow> 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

74 
(if P1 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> Q2)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

75 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

76 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

77 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

78 
"case P of True \<Rightarrow> P  False \<Rightarrow> \<not>P" 
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset

79 
"case P of False \<Rightarrow> \<not>P  True \<Rightarrow> P" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

80 
"case \<not>P of True \<Rightarrow> \<not>P  False \<Rightarrow> P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

81 
"case P of True \<Rightarrow> (Q \<longrightarrow> P)  False \<Rightarrow> (P \<longrightarrow> Q)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

82 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

83 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

84 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

85 
section {* Firstorder logic with equality *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

86 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

87 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

88 
"x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

89 
"x = y \<longrightarrow> y = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

90 
"x = y \<and> y = z \<longrightarrow> x = z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

91 
"x = y \<longrightarrow> f x = f y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

92 
"x = y \<longrightarrow> g x y = g y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

93 
"f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

94 
"((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

95 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

96 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

97 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

98 
"\<forall>x. x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

99 
"(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

100 
"\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

101 
"(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

102 
"(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

103 
"(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

104 
"(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

105 
"(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

106 
"(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

107 
"(\<forall>s. q s \<longrightarrow> r s) \<and> \<not>r s \<and> (\<forall>s. \<not>r s \<and> \<not>q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

108 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

109 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

110 
lemma 
50662
b1f4291eb916
regenerate certificates  and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset

111 
"(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

112 
by smt2 
50662
b1f4291eb916
regenerate certificates  and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset

113 

b1f4291eb916
regenerate certificates  and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents:
49995
diff
changeset

114 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

115 
"\<exists>x. x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

116 
"(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

117 
"(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

118 
"(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

119 
"(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

120 
"\<not>((\<exists>x. \<not>P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not>(\<exists>x. P x))" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

121 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

122 

49995
3b7ad6153322
regenerated "SMT_Examples" certificates after softtimeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset

123 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

124 
"\<exists>x y. x = y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

125 
"\<exists>x. P x \<longrightarrow> (\<exists>y. P x \<and> P y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

126 
"(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

127 
"\<exists>x. P x \<longrightarrow> P a \<and> P b" 
49995
3b7ad6153322
regenerated "SMT_Examples" certificates after softtimeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset

128 
"\<exists>x. (\<exists>y. P y) \<longrightarrow> P x" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

129 
"(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))" 
56727  130 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

131 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

132 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

133 
"(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

134 
"(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

135 
"(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

136 
"(if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)) \<longrightarrow> P x \<longrightarrow> P y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

137 
"(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c" 
56727  138 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

139 

49995
3b7ad6153322
regenerated "SMT_Examples" certificates after softtimeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset

140 
lemma 
41132  141 
"\<forall>x. \<exists>y. f x y = f x (g x)" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

142 
"(\<not>\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<not>(\<forall>x. \<not> P x))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

143 
"\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

144 
"\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

145 
"\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

146 
"(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

147 
"\<exists>z. P z \<longrightarrow> (\<forall>x. P x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

148 
"(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)" 
56727  149 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

150 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

151 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

152 
"(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

153 
"(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not>P y))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

154 
"P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

155 
"(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

156 
"(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

157 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

158 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

159 
lemma 
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset

160 
"(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c" 
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset

161 
"(\<exists>x\<in>M. P x) \<or> \<not>(P c \<and> c \<in> M)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

162 
by smt2+ 
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset

163 

4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into metaequalities for the rewriting conversions;
boehmes
parents:
37157
diff
changeset

164 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

165 
"let P = True in P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

166 
"let P = P1 \<or> P2 in P \<or> \<not>P" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

167 
"let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

168 
"(let x = y in x) = y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

169 
"(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

170 
"(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

171 
"(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

172 
"let P = (\<forall>x. Q x) in if P then P else \<not>P" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

173 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

174 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

175 
lemma 
47155
ade3fc826af3
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents:
47152
diff
changeset

176 
"a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b" 
56727  177 
using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *) 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

178 
by smt2 
41899
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset

179 

83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset

180 
lemma 
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset

181 
"(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c" 
83dd157ec9ab
finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents:
41601
diff
changeset

182 
"(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b" 
56727  183 
using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *) 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

184 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

185 

44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

186 

3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

187 
section {* Guidance for quantifier heuristics: patterns and weights *} 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

188 

37124  189 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

190 
assumes "\<forall>x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)" 
37124  191 
shows "f 1 = 1" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

192 
using assms using [[smt2_trace]] by smt2 
37124  193 

194 
lemma 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

195 
assumes "\<forall>x y. SMT2.trigger [[SMT2.pat (f x), SMT2.pat (g y)]] (f x = g y)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45694
diff
changeset

196 
shows "f a = g b" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

197 
using assms by smt2 
37124  198 

44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

199 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

200 
assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (P x > Q x)" 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

201 
and "P t" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

202 
shows "Q t" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

203 
using assms by smt2 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

204 

3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

205 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

206 
assumes "ALL x. SMT2.trigger [[SMT2.pat (P x), SMT2.pat (Q x)]] 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

207 
(P x & Q x > R x)" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

208 
and "P t" and "Q t" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

209 
shows "R t" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

210 
using assms by smt2 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

211 

3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

212 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

213 
assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)], [SMT2.pat (Q x)]] 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

214 
((P x > R x) & (Q x > R x))" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

215 
and "P t  Q t" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

216 
shows "R t" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

217 
using assms by smt2 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

218 

3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

219 
lemma 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

220 
assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (SMT2.weight 2 (P x > Q x))" 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

221 
and "P t" 
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

222 
shows "Q t" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

223 
using assms by smt2 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

224 

175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

225 
lemma 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

226 
assumes "ALL x. SMT2.weight 1 (P x > Q x)" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

227 
and "P t" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

228 
shows "Q t" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

229 
using assms by smt2 
44753
3c73f4068978
added some examples for pattern and weight annotations
boehmes
parents:
41899
diff
changeset

230 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

231 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

232 
section {* Metalogical connectives *} 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

233 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

234 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

235 
"True \<Longrightarrow> True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

236 
"False \<Longrightarrow> True" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

237 
"False \<Longrightarrow> False" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

238 
"P' x \<Longrightarrow> P' x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

239 
"P \<Longrightarrow> P \<or> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

240 
"Q \<Longrightarrow> P \<or> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

241 
"\<not>P \<Longrightarrow> P \<longrightarrow> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

242 
"Q \<Longrightarrow> P \<longrightarrow> Q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

243 
"\<lbrakk>P; \<not>Q\<rbrakk> \<Longrightarrow> \<not>(P \<longrightarrow> Q)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

244 
"P' x \<equiv> P' x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

245 
"P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

246 
"P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

247 
"x \<equiv> y \<Longrightarrow> y \<equiv> z \<Longrightarrow> x \<equiv> (z::'a::type)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

248 
"x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

249 
"(\<And>x. g x) \<Longrightarrow> g a \<or> a" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

250 
"(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

251 
"(p \<or> q) \<and> \<not>p \<Longrightarrow> q" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

252 
"(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" 
56727  253 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

254 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

255 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

256 
section {* Natural numbers *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

257 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

258 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

259 
"(0::nat) = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

260 
"(1::nat) = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

261 
"(0::nat) < 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

262 
"(0::nat) \<le> 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

263 
"(123456789::nat) < 2345678901" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

264 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

265 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

266 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

267 
"Suc 0 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

268 
"Suc x = x + 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

269 
"x < Suc x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

270 
"(Suc x = Suc y) = (x = y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

271 
"Suc (x + y) < Suc x + Suc y" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

272 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

273 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

274 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

275 
"(x::nat) + 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

276 
"0 + x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

277 
"x + y = y + x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

278 
"x + (y + z) = (x + y) + z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

279 
"(x + y = 0) = (x = 0 \<and> y = 0)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

280 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

281 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

282 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

283 
"(x::nat)  0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

284 
"x < y \<longrightarrow> x  y = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

285 
"x  y = 0 \<or> y  x = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

286 
"(x  y) + y = (if x < y then y else x)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

287 
"x  y  z = x  (y + z)" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

288 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

289 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

290 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

291 
"(x::nat) * 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

292 
"0 * x = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

293 
"x * 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

294 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

295 
"3 * x = x * 3" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

296 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

297 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

298 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

299 
"(0::nat) div 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

300 
"(x::nat) div 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

301 
"(0::nat) div 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

302 
"(1::nat) div 1 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

303 
"(3::nat) div 1 = 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

304 
"(x::nat) div 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

305 
"(0::nat) div 3 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

306 
"(1::nat) div 3 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

307 
"(3::nat) div 3 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

308 
"(x::nat) div 3 \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

309 
"(x div 3 = x) = (x = 0)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

310 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

311 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

312 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

313 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

314 
"(0::nat) mod 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

315 
"(x::nat) mod 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

316 
"(0::nat) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

317 
"(1::nat) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

318 
"(3::nat) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

319 
"(x::nat) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

320 
"(0::nat) mod 3 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

321 
"(1::nat) mod 3 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

322 
"(3::nat) mod 3 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

323 
"x mod 3 < 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

324 
"(x mod 3 = x) = (x < 3)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

325 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

326 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

327 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

328 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

329 
"(x::nat) = x div 1 * 1 + x mod 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

330 
"x = x div 3 * 3 + x mod 3" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

331 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

332 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

333 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

334 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

335 
"min (x::nat) y \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

336 
"min x y \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

337 
"min x y \<le> x + y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

338 
"z < x \<and> z < y \<longrightarrow> z < min x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

339 
"min x y = min y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

340 
"min x 0 = 0" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

341 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

342 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

343 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

344 
"max (x::nat) y \<ge> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

345 
"max x y \<ge> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

346 
"max x y \<ge> (x  y) + (y  x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

347 
"z > x \<and> z > y \<longrightarrow> z > max x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

348 
"max x y = max y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

349 
"max x 0 = x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

350 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

351 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

352 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

353 
"0 \<le> (x::nat)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

354 
"0 < x \<and> x \<le> 1 \<longrightarrow> x = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

355 
"x \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

356 
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

357 
"x < y \<longrightarrow> 3 * x < 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

358 
"x < y \<longrightarrow> x \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

359 
"(x < y) = (x + 1 \<le> y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

360 
"\<not>(x < x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

361 
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

362 
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

363 
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

364 
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

365 
"x < y \<and> y < z \<longrightarrow> \<not>(z < x)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

366 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

367 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

368 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

369 
section {* Integers *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

370 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

371 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

372 
"(0::int) = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

373 
"(0::int) = ( 0)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

374 
"(1::int) = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

375 
"\<not>(1 = (1::int))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

376 
"(0::int) < 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

377 
"(0::int) \<le> 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

378 
"123 + 345 < (567::int)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

379 
"(123456789::int) < 2345678901" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

380 
"(123456789::int) < 2345678901" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

381 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

382 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

383 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

384 
"(x::int) + 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

385 
"0 + x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

386 
"x + y = y + x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

387 
"x + (y + z) = (x + y) + z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

388 
"(x + y = 0) = (x = y)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

389 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

390 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

391 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

392 
"(1::int) =  1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

393 
"(3::int) =  3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

394 
"(x::int) < 0 \<longleftrightarrow> x > 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

395 
"x > 0 \<longrightarrow> x < 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

396 
"x < 0 \<longrightarrow> x > 0" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

397 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

398 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

399 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

400 
"(x::int)  0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

401 
"0  x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

402 
"x < y \<longrightarrow> x  y < 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

403 
"x  y = (y  x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

404 
"x  y = y + x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

405 
"x  y  z = x  (y + z)" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

406 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

407 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

408 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

409 
"(x::int) * 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

410 
"0 * x = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

411 
"x * 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

412 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

413 
"x * 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

414 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

415 
"3 * x = x * 3" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

416 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

417 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

418 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

419 
"(0::int) div 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

420 
"(x::int) div 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

421 
"(0::int) div 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

422 
"(1::int) div 1 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

423 
"(3::int) div 1 = 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

424 
"(x::int) div 1 = x" 
37151  425 
"(0::int) div 1 = 0" 
426 
"(1::int) div 1 = 1" 

427 
"(3::int) div 1 = 3" 

428 
"(x::int) div 1 = x" 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

429 
"(0::int) div 3 = 0" 
37151  430 
"(0::int) div 3 = 0" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

431 
"(1::int) div 3 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

432 
"(3::int) div 3 = 1" 
37151  433 
"(5::int) div 3 = 1" 
434 
"(1::int) div 3 = 1" 

435 
"(3::int) div 3 = 1" 

436 
"(5::int) div 3 = 2" 

437 
"(1::int) div 3 = 1" 

438 
"(3::int) div 3 = 1" 

439 
"(5::int) div 3 = 2" 

440 
"(1::int) div 3 = 0" 

441 
"(3::int) div 3 = 1" 

442 
"(5::int) div 3 = 1" 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

443 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

444 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

445 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

446 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

447 
"(0::int) mod 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

448 
"(x::int) mod 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

449 
"(0::int) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

450 
"(1::int) mod 1 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

451 
"(3::int) mod 1 = 0" 
37151  452 
"(x::int) mod 1 = 0" 
453 
"(0::int) mod 1 = 0" 

454 
"(1::int) mod 1 = 0" 

455 
"(3::int) mod 1 = 0" 

456 
"(x::int) mod 1 = 0" 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

457 
"(0::int) mod 3 = 0" 
37151  458 
"(0::int) mod 3 = 0" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

459 
"(1::int) mod 3 = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

460 
"(3::int) mod 3 = 0" 
37151  461 
"(5::int) mod 3 = 2" 
462 
"(1::int) mod 3 = 2" 

463 
"(3::int) mod 3 = 0" 

464 
"(5::int) mod 3 = 1" 

465 
"(1::int) mod 3 = 2" 

466 
"(3::int) mod 3 = 0" 

467 
"(5::int) mod 3 = 1" 

468 
"(1::int) mod 3 = 1" 

469 
"(3::int) mod 3 = 0" 

470 
"(5::int) mod 3 = 2" 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

471 
"x mod 3 < 3" 
37151  472 
"(x mod 3 = x) \<longrightarrow> (x < 3)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

473 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

474 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

475 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

476 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

477 
"(x::int) = x div 1 * 1 + x mod 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

478 
"x = x div 3 * 3 + x mod 3" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

479 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

480 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

481 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

482 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

483 
"abs (x::int) \<ge> 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

484 
"(abs x = 0) = (x = 0)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

485 
"(x \<ge> 0) = (abs x = x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

486 
"(x \<le> 0) = (abs x = x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

487 
"abs (abs x) = abs x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

488 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

489 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

490 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

491 
"min (x::int) y \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

492 
"min x y \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

493 
"z < x \<and> z < y \<longrightarrow> z < min x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

494 
"min x y = min y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

495 
"x \<ge> 0 \<longrightarrow> min x 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

496 
"min x y \<le> abs (x + y)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

497 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

498 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

499 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

500 
"max (x::int) y \<ge> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

501 
"max x y \<ge> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

502 
"z > x \<and> z > y \<longrightarrow> z > max x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

503 
"max x y = max y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

504 
"x \<ge> 0 \<longrightarrow> max x 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

505 
"max x y \<ge>  abs x  abs y" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

506 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

507 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

508 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

509 
"0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

510 
"x \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

511 
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

512 
"x < y \<longrightarrow> 3 * x < 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

513 
"x < y \<longrightarrow> x \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

514 
"(x < y) = (x + 1 \<le> y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

515 
"\<not>(x < x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

516 
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

517 
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

518 
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

519 
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

520 
"x < y \<and> y < z \<longrightarrow> \<not>(z < x)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

521 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

522 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

523 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

524 
section {* Reals *} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

525 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

526 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

527 
"(0::real) = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

528 
"(0::real) = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

529 
"(0::real) = ( 0)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

530 
"(1::real) = 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

531 
"\<not>(1 = (1::real))" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

532 
"(0::real) < 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

533 
"(0::real) \<le> 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

534 
"123 + 345 < (567::real)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

535 
"(123456789::real) < 2345678901" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

536 
"(123456789::real) < 2345678901" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

537 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

538 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

539 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

540 
"(x::real) + 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

541 
"0 + x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

542 
"x + y = y + x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

543 
"x + (y + z) = (x + y) + z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

544 
"(x + y = 0) = (x = y)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

545 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

546 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

547 
lemma 
41132  548 
"(1::real) =  1" 
549 
"(3::real) =  3" 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

550 
"(x::real) < 0 \<longleftrightarrow> x > 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

551 
"x > 0 \<longrightarrow> x < 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

552 
"x < 0 \<longrightarrow> x > 0" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

553 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

554 

49995
3b7ad6153322
regenerated "SMT_Examples" certificates after softtimeout change + removed a few needless oracles
blanchet
parents:
49834
diff
changeset

555 
lemma 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

556 
"(x::real)  0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

557 
"0  x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

558 
"x < y \<longrightarrow> x  y < 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

559 
"x  y = (y  x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

560 
"x  y = y + x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

561 
"x  y  z = x  (y + z)" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

562 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

563 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

564 
lemma 
41132  565 
"(x::real) * 0 = 0" 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

566 
"0 * x = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

567 
"x * 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

568 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

569 
"x * 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

570 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

571 
"3 * x = x * 3" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

572 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

573 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

574 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

575 
"(1/2 :: real) < 1" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

576 
"(1::real) / 3 = 1 / 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

577 
"(1::real) / 3 =  1 / 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

578 
"(1::real) / 3 =  1 / 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

579 
"(1::real) / 3 = 1 / 3" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

580 
"(x::real) / 1 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

581 
"x > 0 \<longrightarrow> x / 3 < x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

582 
"x < 0 \<longrightarrow> x / 3 > x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

583 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

584 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

585 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

586 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

587 
"(3::real) * (x / 3) = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

588 
"(x * 3) / 3 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

589 
"x > 0 \<longrightarrow> 2 * x / 3 < x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

590 
"x < 0 \<longrightarrow> 2 * x / 3 > x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

591 
using [[z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

592 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

593 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

594 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

595 
"abs (x::real) \<ge> 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

596 
"(abs x = 0) = (x = 0)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

597 
"(x \<ge> 0) = (abs x = x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

598 
"(x \<le> 0) = (abs x = x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

599 
"abs (abs x) = abs x" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

600 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

601 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

602 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

603 
"min (x::real) y \<le> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

604 
"min x y \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

605 
"z < x \<and> z < y \<longrightarrow> z < min x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

606 
"min x y = min y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

607 
"x \<ge> 0 \<longrightarrow> min x 0 = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

608 
"min x y \<le> abs (x + y)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

609 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

610 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

611 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

612 
"max (x::real) y \<ge> x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

613 
"max x y \<ge> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

614 
"z > x \<and> z > y \<longrightarrow> z > max x y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

615 
"max x y = max y x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

616 
"x \<ge> 0 \<longrightarrow> max x 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

617 
"max x y \<ge>  abs x  abs y" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

618 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

619 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

620 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

621 
"x \<le> (x::real)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

622 
"x \<le> y \<longrightarrow> 3 * x \<le> 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

623 
"x < y \<longrightarrow> 3 * x < 3 * y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

624 
"x < y \<longrightarrow> x \<le> y" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

625 
"\<not>(x < x)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

626 
"x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

627 
"x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

628 
"x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

629 
"x < y \<longrightarrow> y < z \<longrightarrow> x < z" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

630 
"x < y \<and> y < z \<longrightarrow> \<not>(z < x)" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

631 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

632 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

633 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

634 
section {* Datatypes, Records, and Typedefs *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

635 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

636 
subsection {* Without support by the SMT solver *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

637 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

638 
subsubsection {* Algebraic datatypes *} 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

639 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

640 
lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

641 
"x = fst (x, y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

642 
"y = snd (x, y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

643 
"((x, y) = (y, x)) = (x = y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

644 
"((x, y) = (u, v)) = (x = u \<and> y = v)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

645 
"(fst (x, y, z) = fst (u, v, w)) = (x = u)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

646 
"(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

647 
"(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

648 
"(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

649 
"(fst (x, y) = snd (x, y)) = (x = y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

650 
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

651 
"(fst (x, y) = snd (x, y)) = (x = y)" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

652 
"(fst p = snd p) = (p = (snd p, fst p))" 
41132  653 
using fst_conv snd_conv pair_collapse 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

654 
by smt2+ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

655 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

656 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

657 
"[x] \<noteq> Nil" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

658 
"[x, y] \<noteq> Nil" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

659 
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

660 
"hd (x # xs) = x" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

661 
"tl (x # xs) = xs" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

662 
"hd [x, y, z] = x" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

663 
"tl [x, y, z] = [y, z]" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

664 
"hd (tl [x, y, z]) = y" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

665 
"tl (tl [x, y, z]) = [z]" 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset

666 
using list.sel(1,3) list.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

667 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

668 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

669 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

670 
"fst (hd [(a, b)]) = a" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

671 
"snd (hd [(a, b)]) = b" 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset

672 
using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

673 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

674 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

675 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

676 
subsubsection {* Records *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

677 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

678 
record point = 
41427  679 
cx :: int 
680 
cy :: int 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

681 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

682 
record bw_point = point + 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

683 
black :: bool 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

684 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

685 
lemma 
41427  686 
"p1 = p2 \<longrightarrow> cx p1 = cx p2" 
687 
"p1 = p2 \<longrightarrow> cy p1 = cy p2" 

688 
"cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" 

689 
"cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

690 
using point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

691 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

692 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

693 
lemma 
41427  694 
"cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" 
695 
"cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" 

696 
"cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" 

697 
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" 

698 
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" 

699 
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" 

700 
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

701 
using point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

702 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

703 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

704 
lemma 
41427  705 
"cy (p \<lparr> cx := a \<rparr>) = cy p" 
706 
"cx (p \<lparr> cy := a \<rparr>) = cx p" 

707 
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

708 
sorry 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

709 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

710 
lemma 
41427  711 
"p1 = p2 \<longrightarrow> cx p1 = cx p2" 
712 
"p1 = p2 \<longrightarrow> cy p1 = cy p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

713 
"p1 = p2 \<longrightarrow> black p1 = black p2" 
41427  714 
"cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" 
715 
"cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

716 
"black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

717 
using point.simps bw_point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

718 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

719 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

720 
lemma 
41427  721 
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" 
722 
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" 

723 
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" 

724 
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" 

725 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" 

726 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" 

727 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

728 
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" 

729 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

730 
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" 

731 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

732 
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

733 
using point.simps bw_point.simps 
56859  734 
by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *) 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

735 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

736 
lemma 
41427  737 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" 
738 
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = 

739 
\<lparr> cx = 3, cy = 4, black = False \<rparr>" 

740 
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = 

741 
p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

742 
sorry 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

743 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

744 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

745 
subsubsection {* Type definitions *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

746 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44925
diff
changeset

747 
definition "three = {1, 2, 3::int}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44925
diff
changeset

748 

49834  749 
typedef three = three 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44925
diff
changeset

750 
unfolding three_def by auto 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

751 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

752 
definition n1 where "n1 = Abs_three 1" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

753 
definition n2 where "n2 = Abs_three 2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

754 
definition n3 where "n3 = Abs_three 3" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

755 
definition nplus where "nplus n m = Abs_three (Rep_three n + Rep_three m)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

756 

41427  757 
lemma three_def': "(n \<in> three) = (n = 1 \<or> n = 2 \<or> n = 3)" 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

758 
by (auto simp add: three_def) 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

759 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

760 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

761 
"n1 = n1" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

762 
"n2 = n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

763 
"n1 \<noteq> n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

764 
"nplus n1 n1 = n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

765 
"nplus n1 n2 = n3" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

766 
using n1_def n2_def n3_def nplus_def 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

767 
using three_def' Rep_three Abs_three_inverse 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

768 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

769 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

770 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

771 
subsection {* With support by the SMT solver (but without proofs) *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

772 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

773 
subsubsection {* Algebraic datatypes *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

774 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

775 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

776 
"x = fst (x, y)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

777 
"y = snd (x, y)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

778 
"((x, y) = (y, x)) = (x = y)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

779 
"((x, y) = (u, v)) = (x = u \<and> y = v)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

780 
"(fst (x, y, z) = fst (u, v, w)) = (x = u)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

781 
"(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

782 
"(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

783 
"(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

784 
"(fst (x, y) = snd (x, y)) = (x = y)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

785 
"p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

786 
"(fst (x, y) = snd (x, y)) = (x = y)" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

787 
"(fst p = snd p) = (p = (snd p, fst p))" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

788 
using fst_conv snd_conv pair_collapse 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

789 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

790 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

791 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

792 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

793 
"[x] \<noteq> Nil" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

794 
"[x, y] \<noteq> Nil" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

795 
"x \<noteq> y \<longrightarrow> [x] \<noteq> [y]" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

796 
"hd (x # xs) = x" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

797 
"tl (x # xs) = xs" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

798 
"hd [x, y, z] = x" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

799 
"tl [x, y, z] = [y, z]" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

800 
"hd (tl [x, y, z]) = y" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

801 
"tl (tl [x, y, z]) = [z]" 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset

802 
using list.sel(1,3) 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

803 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

804 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

805 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

806 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

807 
"fst (hd [(a, b)]) = a" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

808 
"snd (hd [(a, b)]) = b" 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
54489
diff
changeset

809 
using fst_conv snd_conv pair_collapse list.sel(1,3) 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

810 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

811 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

812 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

813 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

814 
subsubsection {* Records *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

815 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

816 
lemma 
41427  817 
"p1 = p2 \<longrightarrow> cx p1 = cx p2" 
818 
"p1 = p2 \<longrightarrow> cy p1 = cy p2" 

819 
"cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" 

820 
"cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

821 
using point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

822 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

823 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

824 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

825 
lemma 
41427  826 
"cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" 
827 
"cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" 

828 
"cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" 

829 
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" 

830 
"\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" 

831 
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" 

832 
"p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

833 
using point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

834 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

835 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

836 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

837 
lemma 
41427  838 
"cy (p \<lparr> cx := a \<rparr>) = cy p" 
839 
"cx (p \<lparr> cy := a \<rparr>) = cx p" 

840 
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

841 
using point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

842 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

843 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

844 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

845 
lemma 
41427  846 
"p1 = p2 \<longrightarrow> cx p1 = cx p2" 
847 
"p1 = p2 \<longrightarrow> cy p1 = cy p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

848 
"p1 = p2 \<longrightarrow> black p1 = black p2" 
41427  849 
"cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" 
850 
"cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

851 
"black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

852 
using point.simps bw_point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

853 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

854 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

855 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

856 
lemma 
41427  857 
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" 
858 
"cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" 

859 
"black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" 

860 
"cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" 

861 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" 

862 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" 

863 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

864 
p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" 

865 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

866 
p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" 

867 
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> 

868 
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

869 
using point.simps bw_point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

870 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

871 
by smt2+ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

872 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

873 
lemma 
41427  874 
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" 
875 
"\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = 

876 
\<lparr> cx = 3, cy = 4, black = False \<rparr>" 

877 
sorry 

878 

879 
lemma 

880 
"p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = 

881 
p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

882 
using point.simps bw_point.simps 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

883 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

884 
by smt2 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

885 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

886 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

887 
subsubsection {* Type definitions *} 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

888 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

889 
lemma 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

890 
"n1 = n1" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

891 
"n2 = n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

892 
"n1 \<noteq> n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

893 
"nplus n1 n1 = n2" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

894 
"nplus n1 n2 = n3" 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41132
diff
changeset

895 
using n1_def n2_def n3_def nplus_def 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

896 
using [[smt2_oracle, z3_new_extensions]] 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

897 
by smt2+ 
37157  898 

899 

900 
section {* Function updates *} 

901 

902 
lemma 

903 
"(f (i := v)) i = v" 

904 
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" 

905 
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" 

906 
"i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" 

907 
"i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" 

908 
"i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" 

47155
ade3fc826af3
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents:
47152
diff
changeset

909 
"i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and> i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" 
41132  910 
using fun_upd_same fun_upd_apply 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

911 
by smt2+ 
37157  912 

913 

914 
section {* Sets *} 

915 

44925  916 
lemma Empty: "x \<notin> {}" by simp 
917 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

918 
lemmas smt2_sets = Empty UNIV_I Un_iff Int_iff 
37157  919 

920 
lemma 

921 
"x \<notin> {}" 

922 
"x \<in> UNIV" 

44925  923 
"x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B" 
924 
"x \<in> P \<union> {} \<longleftrightarrow> x \<in> P" 

37157  925 
"x \<in> P \<union> UNIV" 
44925  926 
"x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P" 
927 
"x \<in> P \<union> P \<longleftrightarrow> x \<in> P" 

928 
"x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R" 

929 
"x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B" 

37157  930 
"x \<notin> P \<inter> {}" 
44925  931 
"x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P" 
932 
"x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P" 

933 
"x \<in> P \<inter> P \<longleftrightarrow> x \<in> P" 

934 
"x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R" 

935 
"{x. x \<in> P} = {y. y \<in> P}" 

56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55417
diff
changeset

936 
by (smt2 smt2_sets)+ 
37157  937 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

938 
end 