102 "f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x" |
102 "f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x" |
103 "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
103 "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
104 by smt+ |
104 by smt+ |
105 |
105 |
106 lemma |
106 lemma |
107 "SMT.distinct []" |
107 "distinct []" |
108 "SMT.distinct [a]" |
108 "distinct [a]" |
109 "SMT.distinct [a, b, c] \<longrightarrow> a \<noteq> c" |
109 "distinct [a, b, c] \<longrightarrow> a \<noteq> c" |
110 "SMT.distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d" |
110 "distinct [a, b, c] \<longrightarrow> d = b \<longrightarrow> a \<noteq> d" |
111 "\<not> SMT.distinct [a, b, a, b]" |
111 "\<not> distinct [a, b, a, b]" |
112 "a = b \<longrightarrow> \<not> SMT.distinct [a, b]" |
112 "a = b \<longrightarrow> \<not> distinct [a, b]" |
113 "a = b \<and> a = c \<longrightarrow> \<not> SMT.distinct [a, b, c]" |
113 "a = b \<and> a = c \<longrightarrow> \<not> distinct [a, b, c]" |
114 "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [d, b, c, a]" |
114 "distinct [a, b, c, d] \<longrightarrow> distinct [d, b, c, a]" |
115 "SMT.distinct [a, b, c, d] \<longrightarrow> SMT.distinct [a, b, c] \<and> SMT.distinct [b, c, d]" |
115 "distinct [a, b, c, d] \<longrightarrow> distinct [a, b, c] \<and> distinct [b, c, d]" |
116 by smt+ |
116 by smt+ |
117 |
117 |
118 lemma |
118 lemma |
119 "\<forall>x. x = x" |
119 "\<forall>x. x = x" |
120 "(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)" |
120 "(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)" |
191 "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)" |
191 "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)" |
192 "let P = (\<forall>x. Q x) in if P then P else \<not>P" |
192 "let P = (\<forall>x. Q x) in if P then P else \<not>P" |
193 by smt+ |
193 by smt+ |
194 |
194 |
195 lemma |
195 lemma |
196 "SMT.distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b" |
196 "distinct [a, b, c] \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b" |
197 sorry (* FIXME: injective function *) |
197 sorry (* FIXME: injective function *) |
198 |
198 |
199 lemma |
199 lemma |
200 assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)" |
200 assumes "\<forall>x. SMT.trigger [[SMT.pat (f x)]] (f x = x)" |
201 shows "f 1 = 1" |
201 shows "f 1 = 1" |
634 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" |
634 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2" |
635 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" |
635 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1" |
636 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" |
636 "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2" |
637 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
637 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
638 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
638 "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2" |
639 "SMT.distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" |
639 "distinct [i1, i2, i3] \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3" |
640 by smt+ |
640 by smt+ |
641 |
641 |
642 |
642 |
643 |
643 |
644 section {* Sets *} |
644 section {* Sets *} |