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;
     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 
    13 inductive_set
    14   lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
    15   for R :: "('a * 'a) set"
    16 where
    17   lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
    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"
    19 
    20 lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
    21   apply (induct as bs rule: lprod.induct)
    22   apply auto
    23   done
    24 
    25 lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
    26   apply (induct as bs rule: lprod.induct)
    27   apply auto
    28   done
    29 
    30 lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
    31   apply (induct as bs rule: lprod.induct)
    32   apply (auto)
    33   done
    34 
    35 lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
    36   by (auto intro: lprod_subset_elem)
    37 
    38 lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
    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
    45   case (lprod_list ah at bh bt a b)
    46   from prems have transR: "trans R" by auto
    47   have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
    48     by (simp add: algebra_simps)
    49   have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    50     by (simp add: algebra_simps)
    51   from prems have "(?ma, ?mb) \<in> mult R"
    52     by auto
    53   with mult_implies_one_step[OF transR] have 
    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)"
    55     by blast
    56   then obtain I J K where 
    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)"
    58     by blast   
    59   show ?case
    60   proof (cases "a = b")
    61     case True    
    62     have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
    63       apply (rule one_step_implies_mult[OF transR])
    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: algebra_simps)
    70       done
    71   next
    72     case False
    73     from False lprod_list have False: "(a, b) \<in> R" by blast
    74     have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
    75       apply (rule one_step_implies_mult[OF transR])
    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: algebra_simps)
    82       done
    83   qed
    84 qed
    85 
    86 lemma wf_lprod[recdef_wf,simp,intro]:
    87   assumes wf_R: "wf R"
    88   shows "wf (lprod R)"
    89 proof -
    90   have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
    91     by (auto simp add: lprod_implies_mult trans_trancl)
    92   note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
    93     OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
    94   note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
    95   show ?thesis by (auto intro: lprod)
    96 qed
    97 
    98 constdefs
    99   gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   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) }"
   101   gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   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) }"
   103 
   104 lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
   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 
   108 lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
   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 
   112 lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
   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 
   116 lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
   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]: 
   121   assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
   122 proof -
   123   have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   124     by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
   125   with wfR show ?thesis
   126     by (rule_tac wf_subset, auto)
   127 qed
   128 
   129 lemma [recdef_wf, simp, intro]: 
   130   assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
   131 proof -
   132   have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   133     by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
   134   with wfR show ?thesis
   135     by (rule_tac wf_subset, auto)
   136 qed
   137 
   138 lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
   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 
   143 lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
   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 
   148 lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
   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 
   153 lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
   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 
   158 lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
   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 
   163 lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
   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 
   168 lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
   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 
   177 lemma "((as,bs) \<in> lprod R) = 
   178   (\<exists> f. perm f {0 ..< (length as)} \<and> 
   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> 
   180   (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
   181 oops
   182 
   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" 
   184 oops
   185 
   186 
   187 
   188 end