Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/ZF/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 7 kB

Quellcode-Bibliothek LProd.thy Sprache: Isabelle

(*  Title:      HOL/ZF/LProd.thy
    Author:     Steven Obua

    Introduces the lprod relation.
    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
*)

theory LProd
imports "HOL-Library.Multiset"
begin

inductive_set
  lprod :: "('a * 'a) set \ ('a list * 'a list) set"
  for R :: "('a * 'a) set"
where
  lprod_single[intro!]: "(a, b) \ R \ ([a], [b]) \ lprod R"
| lprod_list[intro!]: "(ah@at, bh@bt) \ lprod R \ (a,b) \ R \ a = b \ (ah@a#at, bh@b#bt) \ lprod R"

lemma "(as,bs) \ lprod R \ length as = length bs"
  apply (induct as bs rule: lprod.induct)
  apply auto
  done

lemma "(as, bs) \ lprod R \ 1 \ length as \ 1 \ length bs"
  apply (induct as bs rule: lprod.induct)
  apply auto
  done

lemma lprod_subset_elem: "(as, bs) \ lprod S \ S \ R \ (as, bs) \ lprod R"
  apply (induct as bs rule: lprod.induct)
  apply (auto)
  done

lemma lprod_subset: "S \ R \ lprod S \ lprod R"
  by (auto intro: lprod_subset_elem)

lemma lprod_implies_mult: "(as, bs) \ lprod R \ trans R \ (mset as, mset bs) \ mult R"
proof (induct as bs rule: lprod.induct)
  case (lprod_single a b)
  note step = one_step_implies_mult[
    where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]
  show ?case by (auto intro: lprod_single step)
next
  case (lprod_list ah at bh bt a b)
  then have transR: "trans R" by auto
  have as: "mset (ah @ a # at) = mset (ah @ at) + {#a#}" (is "_ = ?ma + _")
    by (simp add: algebra_simps)
  have bs: "mset (bh @ b # bt) = mset (bh @ bt) + {#b#}" (is "_ = ?mb + _")
    by (simp add: algebra_simps)
  from lprod_list have "(?ma, ?mb) \ mult R"
    by auto
  with mult_implies_one_step[OF transR] have
    "\I J K. ?mb = I + J \ ?ma = I + K \ J \ {#} \ (\k\set_mset K. \j\set_mset J. (k, j) \ R)"
    by blast
  then obtain I J K where
    decomposed: "?mb = I + J \ ?ma = I + K \ J \ {#} \ (\k\set_mset K. \j\set_mset J. (k, j) \ R)"
    by blast
  show ?case
  proof (cases "a = b")
    case True
    have "((I + {#b#}) + K, (I + {#b#}) + J) \ mult R"
      apply (rule one_step_implies_mult)
      apply (auto simp add: decomposed)
      done
    then show ?thesis
      apply (simp only: as bs)
      apply (simp only: decomposed True)
      apply (simp add: algebra_simps)
      done
  next
    case False
    from False lprod_list have False: "(a, b) \ R" by blast
    have "(I + (K + {#a#}), I + (J + {#b#})) \ mult R"
      apply (rule one_step_implies_mult)
      apply (auto simp add: False decomposed)
      done
    then show ?thesis
      apply (simp only: as bs)
      apply (simp only: decomposed)
      apply (simp add: algebra_simps)
      done
  qed
qed

lemma wf_lprod[simp,intro]:
  assumes wf_R: "wf R"
  shows "wf (lprod R)"
proof -
  have subset: "lprod (R\<^sup>+) \ inv_image (mult (R\<^sup>+)) mset"
    by (auto simp add: lprod_implies_mult trans_trancl)
  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R\<^sup>+)" and f="mset",
    OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
  note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
  show ?thesis by (auto intro: lprod)
qed

definition gprod_2_2 :: "('a * 'a) set \ (('a * 'a) * ('a * 'a)) set" where
  "gprod_2_2 R \ { ((a,b), (c,d)) . (a = c \ (b,d) \ R) \ (b = d \ (a,c) \ R) }"

definition gprod_2_1 :: "('a * 'a) set \ (('a * 'a) * ('a * 'a)) set" where
  "gprod_2_1 R \ { ((a,b), (c,d)) . (a = d \ (b,c) \ R) \ (b = c \ (a,d) \ R) }"

lemma lprod_2_3: "(a, b) \ R \ ([a, c], [b, c]) \ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and
    ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified])

lemma lprod_2_4: "(a, b) \ R \ ([c, a], [c, b]) \ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and
    ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])

lemma lprod_2_1: "(a, b) \ R \ ([c, a], [b, c]) \ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and
    ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified])

lemma lprod_2_2: "(a, b) \ R \ ([a, c], [c, b]) \ lprod R"
  by (auto intro: lprod_list[where a=c and b=c and
    ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])

lemma [simp, intro]:
  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
proof -
  have "gprod_2_1 R \ inv_image (lprod R) (\ (a,b). [a,b])"
    by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
  with wfR show ?thesis
    by (rule_tac wf_subset, auto)
qed

lemma [simp, intro]:
  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
proof -
  have "gprod_2_2 R \ inv_image (lprod R) (\ (a,b). [a,b])"
    by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
  with wfR show ?thesis
    by (rule_tac wf_subset, auto)
qed

lemma lprod_3_1: assumes "(x', x) \ R" shows "([y, z, x'], [x, y, z]) \ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
  apply (auto simp add: lprod_2_1 assms)
  done

lemma lprod_3_2: assumes "(z',z) \ R" shows "([z', x, y], [x,y,z]) \ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
  apply (auto simp add: lprod_2_2 assms)
  done

lemma lprod_3_3: assumes xr: "(xr, x) \ R" shows "([xr, y, z], [x, y, z]) \ lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
  apply (simp add: xr lprod_2_3)
  done

lemma lprod_3_4: assumes yr: "(yr, y) \ R" shows "([x, yr, z], [x, y, z]) \ lprod R"
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
  apply (simp add: yr lprod_2_3)
  done

lemma lprod_3_5: assumes zr: "(zr, z) \ R" shows "([x, y, zr], [x, y, z]) \ lprod R"
  apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
  apply (simp add: zr lprod_2_4)
  done

lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
  apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
  apply (simp add: y' lprod_2_4)
  done

lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
  apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
  apply (simp add: z' lprod_2_4)
  done

definition perm :: "('a \ 'a) \ 'a set \ bool" where
   "perm f A \ inj_on f A \ f ` A = A"

lemma "((as,bs) \ lprod R) =
  (\<exists> f. perm f {0 ..< (length as)} \<and>
  (\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and>
  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
oops

lemma "trans R \ (ah@a#at, bh@b#bt) \ lprod R \ (b, a) \ R \ a = b \ (ah@at, bh@bt) \ lprod R"
oops

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.