src/HOL/ZF/LProd.thy
 author haftmann Sun Sep 21 16:56:11 2014 +0200 (2014-09-21) changeset 58410 6d46ad54a2ab parent 44011 f67c93f52d13 child 60495 d7ff0a1df90a permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
```     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
```
```     9 imports "~~/src/HOL/Library/Multiset"
```
```    10 begin
```
```    11
```
```    12 inductive_set
```
```    13   lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
```
```    14   for R :: "('a * 'a) set"
```
```    15 where
```
```    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"
```
```    18
```
```    19 lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
```
```    20   apply (induct as bs rule: lprod.induct)
```
```    21   apply auto
```
```    22   done
```
```    23
```
```    24 lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
```
```    25   apply (induct as bs rule: lprod.induct)
```
```    26   apply auto
```
```    27   done
```
```    28
```
```    29 lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
```
```    30   apply (induct as bs rule: lprod.induct)
```
```    31   apply (auto)
```
```    32   done
```
```    33
```
```    34 lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
```
```    35   by (auto intro: lprod_subset_elem)
```
```    36
```
```    37 lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
```
```    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
```
```    44   case (lprod_list ah at bh bt a b)
```
```    45   then have transR: "trans R" by auto
```
```    46   have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
```
```    47     by (simp add: algebra_simps)
```
```    48   have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
```
```    49     by (simp add: algebra_simps)
```
```    50   from lprod_list have "(?ma, ?mb) \<in> mult R"
```
```    51     by auto
```
```    52   with mult_implies_one_step[OF transR] have
```
```    53     "\<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)"
```
```    54     by blast
```
```    55   then obtain I J K where
```
```    56     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)"
```
```    57     by blast
```
```    58   show ?case
```
```    59   proof (cases "a = b")
```
```    60     case True
```
```    61     have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
```
```    62       apply (rule one_step_implies_mult[OF transR])
```
```    63       apply (auto simp add: decomposed)
```
```    64       done
```
```    65     then show ?thesis
```
```    66       apply (simp only: as bs)
```
```    67       apply (simp only: decomposed True)
```
```    68       apply (simp add: algebra_simps)
```
```    69       done
```
```    70   next
```
```    71     case False
```
```    72     from False lprod_list have False: "(a, b) \<in> R" by blast
```
```    73     have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
```
```    74       apply (rule one_step_implies_mult[OF transR])
```
```    75       apply (auto simp add: False decomposed)
```
```    76       done
```
```    77     then show ?thesis
```
```    78       apply (simp only: as bs)
```
```    79       apply (simp only: decomposed)
```
```    80       apply (simp add: algebra_simps)
```
```    81       done
```
```    82   qed
```
```    83 qed
```
```    84
```
```    85 lemma wf_lprod[simp,intro]:
```
```    86   assumes wf_R: "wf R"
```
```    87   shows "wf (lprod R)"
```
```    88 proof -
```
```    89   have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
```
```    90     by (auto simp add: lprod_implies_mult trans_trancl)
```
```    91   note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of",
```
```    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]
```
```    94   show ?thesis by (auto intro: lprod)
```
```    95 qed
```
```    96
```
```    97 definition gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where
```
```    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) }"
```
```    99
```
```   100 definition gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where
```
```   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) }"
```
```   102
```
```   103 lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
```
```   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
```
```   107 lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
```
```   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
```
```   111 lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
```
```   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
```
```   115 lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
```
```   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
```
```   119 lemma [simp, intro]:
```
```   120   assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
```
```   121 proof -
```
```   122   have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
```
```   123     by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
```
```   124   with wfR show ?thesis
```
```   125     by (rule_tac wf_subset, auto)
```
```   126 qed
```
```   127
```
```   128 lemma [simp, intro]:
```
```   129   assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
```
```   130 proof -
```
```   131   have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
```
```   132     by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
```
```   133   with wfR show ?thesis
```
```   134     by (rule_tac wf_subset, auto)
```
```   135 qed
```
```   136
```
```   137 lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
```
```   138   apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
```
```   139   apply (auto simp add: lprod_2_1 assms)
```
```   140   done
```
```   141
```
```   142 lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
```
```   143   apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
```
```   144   apply (auto simp add: lprod_2_2 assms)
```
```   145   done
```
```   146
```
```   147 lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
```
```   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
```
```   152 lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
```
```   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
```
```   157 lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
```
```   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
```
```   162 lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
```
```   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
```
```   167 lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
```
```   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
```
```   172 definition perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" where
```
```   173    "perm f A \<equiv> inj_on f A \<and> f ` A = A"
```
```   174
```
```   175 lemma "((as,bs) \<in> lprod R) =
```
```   176   (\<exists> f. perm f {0 ..< (length as)} \<and>
```
```   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))"
```
```   179 oops
```
```   180
```
```   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"
```
```   182 oops
```
```   183
```
```   184 end
```