author | berghofe |
Wed, 07 Feb 2007 18:10:21 +0100 | |
changeset 22282 | 71b4aefad227 |
parent 19769 | c40ce2de2020 |
child 23477 | f4b83f03cac9 |
permissions | -rw-r--r-- |
19203 | 1 |
(* Title: HOL/ZF/LProd.thy |
2 |
ID: $Id$ |
|
3 |
Author: Steven Obua |
|
4 |
||
5 |
Introduces the lprod relation. |
|
6 |
See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
|
7 |
*) |
|
8 |
||
9 |
theory LProd |
|
10 |
imports Multiset |
|
11 |
begin |
|
12 |
||
22282 | 13 |
inductive2 |
14 |
lprod :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
15 |
for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
16 |
where |
|
17 |
lprod_single[intro!]: "R a b \<Longrightarrow> lprod R [a] [b]" |
|
18 |
| lprod_list[intro!]: "lprod R (ah@at) (bh@bt) \<Longrightarrow> R a b \<or> a = b \<Longrightarrow> lprod R (ah@a#at) (bh@b#bt)" |
|
19203 | 19 |
|
22282 | 20 |
lemma "lprod R as bs \<Longrightarrow> length as = length bs" |
19203 | 21 |
apply (induct as bs rule: lprod.induct) |
22 |
apply auto |
|
23 |
done |
|
24 |
||
22282 | 25 |
lemma "lprod R as bs \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs" |
19203 | 26 |
apply (induct as bs rule: lprod.induct) |
27 |
apply auto |
|
28 |
done |
|
29 |
||
22282 | 30 |
lemma lprod_subset_elem: "lprod S as bs \<Longrightarrow> S \<le> R \<Longrightarrow> lprod R as bs" |
19203 | 31 |
apply (induct as bs rule: lprod.induct) |
32 |
apply (auto) |
|
33 |
done |
|
34 |
||
22282 | 35 |
lemma lprod_subset: "S \<le> R \<Longrightarrow> lprod S \<le> lprod R" |
19203 | 36 |
by (auto intro: lprod_subset_elem) |
37 |
||
22282 | 38 |
lemma lprod_implies_mult: "lprod R as bs \<Longrightarrow> transP R \<Longrightarrow> mult R (multiset_of as) (multiset_of bs)" |
19203 | 39 |
proof (induct as bs rule: lprod.induct) |
40 |
case (lprod_single a b) |
|
41 |
note step = one_step_implies_mult[ |
|
42 |
where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified] |
|
43 |
show ?case by (auto intro: lprod_single step) |
|
44 |
next |
|
22282 | 45 |
case (lprod_list ah at bh bt a b) |
46 |
from prems have transR: "transP R" by auto |
|
19203 | 47 |
have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _") |
48 |
by (simp add: ring_eq_simps) |
|
49 |
have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _") |
|
50 |
by (simp add: ring_eq_simps) |
|
22282 | 51 |
from prems have "mult R ?ma ?mb" |
19203 | 52 |
by auto |
53 |
with mult_implies_one_step[OF transR] have |
|
22282 | 54 |
"\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. R k j)" |
19203 | 55 |
by blast |
56 |
then obtain I J K where |
|
22282 | 57 |
decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. R k j)" |
19203 | 58 |
by blast |
59 |
show ?case |
|
60 |
proof (cases "a = b") |
|
61 |
case True |
|
22282 | 62 |
have "mult R ((I + {#b#}) + K) ((I + {#b#}) + J)" |
63 |
apply (rule one_step_implies_mult) |
|
19203 | 64 |
apply (auto simp add: decomposed) |
65 |
done |
|
66 |
then show ?thesis |
|
67 |
apply (simp only: as bs) |
|
68 |
apply (simp only: decomposed True) |
|
69 |
apply (simp add: ring_eq_simps) |
|
70 |
done |
|
71 |
next |
|
72 |
case False |
|
22282 | 73 |
from False lprod_list have False: "R a b" by blast |
74 |
have "mult R (I + (K + {#a#})) (I + (J + {#b#}))" |
|
75 |
apply (rule one_step_implies_mult) |
|
19203 | 76 |
apply (auto simp add: False decomposed) |
77 |
done |
|
78 |
then show ?thesis |
|
79 |
apply (simp only: as bs) |
|
80 |
apply (simp only: decomposed) |
|
81 |
apply (simp add: ring_eq_simps) |
|
82 |
done |
|
83 |
qed |
|
84 |
qed |
|
85 |
||
86 |
lemma wf_lprod[recdef_wf,simp,intro]: |
|
22282 | 87 |
assumes wf_R: "wfP R" |
88 |
shows "wfP (lprod R)" |
|
19203 | 89 |
proof - |
22282 | 90 |
have subset: "lprod (R^++) \<le> inv_imagep (mult (R^++)) multiset_of" |
91 |
by (auto simp add: lprod_implies_mult trans_trancl[to_pred]) |
|
92 |
note lprodtrancl = wfP_subset[OF wf_inv_image[to_pred, where r="mult (R^++)" and f="multiset_of", |
|
93 |
OF wf_mult[OF wfP_trancl[OF wf_R]]], OF subset] |
|
94 |
note lprod = wfP_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified] |
|
19203 | 95 |
show ?thesis by (auto intro: lprod) |
96 |
qed |
|
97 |
||
98 |
constdefs |
|
22282 | 99 |
gprod_2_2 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool" |
100 |
"gprod_2_2 R \<equiv> \<lambda>(a,b) (c,d). (a = c \<and> R b d) \<or> (b = d \<and> R a c)" |
|
101 |
gprod_2_1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool" |
|
102 |
"gprod_2_1 R \<equiv> \<lambda>(a,b) (c,d). (a = d \<and> R b c) \<or> (b = c \<and> R a d)" |
|
19203 | 103 |
|
22282 | 104 |
lemma lprod_2_3: "R a b \<Longrightarrow> lprod R [a, c] [b, c]" |
19203 | 105 |
by (auto intro: lprod_list[where a=c and b=c and |
106 |
ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) |
|
107 |
||
22282 | 108 |
lemma lprod_2_4: "R a b \<Longrightarrow> lprod R [c, a] [c, b]" |
19203 | 109 |
by (auto intro: lprod_list[where a=c and b=c and |
110 |
ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified]) |
|
111 |
||
22282 | 112 |
lemma lprod_2_1: "R a b \<Longrightarrow> lprod R [c, a] [b, c]" |
19203 | 113 |
by (auto intro: lprod_list[where a=c and b=c and |
114 |
ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) |
|
115 |
||
22282 | 116 |
lemma lprod_2_2: "R a b \<Longrightarrow> lprod R [a, c] [c, b]" |
19203 | 117 |
by (auto intro: lprod_list[where a=c and b=c and |
118 |
ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified]) |
|
119 |
||
120 |
lemma [recdef_wf, simp, intro]: |
|
22282 | 121 |
assumes wfR: "wfP R" shows "wfP (gprod_2_1 R)" |
19203 | 122 |
proof - |
22282 | 123 |
have "gprod_2_1 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])" |
19769
c40ce2de2020
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
krauss
parents:
19203
diff
changeset
|
124 |
by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2) |
19203 | 125 |
with wfR show ?thesis |
22282 | 126 |
by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred]) |
19203 | 127 |
qed |
128 |
||
129 |
lemma [recdef_wf, simp, intro]: |
|
22282 | 130 |
assumes wfR: "wfP R" shows "wfP (gprod_2_2 R)" |
19203 | 131 |
proof - |
22282 | 132 |
have "gprod_2_2 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])" |
19769
c40ce2de2020
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
krauss
parents:
19203
diff
changeset
|
133 |
by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4) |
19203 | 134 |
with wfR show ?thesis |
22282 | 135 |
by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred]) |
19203 | 136 |
qed |
137 |
||
22282 | 138 |
lemma lprod_3_1: assumes "R x' x" shows "lprod R [y, z, x'] [x, y, z]" |
19203 | 139 |
apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified]) |
140 |
apply (auto simp add: lprod_2_1 prems) |
|
141 |
done |
|
142 |
||
22282 | 143 |
lemma lprod_3_2: assumes "R z' z" shows "lprod R [z', x, y] [x,y,z]" |
19203 | 144 |
apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified]) |
145 |
apply (auto simp add: lprod_2_2 prems) |
|
146 |
done |
|
147 |
||
22282 | 148 |
lemma lprod_3_3: assumes xr: "R xr x" shows "lprod R [xr, y, z] [x, y, z]" |
19203 | 149 |
apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified]) |
150 |
apply (simp add: xr lprod_2_3) |
|
151 |
done |
|
152 |
||
22282 | 153 |
lemma lprod_3_4: assumes yr: "R yr y" shows "lprod R [x, yr, z] [x, y, z]" |
19203 | 154 |
apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified]) |
155 |
apply (simp add: yr lprod_2_3) |
|
156 |
done |
|
157 |
||
22282 | 158 |
lemma lprod_3_5: assumes zr: "R zr z" shows "lprod R [x, y, zr] [x, y, z]" |
19203 | 159 |
apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified]) |
160 |
apply (simp add: zr lprod_2_4) |
|
161 |
done |
|
162 |
||
22282 | 163 |
lemma lprod_3_6: assumes y': "R y' y" shows "lprod R [x, z, y'] [x, y, z]" |
19203 | 164 |
apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified]) |
165 |
apply (simp add: y' lprod_2_4) |
|
166 |
done |
|
167 |
||
22282 | 168 |
lemma lprod_3_7: assumes z': "R z' z" shows "lprod R [x, z', y] [x, y, z]" |
19203 | 169 |
apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified]) |
170 |
apply (simp add: z' lprod_2_4) |
|
171 |
done |
|
172 |
||
173 |
constdefs |
|
174 |
perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" |
|
175 |
"perm f A \<equiv> inj_on f A \<and> f ` A = A" |
|
176 |
||
22282 | 177 |
lemma "lprod R as bs = |
19203 | 178 |
(\<exists> f. perm f {0 ..< (length as)} \<and> |
22282 | 179 |
(\<forall> j. j < length as \<longrightarrow> (R (nth as j) (nth bs (f j)) \<or> (nth as j = nth bs (f j)))) \<and> |
180 |
(\<exists> i. i < length as \<and> R (nth as i) (nth bs (f i))))" |
|
19203 | 181 |
oops |
182 |
||
22282 | 183 |
lemma "transP R \<Longrightarrow> lprod R (ah@a#at) (bh@b#bt) \<Longrightarrow> R b a \<or> a = b \<Longrightarrow> lprod R (ah@at) (bh@bt)" |
19203 | 184 |
oops |
185 |
||
186 |
||
187 |
||
188 |
end |