src/HOL/ZF/LProd.thy
author nipkow
Fri, 18 Mar 2016 12:48:00 +0100
changeset 62651 66568c9b8216
parent 60515 484559628038
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
superfluous premise (noticed by Julian Nagele)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     1
(*  Title:      HOL/ZF/LProd.thy
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     2
    Author:     Steven Obua
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     3
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     4
    Introduces the lprod relation.
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     5
    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     6
*)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     7
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     8
theory LProd 
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 35422
diff changeset
     9
imports "~~/src/HOL/Library/Multiset"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    10
begin
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    11
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    12
inductive_set
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    13
  lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    14
  for R :: "('a * 'a) set"
22282
71b4aefad227 - Adapted to new inductive definition package
berghofe
parents: 19769
diff changeset
    15
where
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    16
  lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    18
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    19
lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    20
  apply (induct as bs rule: lprod.induct)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    21
  apply auto
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    22
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    23
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    24
lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    25
  apply (induct as bs rule: lprod.induct)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    26
  apply auto
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    27
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    28
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    29
lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    30
  apply (induct as bs rule: lprod.induct)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    31
  apply (auto)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    32
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    33
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    34
lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    35
  by (auto intro: lprod_subset_elem)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    36
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 60495
diff changeset
    37
lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (mset as, mset bs) \<in> mult R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    38
proof (induct as bs rule: lprod.induct)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    39
  case (lprod_single a b)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    40
  note step = one_step_implies_mult[
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    41
    where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    42
  show ?case by (auto intro: lprod_single step)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    43
next
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    44
  case (lprod_list ah at bh bt a b)
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41413
diff changeset
    45
  then have transR: "trans R" by auto
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 60495
diff changeset
    46
  have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23771
diff changeset
    47
    by (simp add: algebra_simps)
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 60495
diff changeset
    48
  have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23771
diff changeset
    49
    by (simp add: algebra_simps)
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41413
diff changeset
    50
  from lprod_list have "(?ma, ?mb) \<in> mult R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    51
    by auto
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    52
  with mult_implies_one_step[OF transR] have 
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 44011
diff changeset
    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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    54
    by blast
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    55
  then obtain I J K where 
60495
d7ff0a1df90a renamed Multiset.set_of to the canonical set_mset
nipkow
parents: 44011
diff changeset
    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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    57
    by blast   
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    58
  show ?case
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    59
  proof (cases "a = b")
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    60
    case True    
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    61
    have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
62651
66568c9b8216 superfluous premise (noticed by Julian Nagele)
nipkow
parents: 60515
diff changeset
    62
      apply (rule one_step_implies_mult)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    63
      apply (auto simp add: decomposed)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    64
      done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    65
    then show ?thesis
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    66
      apply (simp only: as bs)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    67
      apply (simp only: decomposed True)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23771
diff changeset
    68
      apply (simp add: algebra_simps)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    69
      done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    70
  next
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    71
    case False
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    72
    from False lprod_list have False: "(a, b) \<in> R" by blast
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    73
    have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
62651
66568c9b8216 superfluous premise (noticed by Julian Nagele)
nipkow
parents: 60515
diff changeset
    74
      apply (rule one_step_implies_mult)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    75
      apply (auto simp add: False decomposed)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    76
      done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    77
    then show ?thesis
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    78
      apply (simp only: as bs)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    79
      apply (simp only: decomposed)
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 23771
diff changeset
    80
      apply (simp add: algebra_simps)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    81
      done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    82
  qed
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    83
qed
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    84
44011
f67c93f52d13 eliminated obsolete recdef/wfrec related declarations
krauss
parents: 41528
diff changeset
    85
lemma wf_lprod[simp,intro]:
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    86
  assumes wf_R: "wf R"
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    87
  shows "wf (lprod R)"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    88
proof -
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 60495
diff changeset
    89
  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) mset"
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    90
    by (auto simp add: lprod_implies_mult trans_trancl)
60515
484559628038 renamed multiset_of -> mset
nipkow
parents: 60495
diff changeset
    91
  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="mset", 
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    92
    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    93
  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    94
  show ?thesis by (auto intro: lprod)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    95
qed
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    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
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
    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
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   102
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   103
lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   104
  by (auto intro: lprod_list[where a=c and b=c and 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   105
    ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   106
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   107
lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   108
  by (auto intro: lprod_list[where a=c and b=c and 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   109
    ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   110
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   111
lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   112
  by (auto intro: lprod_list[where a=c and b=c and 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   113
    ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   114
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   115
lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   116
  by (auto intro: lprod_list[where a=c and b=c and 
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   117
    ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   118
44011
f67c93f52d13 eliminated obsolete recdef/wfrec related declarations
krauss
parents: 41528
diff changeset
   119
lemma [simp, intro]:
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   120
  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   121
proof -
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   124
  with wfR show ?thesis
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   125
    by (rule_tac wf_subset, auto)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   126
qed
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   127
44011
f67c93f52d13 eliminated obsolete recdef/wfrec related declarations
krauss
parents: 41528
diff changeset
   128
lemma [simp, intro]:
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   129
  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   130
proof -
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   133
  with wfR show ?thesis
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   134
    by (rule_tac wf_subset, auto)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   135
qed
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   136
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   137
lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   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
276078f01ada eliminated global prems;
wenzelm
parents: 41413
diff changeset
   139
  apply (auto simp add: lprod_2_1 assms)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   140
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   141
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   142
lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   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
276078f01ada eliminated global prems;
wenzelm
parents: 41413
diff changeset
   144
  apply (auto simp add: lprod_2_2 assms)
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   145
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   146
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   147
lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   148
  apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   149
  apply (simp add: xr lprod_2_3)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   150
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   151
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   152
lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   153
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   154
  apply (simp add: yr lprod_2_3)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   155
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   156
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   157
lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   158
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   159
  apply (simp add: zr lprod_2_4)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   160
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   161
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   162
lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   163
  apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   164
  apply (simp add: y' lprod_2_4)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   165
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   166
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   167
lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   168
  apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   169
  apply (simp add: z' lprod_2_4)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   170
  done
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   173
   "perm f A \<equiv> inj_on f A \<and> f ` A = A"
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   174
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   175
lemma "((as,bs) \<in> lprod R) = 
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   176
  (\<exists> f. perm f {0 ..< (length as)} \<and> 
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   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> 
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   178
  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   179
oops
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   180
23771
bde6db239efa Restored set notation in Multiset theory.
berghofe
parents: 23477
diff changeset
   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
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   182
oops
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
   183
35422
e74b6f3b950c tuned final whitespace;
wenzelm
parents: 35416
diff changeset
   184
end