merged

--- a/NEWS	Thu Apr 13 23:53:12 2023 +0200
+++ b/NEWS	Fri Apr 14 10:12:30 2023 +0200
@@ -230,6 +230,7 @@
       mult_mono_strong
       multeqp_code_iff_reflclp_multp
       multp_code_iff_multp
+      multp_image_mset_image_msetI
       multp_mono_strong
       multp_repeat_mset_repeat_msetI
       total_mult
@@ -245,8 +246,10 @@
       irreflp_on_multpHO[simp]
       multpDM_mono_strong
       multpDM_plus_plusI[simp]
+      multpHO_double_double[simp]
       multpHO_mono_strong
       multpHO_plus_plus[simp]
+      multpHO_repeat_mset_repeat_mset[simp]
       strict_subset_implies_multpDM
       strict_subset_implies_multpHO
       totalp_multpDM

--- a/src/HOL/Data_Structures/Tries_Binary.thy	Thu Apr 13 23:53:12 2023 +0200
+++ b/src/HOL/Data_Structures/Tries_Binary.thy	Fri Apr 14 10:12:30 2023 +0200
@@ -91,9 +91,39 @@
 lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
 by(auto simp add: isin_delete set_trie_def)
 
+text \<open>Invariant: tries are fully shrunk:\<close>
+fun invar where
+"invar Lf = True" |
+"invar (Nd b (l,r)) = (invar l \<and> invar r \<and> (l = Lf \<and> r = Lf \<longrightarrow> b))"
+
+lemma insert_Lf: "insert xs t \<noteq> Lf"
+using insert.elims by blast
+
+lemma invar_insert: "invar t \<Longrightarrow> invar(insert xs t)"
+proof(induction xs t rule: insert.induct)
+  case 1 thus ?case by simp
+next
+  case (2 b lr)
+  thus ?case by(cases lr; simp)
+next
+  case (3 k ks)
+  thus ?case by(simp; cases ks; auto)
+next
+  case (4 k ks b lr)
+  then show ?case by(cases lr; auto simp: insert_Lf)
+qed
+
+lemma invar_delete: "invar t \<Longrightarrow> invar(delete xs t)"
+proof(induction t arbitrary: xs)
+  case Lf thus ?case by simp
+next
+  case (Nd b lr)
+  thus ?case by(cases lr)(auto split: list.split)
+qed
+
 interpretation S: Set
 where empty = empty and isin = isin and insert = insert and delete = delete
-and set = set_trie and invar = "\<lambda>t. True"
+and set = set_trie and invar = invar
 proof (standard, goal_cases)
   case 1 show ?case by (rule set_trie_empty)
 next
@@ -102,13 +132,24 @@
   case 3 thus ?case by(auto simp: set_trie_insert)
 next
   case 4 show ?case by(rule set_trie_delete)
-qed (rule TrueI)+
+next
+  case 5 show ?case by(simp)
+next
+  case 6 thus ?case by(rule invar_insert)
+next
+  case 7 thus ?case by(rule invar_delete)
+qed
 
 
 subsection "Patricia Trie"
 
 datatype trieP = LfP | NdP "bool list" bool "trieP * trieP"
 
+text \<open>Fully shrunk:\<close>
+fun invarP where
+"invarP LfP = True" |
+"invarP (NdP ps b (l,r)) = (invarP l \<and> invarP r \<and> (l = LfP \<or> r = LfP \<longrightarrow> b))"
+
 fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
 "isinP LfP ks = False" |
 "isinP (NdP ps b lr) ks =
@@ -120,12 +161,12 @@
 definition emptyP :: trieP where
 [simp]: "emptyP = LfP"
 
-fun split where
-"split [] ys = ([],[],ys)" |
-"split xs [] = ([],xs,[])" |
-"split (x#xs) (y#ys) =
+fun lcp :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list" where
+"lcp [] ys = ([],[],ys)" |
+"lcp xs [] = ([],xs,[])" |
+"lcp (x#xs) (y#ys) =
   (if x\<noteq>y then ([],x#xs,y#ys)
-   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
+   else let (ps,xs',ys') = lcp xs ys in (x#ps,xs',ys'))"
 
 
 lemma mod2_cong[fundef_cong]:
@@ -137,7 +178,7 @@
 fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
 "insertP ks LfP  = NdP ks True (LfP,LfP)" |
 "insertP ks (NdP ps b lr) =
-  (case split ks ps of
+  (case lcp ks ps of
      (qs, k#ks', p#ps') \<Rightarrow>
        let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
        NdP qs False (if k then (tp,tk) else (tk,tp)) |
@@ -149,18 +190,26 @@
      (qs,[],[]) \<Rightarrow> NdP ps True lr)"
 
 
-fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
-"nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
+text \<open>Smart constructor that shrinks:\<close>
+definition nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
+"nodeP ps b lr =
+ (if b then  NdP ps b lr
+  else case lr of
+   (LfP,LfP) \<Rightarrow> LfP |
+   (LfP, NdP ks b lr) \<Rightarrow> NdP (ps @ True # ks) b lr |
+   (NdP ks b lr, LfP) \<Rightarrow> NdP (ps @ False # ks) b lr |
+   _ \<Rightarrow> NdP ps b lr)"
 
 fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
 "deleteP ks LfP  = LfP" |
 "deleteP ks (NdP ps b lr) =
-  (case split ks ps of
+  (case lcp ks ps of
      (_, _, _#_) \<Rightarrow> NdP ps b lr |
      (_, k#ks', []) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
      (_, [], []) \<Rightarrow> nodeP ps False lr)"
 
 
+
 subsubsection \<open>Functional Correctness\<close>
 
 text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
@@ -214,9 +263,9 @@
 apply auto
 done
 
-lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
+lemma lcp_if: "lcp ks ps = (qs, ks', ps') \<Longrightarrow>
   ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
-apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
+apply(induction ks ps arbitrary: qs ks' ps' rule: lcp.induct)
 apply(auto split: prod.splits if_splits)
 done
 
@@ -224,7 +273,7 @@
   "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
 apply(induction t arbitrary: ks)
 apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
-           dest!: split_if split: list.split prod.split if_splits)
+           dest!: lcp_if split: list.split prod.split if_splits)
 done
 
 
@@ -246,14 +295,52 @@
    = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
 by(induction xs)(auto simp: prefix_trie_Lf)
 
+lemma nodeP_LfP2: "nodeP xs False (LfP, LfP) = LfP"
+by(simp add: nodeP_def)
+
+text \<open>Some non-inductive aux. lemmas:\<close>
+
+lemma abs_trieP_nodeP: "a\<noteq>LfP \<or> b \<noteq> LfP \<Longrightarrow>
+  abs_trieP (nodeP xs f (a, b)) = prefix_trie xs (Nd f (abs_trieP a, abs_trieP b))"
+by(auto simp add: nodeP_def prefix_trie_append split: trieP.split)
+
+lemma nodeP_True: "nodeP ps True lr = NdP ps True lr"
+by(simp add: nodeP_def)
+
 lemma delete_abs_trieP:
   "delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
 apply(induction t arbitrary: ks)
 apply(auto simp: delete_prefix_trie delete_append_prefix_trie
-        prefix_trie_append prefix_trie_Lf abs_trieP_Lf
-        dest!: split_if split: if_splits list.split prod.split)
+        prefix_trie_append prefix_trie_Lf abs_trieP_Lf nodeP_LfP2 abs_trieP_nodeP nodeP_True
+        dest!: lcp_if split: if_splits list.split prod.split)
 done
 
+text \<open>Invariant preservation:\<close>
+
+lemma insertP_LfP: "insertP xs t \<noteq> LfP"
+by(cases t)(auto split: prod.split list.split)
+
+lemma invarP_insertP: "invarP t \<Longrightarrow> invarP(insertP xs t)"
+proof(induction t arbitrary: xs)
+  case LfP thus ?case by simp
+next
+  case (NdP bs b lr)
+  then show ?case
+    by(cases lr)(auto simp: insertP_LfP split: prod.split list.split)
+qed
+
+(* Inlining this proof leads to nontermination *)
+lemma invarP_nodeP: "\<lbrakk> invarP t1; invarP t2\<rbrakk> \<Longrightarrow> invarP (nodeP xs b (t1, t2))"
+by (auto simp add: nodeP_def split: trieP.split)
+
+lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP(deleteP xs t)"
+proof(induction t arbitrary: xs)
+  case LfP thus ?case by simp
+next
+  case (NdP ks b lr)
+  thus ?case by(cases lr)(auto simp: invarP_nodeP split: prod.split list.split)
+qed
+
 
 text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
 
@@ -271,7 +358,7 @@
 
 interpretation SP: Set
 where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
-and set = set_trieP and invar = "\<lambda>t. True"
+and set = set_trieP and invar = invarP
 proof (standard, goal_cases)
   case 1 show ?case by (simp add: set_trieP_def set_trie_def)
 next
@@ -280,6 +367,12 @@
   case 3 thus ?case by (auto simp: set_trieP_insertP)
 next
   case 4 thus ?case by(auto simp: set_trieP_deleteP)
-qed (rule TrueI)+
+next
+  case 5 thus ?case by(simp)
+next
+  case 6 thus ?case by(rule invarP_insertP)
+next
+  case 7 thus ?case by(rule invarP_deleteP)
+qed
 
 end

--- a/src/HOL/Library/Multiset.thy	Thu Apr 13 23:53:12 2023 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 14 10:12:30 2023 +0200
@@ -3257,6 +3257,28 @@
   shows "monotone (multp orda) (multp ordb) (image_mset f)"
   by (rule monotone_on_multp_multp_image_mset[OF assms, simplified])
 
+lemma multp_image_mset_image_msetI:
+  assumes "multp (\<lambda>x y. R (f x) (f y)) M1 M2" and "transp R"
+  shows "multp R (image_mset f M1) (image_mset f M2)"
+proof -
+  from \<open>transp R\<close> have "transp (\<lambda>x y. R (f x) (f y))"
+    by (auto intro: transpI dest: transpD)
+  with \<open>multp (\<lambda>x y. R (f x) (f y)) M1 M2\<close> obtain I J K where
+    "M2 = I + J" and "M1 = I + K" and "J \<noteq> {#}" and "\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)"
+    using multp_implies_one_step by blast
+
+  have "multp R (image_mset f I + image_mset f K) (image_mset f I + image_mset f J)"
+  proof (rule one_step_implies_multp)
+    show "image_mset f J \<noteq> {#}"
+      by (simp add: \<open>J \<noteq> {#}\<close>)
+  next
+    show "\<forall>k\<in>#image_mset f K. \<exists>j\<in>#image_mset f J. R k j"
+      by (simp add: \<open>\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)\<close>)
+  qed
+  thus ?thesis
+    by (simp add: \<open>M1 = I + K\<close> \<open>M2 = I + J\<close>)
+qed
+
 lemma multp_image_mset_image_msetD:
   assumes
     "multp R (image_mset f A) (image_mset f B)" and

--- a/src/HOL/Library/Multiset_Order.thy	Thu Apr 13 23:53:12 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Fri Apr 14 10:12:30 2023 +0200
@@ -489,6 +489,47 @@
   by (meson less_eq_multiset_def mset_lt_single_right_iff)
 
 
+subsubsection \<open>Simplifications\<close>
+
+lemma multp\<^sub>H\<^sub>O_repeat_mset_repeat_mset[simp]:
+  assumes "n \<noteq> 0"
+  shows "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B) \<longleftrightarrow> multp\<^sub>H\<^sub>O R A B"
+proof (rule iffI)
+  assume hyp: "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
+  hence
+    1: "repeat_mset n A \<noteq> repeat_mset n B" and
+    2: "\<forall>y. n * count B y < n * count A y \<longrightarrow> (\<exists>x. R y x \<and> n * count A x < n * count B x)"
+    by (simp_all add: multp\<^sub>H\<^sub>O_def)
+
+  from 1 \<open>n \<noteq> 0\<close> have "A \<noteq> B"
+    by auto
+
+  moreover from 2 \<open>n \<noteq> 0\<close> have "\<forall>y. count B y < count A y \<longrightarrow> (\<exists>x. R y x \<and> count A x < count B x)"
+    by auto
+
+  ultimately show "multp\<^sub>H\<^sub>O R A B"
+    by (simp add: multp\<^sub>H\<^sub>O_def)
+next
+  assume "multp\<^sub>H\<^sub>O R A B"
+  hence 1: "A \<noteq> B" and 2: "\<forall>y. count B y < count A y \<longrightarrow> (\<exists>x. R y x \<and> count A x < count B x)"
+    by (simp_all add: multp\<^sub>H\<^sub>O_def)
+
+  from 1 have "repeat_mset n A \<noteq> repeat_mset n B"
+    by (simp add: assms repeat_mset_cancel1)
+
+  moreover from 2 have "\<forall>y. n * count B y < n * count A y \<longrightarrow>
+    (\<exists>x. R y x \<and> n * count A x < n * count B x)"
+    by auto
+
+  ultimately show "multp\<^sub>H\<^sub>O R (repeat_mset n A) (repeat_mset n B)"
+    by (simp add: multp\<^sub>H\<^sub>O_def)
+qed
+
+lemma multp\<^sub>H\<^sub>O_double_double[simp]: "multp\<^sub>H\<^sub>O R (A + A) (B + B) \<longleftrightarrow> multp\<^sub>H\<^sub>O R A B"
+  using multp\<^sub>H\<^sub>O_repeat_mset_repeat_mset[of 2]
+  by (simp add: numeral_Bit0)
+
+
 subsection \<open>Simprocs\<close>
 
 lemma mset_le_add_iff1: