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/Bali/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 9 kB

SSL Basis.thy Sprache: Isabelle

(*  Title:      HOL/Bali/Basis.thy
    Author:     David von Oheimb
*)
subsection \<open>Definitions extending HOL as logical basis of Bali\<close>

theory Basis
imports Main
begin

subsubsection "misc"

ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>

declare if_split_asm  [split] option.split [split] option.split_asm [split]
setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]

lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}"
  by auto

lemma subset_insertD: "A \ insert x B \ A \ B \ x \ A \ (\B'. A = insert x B' \ B' \ B)"
  apply (case_tac "x \ A")
   apply (rule disjI2)
   apply (rule_tac x = "A - {x}" in exI)
   apply fast+
  done

abbreviation nat3 :: nat  (\<open>3\<close>) where "3 \<equiv> Suc 2"
abbreviation nat4 :: nat  (\<open>4\<close>) where "4 \<equiv> Suc 3"

(* irrefl_tranclI in Transitive_Closure.thy is more general *)
lemma irrefl_tranclI': "r\ \ r\<^sup>+ = {} \ \x. (x, x) \ r\<^sup>+"
  by (blast elim: tranclE dest: trancl_into_rtrancl)

lemma trancl_rtrancl_trancl: "\(x, y) \ r\<^sup>+; (y, z) \ r\<^sup>*\ \ (x, z) \ r\<^sup>+"
  by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2)

lemma rtrancl_into_trancl3: "\(a, b) \ r\<^sup>*; a \ b\ \ (a, b) \ r\<^sup>+"
  apply (drule rtranclD)
  apply auto
  done

lemma rtrancl_into_rtrancl2: "\(a, b) \ r; (b, c) \ r\<^sup>*\ \ (a, c) \ r\<^sup>*"
  by (auto intro: rtrancl_trans)

lemma triangle_lemma:
  assumes unique: "\a b c. \(a,b)\r; (a,c)\r\ \ b = c"
    and ax: "(a,x)\r\<^sup>*" and ay: "(a,y)\r\<^sup>*"
  shows "(x,y)\r\<^sup>* \ (y,x)\r\<^sup>*"
  using ax ay
proof (induct rule: converse_rtrancl_induct)
  assume "(x,y)\r\<^sup>*"
  then show ?thesis by blast
next
  fix a v
  assume a_v_r: "(a, v) \ r"
    and v_x_rt: "(v, x) \ r\<^sup>*"
    and a_y_rt: "(a, y) \ r\<^sup>*"
    and hyp: "(v, y) \ r\<^sup>* \ (x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*"
  from a_y_rt show "(x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*"
  proof (cases rule: converse_rtranclE)
    assume "a = y"
    with a_v_r v_x_rt have "(y,x) \ r\<^sup>*"
      by (auto intro: rtrancl_trans)
    then show ?thesis by blast
  next
    fix w
    assume a_w_r: "(a, w) \ r"
      and w_y_rt: "(w, y) \ r\<^sup>*"
    from a_v_r a_w_r unique have "v=w" by auto
    with w_y_rt hyp show ?thesis by blast
  qed
qed

lemma rtrancl_cases:
  assumes "(a,b)\r\<^sup>*"
  obtains (Refl) "a = b"
    | (Trancl) "(a,b)\r\<^sup>+"
  apply (rule rtranclE [OF assms])
   apply (auto dest: rtrancl_into_trancl1)
  done

lemma Ball_weaken: "\Ball s P; \ x. P x\Q x\\Ball s Q"
  by auto

lemma finite_SetCompr2:
  "finite {f y x |x y. P y}" if "finite (Collect P)"
    "\y. P y \ finite (range (f y))"
proof -
  have "{f y x |x y. P y} = (\y\Collect P. range (f y))"
    by auto
  with that show ?thesis by simp
qed

lemma list_all2_trans: "\a b c. P1 a b \ P2 b c \ P3 a c \
    \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
  apply (induct_tac xs1)
   apply simp
  apply (rule allI)
  apply (induct_tac xs2)
   apply simp
  apply (rule allI)
  apply (induct_tac xs3)
   apply auto
  done

subsubsection "pairs"

lemma surjective_pairing5:
  "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))),
    snd (snd (snd (snd p))))"
  by auto

lemma fst_splitE [elim!]:
  assumes "fst s' = x'"
  obtains x s where "s' = (x,s)" and "x = x'"
  using assms by (cases s') auto

lemma fst_in_set_lemma: "(x, y) \ set l \ x \ fst ` set l"
  by (induct l) auto

subsubsection "quantifiers"

lemma All_Ex_refl_eq2 [simp]: "(\x. (\b. x = f b \ Q b) \ P x) = (\b. Q b \ P (f b))"
  by auto

lemma ex_ex_miniscope1 [simp]: "(\w v. P w v \ Q v) = (\v. (\w. P w v) \ Q v)"
  by auto

lemma ex_miniscope2 [simp]: "(\v. P v \ Q \ R v) = (Q \ (\v. P v \ R v))"
  by auto

lemma ex_reorder31: "(\z x y. P x y z) = (\x y z. P x y z)"
  by auto

lemma All_Ex_refl_eq1 [simp]: "(\x. (\b. x = f b) \ P x) = (\b. P (f b))"
  by auto

subsubsection "sums"

notation case_sum  (infixr \<open>'(+')\<close> 80)

primrec the_Inl :: "'a + 'b \ 'a"
  where "the_Inl (Inl a) = a"

primrec the_Inr :: "'a + 'b \ 'b"
  where "the_Inr (Inr b) = b"

datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c

primrec the_In1 :: "('a, 'b, 'c) sum3 \ 'a"
  where "the_In1 (In1 a) = a"

primrec the_In2 :: "('a, 'b, 'c) sum3 \ 'b"
  where "the_In2 (In2 b) = b"

primrec the_In3 :: "('a, 'b, 'c) sum3 \ 'c"
  where "the_In3 (In3 c) = c"

abbreviation In1l :: "'al \ ('al + 'ar, 'b, 'c) sum3"
  where "In1l e \ In1 (Inl e)"

abbreviation In1r :: "'ar \ ('al + 'ar, 'b, 'c) sum3"
  where "In1r c \ In1 (Inr c)"

abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \ 'al"
  where "the_In1l \ the_Inl \ the_In1"

abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \ 'ar"
  where "the_In1r \ the_Inr \ the_In1"

ML \<open>
fun sum3_instantiate ctxt thm =
  map (fn s =>
    simplify (ctxt |> Simplifier.del_simps @{thms not_None_eq})
      (Rule_Insts.read_instantiate ctxt [((("t", 0), Position.none), "In" ^ s ^ " x")] ["x"] thm))
    ["1l","2","3","1r"]
\<close>
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)

subsubsection "quantifiers for option type"

syntax
  "_Oall" :: "[pttrn, 'a option, bool] \ bool" (\(3! _:_:/ _)\ [0,0,10] 10)
  "_Oex"  :: "[pttrn, 'a option, bool] \ bool" (\(3? _:_:/ _)\ [0,0,10] 10)

syntax (symbols)
  "_Oall" :: "[pttrn, 'a option, bool] \ bool" (\(3\_\_:/ _)\ [0,0,10] 10)
  "_Oex"  :: "[pttrn, 'a option, bool] \ bool" (\(3\_\_:/ _)\ [0,0,10] 10)

syntax_consts
  "_Oall" \<rightleftharpoons> Ball and
  "_Oex" \<rightleftharpoons> Bex

translations
  "\x\A: P" \ "\x\CONST set_option A. P"
  "\x\A: P" \ "\x\CONST set_option A. P"

subsubsection "Special map update"

text\<open>Deemed too special for theory Map.\<close>

definition chg_map :: "('b \ 'b) \ 'a \ ('a \ 'b) \ ('a \ 'b)"
  where "chg_map f a m = (case m a of None \ m | Some b \ m(a\f b))"

lemma chg_map_new[simp]: "m a = None \ chg_map f a m = m"
  unfolding chg_map_def by auto

lemma chg_map_upd[simp]: "m a = Some b \ chg_map f a m = m(a\f b)"
  unfolding chg_map_def by auto

lemma chg_map_other [simp]: "a \ b \ chg_map f a m b = m b"
  by (auto simp: chg_map_def)

subsubsection "unique association lists"

definition unique :: "('a \ 'b) list \ bool"
  where "unique = distinct \ map fst"

lemma uniqueD: "unique l \ (x, y) \ set l \ (x', y') \ set l \ x = x' \ y = y'"
  unfolding unique_def o_def
  by (induct l) (auto dest: fst_in_set_lemma)

lemma unique_Nil [simp]: "unique []"
  by (simp add: unique_def)

lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l \ (\y. (x,y) \ set l))"
  by (auto simp: unique_def dest: fst_in_set_lemma)

lemma unique_ConsD: "unique (x#xs) \ unique xs"
  by (simp add: unique_def)

lemma unique_single [simp]: "\p. unique [p]"
  by simp

lemma unique_append [rule_format (no_asm)]: "unique l' \ unique l \
    (\<forall>(x,y)\<in>set l. \<forall>(x',y')\<in>set l'. x' \<noteq> x) \<longrightarrow> unique (l @ l')"
  by (induct l) (auto dest: fst_in_set_lemma)

lemma unique_map_inj: "unique l \ inj f \ unique (map (\(k,x). (f k, g k x)) l)"
  by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)

lemma map_of_SomeI: "unique l \ (k, x) \ set l \ map_of l k = Some x"
  by (induct l) auto

subsubsection "list patterns"

definition lsplit :: "[['a, 'a list] \ 'b, 'a list] \ 'b"
  where "lsplit = (\f l. f (hd l) (tl l))"

text \<open>list patterns -- extends pre-defined type "pttrn" used in abstractions\<close>
syntax
  "_lpttrn" :: "[pttrn, pttrn] \ pttrn" (\_#/_\ [901,900] 900)
syntax_consts
  "_lpttrn" \<rightleftharpoons> lsplit
translations
  "\y # x # xs. b" \ "CONST lsplit (\y x # xs. b)"
  "\x # xs. b" \ "CONST lsplit (\x xs. b)"

lemma lsplit [simp]: "lsplit c (x#xs) = c x xs"
  by (simp add: lsplit_def)

lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z"
  by (simp add: lsplit_def)

end

quality96%