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