10217
|
1 |
theory AB = Main:;
|
|
2 |
|
|
3 |
datatype alfa = a | b;
|
|
4 |
|
|
5 |
lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)";
|
|
6 |
apply(case_tac x);
|
|
7 |
by(auto);
|
|
8 |
|
|
9 |
consts S :: "alfa list set"
|
|
10 |
A :: "alfa list set"
|
|
11 |
B :: "alfa list set";
|
|
12 |
|
|
13 |
inductive S A B
|
|
14 |
intros
|
|
15 |
"[] : S"
|
|
16 |
"w : A ==> b#w : S"
|
|
17 |
"w : B ==> a#w : S"
|
|
18 |
|
|
19 |
"w : S ==> a#w : A"
|
|
20 |
"[| v:A; w:A |] ==> b#v@w : A"
|
|
21 |
|
|
22 |
"w : S ==> b#w : B"
|
|
23 |
"[| v:B; w:B |] ==> a#v@w : B";
|
|
24 |
|
|
25 |
thm S_A_B.induct[no_vars];
|
|
26 |
|
|
27 |
lemma "(w : S --> size[x:w. x=a] = size[x:w. x=b]) &
|
|
28 |
(w : A --> size[x:w. x=a] = size[x:w. x=b] + 1) &
|
|
29 |
(w : B --> size[x:w. x=b] = size[x:w. x=a] + 1)";
|
|
30 |
apply(rule S_A_B.induct);
|
|
31 |
by(auto);
|
|
32 |
|
|
33 |
lemma intermed_val[rule_format(no_asm)]:
|
|
34 |
"(!i<n. abs(f(i+1) - f i) <= #1) -->
|
|
35 |
f 0 <= k & k <= f n --> (? i <= n. f i = (k::int))";
|
|
36 |
apply(induct n);
|
|
37 |
apply(simp);
|
|
38 |
apply(arith);
|
|
39 |
apply(rule);
|
|
40 |
apply(erule impE);
|
|
41 |
apply(simp);
|
|
42 |
apply(rule);
|
|
43 |
apply(erule_tac x = n in allE);
|
|
44 |
apply(simp);
|
|
45 |
apply(case_tac "k = f(n+1)");
|
|
46 |
apply(force);
|
|
47 |
apply(erule impE);
|
|
48 |
apply(simp add:zabs_def split:split_if_asm);
|
|
49 |
apply(arith);
|
|
50 |
by(blast intro:le_SucI);
|
|
51 |
|
|
52 |
lemma step1: "ALL i < size w.
|
|
53 |
abs((int(size[x:take (i+1) w . P x]) - int(size[x:take (i+1) w . ~P x])) -
|
|
54 |
(int(size[x:take i w . P x]) - int(size[x:take i w . ~P x]))) <= #1";
|
|
55 |
apply(induct w);
|
|
56 |
apply(simp);
|
|
57 |
apply(simp add:take_Cons split:nat.split);
|
|
58 |
apply(clarsimp);
|
|
59 |
apply(rule conjI);
|
|
60 |
apply(clarify);
|
|
61 |
apply(erule allE);
|
|
62 |
apply(erule impE);
|
|
63 |
apply(assumption);
|
|
64 |
apply(arith);
|
|
65 |
apply(clarify);
|
|
66 |
apply(erule allE);
|
|
67 |
apply(erule impE);
|
|
68 |
apply(assumption);
|
|
69 |
by(arith);
|
|
70 |
|
|
71 |
|
|
72 |
lemma part1:
|
|
73 |
"size[x:w. P x] = Suc(Suc(size[x:w. ~P x])) ==>
|
|
74 |
EX i<=size w. size[x:take i w. P x] = size[x:take i w. ~P x]+1";
|
|
75 |
apply(insert intermed_val[OF step1, of "P" "w" "#1"]);
|
|
76 |
apply(simp);
|
|
77 |
apply(erule exE);
|
|
78 |
apply(rule_tac x=i in exI);
|
|
79 |
apply(simp);
|
|
80 |
apply(rule int_int_eq[THEN iffD1]);
|
|
81 |
apply(simp);
|
|
82 |
by(arith);
|
|
83 |
|
|
84 |
lemma part2:
|
|
85 |
"[| size[x:take i xs @ drop i xs. P x] = size[x:take i xs @ drop i xs. ~P x]+2;
|
|
86 |
size[x:take i xs. P x] = size[x:take i xs. ~P x]+1 |]
|
|
87 |
==> size[x:drop i xs. P x] = size[x:drop i xs. ~P x]+1";
|
|
88 |
by(simp del:append_take_drop_id);
|
|
89 |
|
|
90 |
lemmas [simp] = S_A_B.intros;
|
|
91 |
|
|
92 |
lemma "(size[x:w. x=a] = size[x:w. x=b] --> w : S) &
|
|
93 |
(size[x:w. x=a] = size[x:w. x=b] + 1 --> w : A) &
|
|
94 |
(size[x:w. x=b] = size[x:w. x=a] + 1 --> w : B)";
|
|
95 |
apply(induct_tac w rule: length_induct);
|
|
96 |
apply(case_tac "xs");
|
|
97 |
apply(simp);
|
|
98 |
apply(simp);
|
|
99 |
apply(rule conjI);
|
|
100 |
apply(clarify);
|
|
101 |
apply(frule part1[of "%x. x=a", simplified]);
|
|
102 |
apply(erule exE);
|
|
103 |
apply(erule conjE);
|
|
104 |
apply(drule part2[of "%x. x=a", simplified]);
|
|
105 |
apply(assumption);
|
|
106 |
apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
|
|
107 |
apply(rule S_A_B.intros);
|
|
108 |
apply(force simp add:min_less_iff_disj);
|
|
109 |
apply(force split add: nat_diff_split);
|
|
110 |
apply(clarify);
|
|
111 |
apply(frule part1[of "%x. x=b", simplified]);
|
|
112 |
apply(erule exE);
|
|
113 |
apply(erule conjE);
|
|
114 |
apply(drule part2[of "%x. x=b", simplified]);
|
|
115 |
apply(assumption);
|
|
116 |
apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
|
|
117 |
apply(rule S_A_B.intros);
|
|
118 |
apply(force simp add:min_less_iff_disj);
|
|
119 |
by(force simp add:min_less_iff_disj split add: nat_diff_split);
|
|
120 |
|
|
121 |
end;
|