author  nipkow 
Fri, 18 Mar 2016 12:48:00 +0100  
changeset 62651  66568c9b8216 
parent 60515  484559628038 
child 66453  cc19f7ca2ed6 
permissions  rwrr 
19203  1 
(* Title: HOL/ZF/LProd.thy 
2 
Author: Steven Obua 

3 

4 
Introduces the lprod relation. 

5 
See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan 

6 
*) 

7 

8 
theory LProd 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
35422
diff
changeset

9 
imports "~~/src/HOL/Library/Multiset" 
19203  10 
begin 
11 

23771  12 
inductive_set 
13 
lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set" 

14 
for R :: "('a * 'a) set" 

22282  15 
where 
23771  16 
lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R" 
17 
 lprod_list[intro!]: "(ah@at, bh@bt) \<in> lprod R \<Longrightarrow> (a,b) \<in> R \<or> a = b \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R" 

19203  18 

23771  19 
lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs" 
19203  20 
apply (induct as bs rule: lprod.induct) 
21 
apply auto 

22 
done 

23 

23771  24 
lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs" 
19203  25 
apply (induct as bs rule: lprod.induct) 
26 
apply auto 

27 
done 

28 

23771  29 
lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R" 
19203  30 
apply (induct as bs rule: lprod.induct) 
31 
apply (auto) 

32 
done 

33 

23771  34 
lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R" 
19203  35 
by (auto intro: lprod_subset_elem) 
36 

60515  37 
lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (mset as, mset bs) \<in> mult R" 
19203  38 
proof (induct as bs rule: lprod.induct) 
39 
case (lprod_single a b) 

40 
note step = one_step_implies_mult[ 

41 
where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified] 

42 
show ?case by (auto intro: lprod_single step) 

43 
next 

23771  44 
case (lprod_list ah at bh bt a b) 
41528  45 
then have transR: "trans R" by auto 
60515  46 
have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _") 
29667  47 
by (simp add: algebra_simps) 
60515  48 
have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _") 
29667  49 
by (simp add: algebra_simps) 
41528  50 
from lprod_list have "(?ma, ?mb) \<in> mult R" 
19203  51 
by auto 
52 
with mult_implies_one_step[OF transR] have 

60495  53 
"\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)" 
19203  54 
by blast 
55 
then obtain I J K where 

60495  56 
decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> R)" 
19203  57 
by blast 
58 
show ?case 

59 
proof (cases "a = b") 

60 
case True 

23771  61 
have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R" 
62651  62 
apply (rule one_step_implies_mult) 
19203  63 
apply (auto simp add: decomposed) 
64 
done 

65 
then show ?thesis 

66 
apply (simp only: as bs) 

67 
apply (simp only: decomposed True) 

29667  68 
apply (simp add: algebra_simps) 
19203  69 
done 
70 
next 

71 
case False 

23771  72 
from False lprod_list have False: "(a, b) \<in> R" by blast 
73 
have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R" 

62651  74 
apply (rule one_step_implies_mult) 
19203  75 
apply (auto simp add: False decomposed) 
76 
done 

77 
then show ?thesis 

78 
apply (simp only: as bs) 

79 
apply (simp only: decomposed) 

29667  80 
apply (simp add: algebra_simps) 
19203  81 
done 
82 
qed 

83 
qed 

84 

44011
f67c93f52d13
eliminated obsolete recdef/wfrec related declarations
krauss
parents:
41528
diff
changeset

85 
lemma wf_lprod[simp,intro]: 
23771  86 
assumes wf_R: "wf R" 
87 
shows "wf (lprod R)" 

19203  88 
proof  
60515  89 
have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) mset" 
23771  90 
by (auto simp add: lprod_implies_mult trans_trancl) 
60515  91 
note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="mset", 
23771  92 
OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset] 
93 
note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified] 

19203  94 
show ?thesis by (auto intro: lprod) 
95 
qed 

96 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
29667
diff
changeset

97 
definition gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where 
23771  98 
"gprod_2_2 R \<equiv> { ((a,b), (c,d)) . (a = c \<and> (b,d) \<in> R) \<or> (b = d \<and> (a,c) \<in> R) }" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
29667
diff
changeset

99 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
29667
diff
changeset

100 
definition gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where 
23771  101 
"gprod_2_1 R \<equiv> { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }" 
19203  102 

23771  103 
lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R" 
19203  104 
by (auto intro: lprod_list[where a=c and b=c and 
105 
ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 

106 

23771  107 
lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R" 
19203  108 
by (auto intro: lprod_list[where a=c and b=c and 
109 
ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified]) 

110 

23771  111 
lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R" 
19203  112 
by (auto intro: lprod_list[where a=c and b=c and 
113 
ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 

114 

23771  115 
lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R" 
19203  116 
by (auto intro: lprod_list[where a=c and b=c and 
117 
ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified]) 

118 

44011
f67c93f52d13
eliminated obsolete recdef/wfrec related declarations
krauss
parents:
41528
diff
changeset

119 
lemma [simp, intro]: 
23771  120 
assumes wfR: "wf R" shows "wf (gprod_2_1 R)" 
19203  121 
proof  
23771  122 
have "gprod_2_1 R \<subseteq> inv_image (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

123 
by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2) 
19203  124 
with wfR show ?thesis 
23771  125 
by (rule_tac wf_subset, auto) 
19203  126 
qed 
127 

44011
f67c93f52d13
eliminated obsolete recdef/wfrec related declarations
krauss
parents:
41528
diff
changeset

128 
lemma [simp, intro]: 
23771  129 
assumes wfR: "wf R" shows "wf (gprod_2_2 R)" 
19203  130 
proof  
23771  131 
have "gprod_2_2 R \<subseteq> inv_image (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

132 
by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4) 
19203  133 
with wfR show ?thesis 
23771  134 
by (rule_tac wf_subset, auto) 
19203  135 
qed 
136 

23771  137 
lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R" 
19203  138 
apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified]) 
41528  139 
apply (auto simp add: lprod_2_1 assms) 
19203  140 
done 
141 

23771  142 
lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R" 
19203  143 
apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified]) 
41528  144 
apply (auto simp add: lprod_2_2 assms) 
19203  145 
done 
146 

23771  147 
lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R" 
19203  148 
apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified]) 
149 
apply (simp add: xr lprod_2_3) 

150 
done 

151 

23771  152 
lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R" 
19203  153 
apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified]) 
154 
apply (simp add: yr lprod_2_3) 

155 
done 

156 

23771  157 
lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R" 
19203  158 
apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified]) 
159 
apply (simp add: zr lprod_2_4) 

160 
done 

161 

23771  162 
lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R" 
19203  163 
apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified]) 
164 
apply (simp add: y' lprod_2_4) 

165 
done 

166 

23771  167 
lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R" 
19203  168 
apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified]) 
169 
apply (simp add: z' lprod_2_4) 

170 
done 

171 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
29667
diff
changeset

172 
definition perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" where 
19203  173 
"perm f A \<equiv> inj_on f A \<and> f ` A = A" 
174 

23771  175 
lemma "((as,bs) \<in> lprod R) = 
19203  176 
(\<exists> f. perm f {0 ..< (length as)} \<and> 
23771  177 
(\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and> 
178 
(\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))" 

19203  179 
oops 
180 

23771  181 
lemma "trans R \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R \<Longrightarrow> (b, a) \<in> R \<or> a = b \<Longrightarrow> (ah@at, bh@bt) \<in> lprod R" 
19203  182 
oops 
183 

35422  184 
end 