src/HOL/ZF/LProd.thy
changeset 23771 bde6db239efa
parent 23477 f4b83f03cac9
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/ZF/LProd.thy	Wed Jul 11 11:47:59 2007 +0200
     1.2 +++ b/src/HOL/ZF/LProd.thy	Wed Jul 11 11:49:56 2007 +0200
     1.3 @@ -10,57 +10,57 @@
     1.4  imports Multiset
     1.5  begin
     1.6  
     1.7 -inductive2
     1.8 -  lprod :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     1.9 -  for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 +inductive_set
    1.11 +  lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
    1.12 +  for R :: "('a * 'a) set"
    1.13  where
    1.14 -  lprod_single[intro!]: "R a b \<Longrightarrow> lprod R [a] [b]"
    1.15 -| 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)"
    1.16 +  lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
    1.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"
    1.18  
    1.19 -lemma "lprod R as bs \<Longrightarrow> length as = length bs"
    1.20 +lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
    1.21    apply (induct as bs rule: lprod.induct)
    1.22    apply auto
    1.23    done
    1.24  
    1.25 -lemma "lprod R as bs \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
    1.26 +lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
    1.27    apply (induct as bs rule: lprod.induct)
    1.28    apply auto
    1.29    done
    1.30  
    1.31 -lemma lprod_subset_elem: "lprod S as bs \<Longrightarrow> S \<le> R \<Longrightarrow> lprod R as bs"
    1.32 +lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
    1.33    apply (induct as bs rule: lprod.induct)
    1.34    apply (auto)
    1.35    done
    1.36  
    1.37 -lemma lprod_subset: "S \<le> R \<Longrightarrow> lprod S \<le> lprod R"
    1.38 +lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
    1.39    by (auto intro: lprod_subset_elem)
    1.40  
    1.41 -lemma lprod_implies_mult: "lprod R as bs \<Longrightarrow> transP R \<Longrightarrow> mult R (multiset_of as) (multiset_of bs)"
    1.42 +lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
    1.43  proof (induct as bs rule: lprod.induct)
    1.44    case (lprod_single a b)
    1.45    note step = one_step_implies_mult[
    1.46      where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
    1.47    show ?case by (auto intro: lprod_single step)
    1.48  next
    1.49 -  case (lprod_list ah at bh bt a b) 
    1.50 -  from prems have transR: "transP R" by auto
    1.51 +  case (lprod_list ah at bh bt a b)
    1.52 +  from prems have transR: "trans R" by auto
    1.53    have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
    1.54      by (simp add: ring_simps)
    1.55    have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    1.56      by (simp add: ring_simps)
    1.57 -  from prems have "mult R ?ma ?mb"
    1.58 +  from prems have "(?ma, ?mb) \<in> mult R"
    1.59      by auto
    1.60    with mult_implies_one_step[OF transR] have 
    1.61 -    "\<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)"
    1.62 +    "\<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)"
    1.63      by blast
    1.64    then obtain I J K where 
    1.65 -    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)"
    1.66 +    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)"
    1.67      by blast   
    1.68    show ?case
    1.69    proof (cases "a = b")
    1.70      case True    
    1.71 -    have "mult R ((I + {#b#}) + K) ((I + {#b#}) + J)"
    1.72 -      apply (rule one_step_implies_mult)
    1.73 +    have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
    1.74 +      apply (rule one_step_implies_mult[OF transR])
    1.75        apply (auto simp add: decomposed)
    1.76        done
    1.77      then show ?thesis
    1.78 @@ -70,9 +70,9 @@
    1.79        done
    1.80    next
    1.81      case False
    1.82 -    from False lprod_list have False: "R a b" by blast
    1.83 -    have "mult R (I + (K + {#a#})) (I + (J + {#b#}))"
    1.84 -      apply (rule one_step_implies_mult)
    1.85 +    from False lprod_list have False: "(a, b) \<in> R" by blast
    1.86 +    have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
    1.87 +      apply (rule one_step_implies_mult[OF transR])
    1.88        apply (auto simp add: False decomposed)
    1.89        done
    1.90      then show ?thesis
    1.91 @@ -84,88 +84,88 @@
    1.92  qed
    1.93  
    1.94  lemma wf_lprod[recdef_wf,simp,intro]:
    1.95 -  assumes wf_R: "wfP R"
    1.96 -  shows "wfP (lprod R)"
    1.97 +  assumes wf_R: "wf R"
    1.98 +  shows "wf (lprod R)"
    1.99  proof -
   1.100 -  have subset: "lprod (R^++) \<le> inv_imagep (mult (R^++)) multiset_of"
   1.101 -    by (auto simp add: lprod_implies_mult trans_trancl[to_pred])
   1.102 -  note lprodtrancl = wfP_subset[OF wf_inv_image[to_pred, where r="mult (R^++)" and f="multiset_of", 
   1.103 -    OF wf_mult[OF wfP_trancl[OF wf_R]]], OF subset]
   1.104 -  note lprod = wfP_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
   1.105 +  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
   1.106 +    by (auto simp add: lprod_implies_mult trans_trancl)
   1.107 +  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
   1.108 +    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
   1.109 +  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
   1.110    show ?thesis by (auto intro: lprod)
   1.111  qed
   1.112  
   1.113  constdefs
   1.114 -  gprod_2_2 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool"
   1.115 -  "gprod_2_2 R \<equiv> \<lambda>(a,b) (c,d). (a = c \<and> R b d) \<or> (b = d \<and> R a c)"
   1.116 -  gprod_2_1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool"
   1.117 -  "gprod_2_1 R \<equiv> \<lambda>(a,b) (c,d). (a = d \<and> R b c) \<or> (b = c \<and> R a d)"
   1.118 +  gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   1.119 +  "gprod_2_2 R \<equiv> { ((a,b), (c,d)) . (a = c \<and> (b,d) \<in> R) \<or> (b = d \<and> (a,c) \<in> R) }"
   1.120 +  gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
   1.121 +  "gprod_2_1 R \<equiv>  { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }"
   1.122  
   1.123 -lemma lprod_2_3: "R a b \<Longrightarrow> lprod R [a, c] [b, c]"
   1.124 +lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
   1.125    by (auto intro: lprod_list[where a=c and b=c and 
   1.126      ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 
   1.127  
   1.128 -lemma lprod_2_4: "R a b \<Longrightarrow> lprod R [c, a] [c, b]"
   1.129 +lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
   1.130    by (auto intro: lprod_list[where a=c and b=c and 
   1.131      ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])
   1.132  
   1.133 -lemma lprod_2_1: "R a b \<Longrightarrow> lprod R [c, a] [b, c]"
   1.134 +lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
   1.135    by (auto intro: lprod_list[where a=c and b=c and 
   1.136      ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 
   1.137  
   1.138 -lemma lprod_2_2: "R a b \<Longrightarrow> lprod R [a, c] [c, b]"
   1.139 +lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
   1.140    by (auto intro: lprod_list[where a=c and b=c and 
   1.141      ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
   1.142  
   1.143  lemma [recdef_wf, simp, intro]: 
   1.144 -  assumes wfR: "wfP R" shows "wfP (gprod_2_1 R)"
   1.145 +  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
   1.146  proof -
   1.147 -  have "gprod_2_1 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])"
   1.148 +  have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   1.149      by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
   1.150    with wfR show ?thesis
   1.151 -    by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred])
   1.152 +    by (rule_tac wf_subset, auto)
   1.153  qed
   1.154  
   1.155  lemma [recdef_wf, simp, intro]: 
   1.156 -  assumes wfR: "wfP R" shows "wfP (gprod_2_2 R)"
   1.157 +  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
   1.158  proof -
   1.159 -  have "gprod_2_2 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])"
   1.160 +  have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
   1.161      by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
   1.162    with wfR show ?thesis
   1.163 -    by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred])
   1.164 +    by (rule_tac wf_subset, auto)
   1.165  qed
   1.166  
   1.167 -lemma lprod_3_1: assumes "R x' x" shows "lprod R [y, z, x'] [x, y, z]"
   1.168 +lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
   1.169    apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
   1.170    apply (auto simp add: lprod_2_1 prems)
   1.171    done
   1.172  
   1.173 -lemma lprod_3_2: assumes "R z' z" shows "lprod R [z', x, y] [x,y,z]"
   1.174 +lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
   1.175    apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
   1.176    apply (auto simp add: lprod_2_2 prems)
   1.177    done
   1.178  
   1.179 -lemma lprod_3_3: assumes xr: "R xr x" shows "lprod R [xr, y, z] [x, y, z]"
   1.180 +lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
   1.181    apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
   1.182    apply (simp add: xr lprod_2_3)
   1.183    done
   1.184  
   1.185 -lemma lprod_3_4: assumes yr: "R yr y" shows "lprod R [x, yr, z] [x, y, z]"
   1.186 +lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
   1.187    apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
   1.188    apply (simp add: yr lprod_2_3)
   1.189    done
   1.190  
   1.191 -lemma lprod_3_5: assumes zr: "R zr z" shows "lprod R [x, y, zr] [x, y, z]"
   1.192 +lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
   1.193    apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
   1.194    apply (simp add: zr lprod_2_4)
   1.195    done
   1.196  
   1.197 -lemma lprod_3_6: assumes y': "R y' y" shows "lprod R [x, z, y'] [x, y, z]"
   1.198 +lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
   1.199    apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
   1.200    apply (simp add: y' lprod_2_4)
   1.201    done
   1.202  
   1.203 -lemma lprod_3_7: assumes z': "R z' z" shows "lprod R [x, z', y] [x, y, z]"
   1.204 +lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
   1.205    apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
   1.206    apply (simp add: z' lprod_2_4)
   1.207    done
   1.208 @@ -174,13 +174,13 @@
   1.209     perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool"
   1.210     "perm f A \<equiv> inj_on f A \<and> f ` A = A"
   1.211  
   1.212 -lemma "lprod R as bs = 
   1.213 +lemma "((as,bs) \<in> lprod R) = 
   1.214    (\<exists> f. perm f {0 ..< (length as)} \<and> 
   1.215 -  (\<forall> j. j < length as \<longrightarrow> (R (nth as j) (nth bs (f j)) \<or> (nth as j = nth bs (f j)))) \<and> 
   1.216 -  (\<exists> i. i < length as \<and> R (nth as i) (nth bs (f i))))"
   1.217 +  (\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and> 
   1.218 +  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
   1.219  oops
   1.220  
   1.221 -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)" 
   1.222 +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" 
   1.223  oops
   1.224  
   1.225