diff --git a/thys/Registers/Axioms_Quantum.thy b/thys/Registers/Axioms_Quantum.thy
--- a/thys/Registers/Axioms_Quantum.thy
+++ b/thys/Registers/Axioms_Quantum.thy
@@ -1,157 +1,157 @@
 section \<open>Quantum instantiation of registers\<close>
 
 (* AXIOM INSTANTIATION (use instantiate_laws.py to generate Laws_Quantum.thy)
 
     # Type classes
     domain \<rightarrow> finite
 
     # Types
     some_domain \<rightarrow> unit
 
     # Constants
     comp_update \<rightarrow> cblinfun_compose
     id_update \<rightarrow> id_cblinfun
     preregister \<rightarrow> clinear
     tensor_update \<rightarrow> tensor_op
     
     # Lemmas
     id_update_left \<rightarrow> cblinfun_compose_id_left
     id_update_right \<rightarrow> cblinfun_compose_id_right
     comp_update_assoc \<rightarrow> cblinfun_compose_assoc
     id_preregister \<rightarrow> complex_vector.linear_id
     comp_preregister \<rightarrow> clinear_compose
     tensor_update_mult \<rightarrow> comp_tensor_op
     # preregister_tensor_left \<rightarrow> clinear_tensor_right
     # preregister_tensor_right \<rightarrow> clinear_tensor_left
 
     # Chapter name
     Generic laws about registers \<rightarrow> Generic laws about registers, instantiated quantumly
     Generic laws about complements \<rightarrow> Generic laws about complements, instantiated quantumly
 *)
 
 theory Axioms_Quantum
   imports Jordan_Normal_Form.Matrix_Impl "HOL-Library.Rewrite"
           Complex_Bounded_Operators.Complex_L2
           Finite_Tensor_Product
 begin
 
 
 unbundle cblinfun_notation
 no_notation m_inv ("inv\<index> _" [81] 80)
 
 type_synonym 'a update = \<open>('a ell2, 'a ell2) cblinfun\<close>
 
 lemma preregister_mult_right: \<open>clinear (\<lambda>a. a o\<^sub>C\<^sub>L z)\<close>
   by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
 lemma preregister_mult_left: \<open>clinear (\<lambda>a. z o\<^sub>C\<^sub>L a)\<close>
   by (meson cbilinear_cblinfun_compose cbilinear_def)
 
 definition register :: \<open>('a::finite update \<Rightarrow> 'b::finite update) \<Rightarrow> bool\<close> where
   "register F \<longleftrightarrow> 
      clinear F
    \<and> F id_cblinfun = id_cblinfun 
    \<and> (\<forall>a b. F(a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b)
    \<and> (\<forall>a. F (a*) = (F a)*)"
 
 lemma register_of_id: \<open>register F \<Longrightarrow> F id_cblinfun = id_cblinfun\<close>
   by (simp add: register_def)
 
 lemma register_id: \<open>register id\<close>
   by (simp add: register_def complex_vector.module_hom_id)
 
 lemma register_preregister: "register F \<Longrightarrow> clinear F"
   unfolding register_def by simp
 
 lemma register_comp: "register F \<Longrightarrow> register G \<Longrightarrow> register (G \<circ> F)"
   unfolding register_def
   apply auto
   using clinear_compose by blast
 
 lemma register_mult: "register F \<Longrightarrow> cblinfun_compose (F a) (F b) = F (cblinfun_compose a b)"
   unfolding register_def
   by auto
 
 lemma register_tensor_left: \<open>register (\<lambda>a. tensor_op a id_cblinfun)\<close>
   by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)
 
 lemma register_tensor_right: \<open>register (\<lambda>a. tensor_op id_cblinfun a)\<close>
   by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)
 
-
 definition register_pair ::
   \<open>('a::finite update \<Rightarrow> 'c::finite update) \<Rightarrow> ('b::finite update \<Rightarrow> 'c update)
          \<Rightarrow> (('a\<times>'b) update \<Rightarrow> 'c update)\<close> where
-  \<open>register_pair F G = tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b)\<close>
+  \<open>register_pair F G = (if register F \<and> register G \<and> (\<forall>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) then 
+                        tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b) else (\<lambda>_. 0))\<close>
 
 lemma cbilinear_F_comp_G[simp]: \<open>clinear F \<Longrightarrow> clinear G \<Longrightarrow> cbilinear (\<lambda>a b. F a o\<^sub>C\<^sub>L G b)\<close>
   unfolding cbilinear_def
   by (auto simp add: clinear_iff bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right)
 
 lemma register_pair_apply: 
-  assumes \<open>register F\<close> and \<open>register G\<close>
+  assumes [simp]: \<open>register F\<close> \<open>register G\<close>
   assumes \<open>\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a\<close>
   shows \<open>(register_pair F G) (tensor_op a b) = F a o\<^sub>C\<^sub>L G b\<close>
   unfolding register_pair_def
-  apply (subst tensor_lift_correct[THEN fun_cong, THEN fun_cong])
-   apply (rule cbilinear_F_comp_G)
-  using assms apply (auto intro!: cbilinear_F_comp_G)
-  using register_def by auto
+  apply (simp flip: assms(3))
+  by (metis assms(1) assms(2) cbilinear_F_comp_G register_preregister tensor_lift_correct)
 
 lemma register_pair_is_register:
   fixes F :: \<open>'a::finite update \<Rightarrow> 'c::finite update\<close> and G
   assumes [simp]: \<open>register F\<close> and [simp]: \<open>register G\<close>
   assumes \<open>\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a\<close>
   shows \<open>register (register_pair F G)\<close> 
 proof (unfold register_def, intro conjI allI)
   have [simp]: \<open>clinear F\<close> \<open>clinear G\<close>
     using assms register_def by blast+
   have [simp]: \<open>F id_cblinfun = id_cblinfun\<close> \<open>G id_cblinfun = id_cblinfun\<close>
     using assms(1,2) register_def by blast+
   show [simp]: \<open>clinear (register_pair F G)\<close>
-    unfolding register_pair_def apply (rule tensor_lift_clinear)
-    by simp
+    unfolding register_pair_def 
+    using assms apply auto
+    apply (rule tensor_lift_clinear)
+    by (simp flip: assms(3))
   show \<open>register_pair F G id_cblinfun = id_cblinfun\<close>
     apply (simp flip: tensor_id)
     apply (subst register_pair_apply)
     using assms by simp_all
   have [simp]: \<open>clinear (\<lambda>y. register_pair F G (x o\<^sub>C\<^sub>L y))\<close> for x :: \<open>('a\<times>'b) update\<close>
     apply (rule clinear_compose[unfolded o_def, where g=\<open>register_pair F G\<close>])
     by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
   have [simp]: \<open>clinear (\<lambda>y. x o\<^sub>C\<^sub>L register_pair F G y)\<close> for x :: \<open>'c update\<close>
     apply (rule clinear_compose[unfolded o_def, where f=\<open>register_pair F G\<close>])
     by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
   have [simp]: \<open>clinear (\<lambda>x. register_pair F G (x o\<^sub>C\<^sub>L y))\<close> for y :: \<open>('a\<times>'b) update\<close>
     apply (rule clinear_compose[unfolded o_def, where g=\<open>register_pair F G\<close>])
     by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
   have [simp]: \<open>clinear (\<lambda>x. register_pair F G x o\<^sub>C\<^sub>L y)\<close> for y :: \<open>'c update\<close>
     apply (rule clinear_compose[unfolded o_def, where f=\<open>register_pair F G\<close>])
     by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
   have [simp]: \<open>F (x o\<^sub>C\<^sub>L y) = F x o\<^sub>C\<^sub>L F y\<close> for x y
     by (simp add: register_mult)
   have [simp]: \<open>G (x o\<^sub>C\<^sub>L y) = G x o\<^sub>C\<^sub>L G y\<close> for x y
     by (simp add: register_mult)
   have [simp]: \<open>clinear (\<lambda>a. (register_pair F G (a*))*)\<close>
     apply (rule antilinear_o_antilinear[unfolded o_def, where f=\<open>adj\<close>])
      apply simp
     apply (rule antilinear_o_clinear[unfolded o_def, where g=\<open>adj\<close>])
     by (simp_all)
   have [simp]: \<open>F (a*) = (F a)*\<close> for a
     using assms(1) register_def by blast
   have [simp]: \<open>G (b*) = (G b)*\<close> for b
     using assms(2) register_def by blast
 
   fix a b
   show \<open>register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b\<close>
     apply (rule tensor_extensionality[THEN fun_cong, where x=b], simp_all)
     apply (rule tensor_extensionality[THEN fun_cong, where x=a], simp_all)
     apply (simp_all add: comp_tensor_op register_pair_apply assms(3))
     using assms(3)
     by (metis cblinfun_compose_assoc)
   have \<open>(register_pair F G (a*))* = register_pair F G a\<close>
     apply (rule tensor_extensionality[THEN fun_cong, where x=a])
     by (simp_all add: tensor_op_adjoint register_pair_apply assms(3))
   then show \<open>register_pair F G (a*) = register_pair F G a*\<close>
     by (metis double_adj)
 qed
 
 end
diff --git a/thys/Registers/Check_Autogenerated_Files.thy b/thys/Registers/Check_Autogenerated_Files.thy
new file mode 100644
--- /dev/null
+++ b/thys/Registers/Check_Autogenerated_Files.thy
@@ -0,0 +1,32 @@
+(*
+ * This is an autogenerated file. Do not edit.
+ * It was created using instantiate_laws.py.
+ * It checks whether the other autogenerated files are up-to-date.
+ *)
+
+theory Check_Autogenerated_Files
+  (* These imports are not actually needed, but in jEdit, they will conveniently trigger a re-execution of the checking code below upon changes. *)
+  imports Laws_Classical Laws_Quantum Laws_Complement_Quantum
+begin
+
+ML \<open>
+let
+  fun check kind file expected = let
+    val content = File.read (Path.append (Resources.master_directory \<^theory>) (Path.basic file))
+    val hash = SHA1.digest content |> SHA1.rep
+    in
+      if hash = expected then () else
+      error (kind ^ " file " ^ file ^ " has changed.\nPlease run \"python3 instantiate_laws.py\" to recreated autogenerated files.\nExpected SHA1 hash " ^ expected ^ ", got " ^ hash)
+    end
+in
+  check "Source" "Axioms_Classical.thy" "f4a0dac97bed23ec5b7c4cbf779f8eb2a12aa488";
+  check "Source" "Axioms_Quantum.thy" "b1ac4a827c2b943202c03611176d3c723119d8e1";
+  check "Source" "Laws.thy" "37803f67bcda2df6bf7abe2417d3bf49e6317dcd";
+  check "Source" "Laws_Complement.thy" "6065101853fa432ca4bd6fd3113315e856e21ecb";
+  check "Generated" "Laws_Classical.thy" "051bc83ae9bd061fba08bfa29468a3421817068b";
+  check "Generated" "Laws_Complement_Quantum.thy" "c58ba1680287643d1c3f9b2b97d9784db8e1dd84";
+  check "Generated" "Laws_Quantum.thy" "36d05e686993e4f9b7c5bf57639d840b3e9b2e47"
+end
+\<close>
+
+end
diff --git a/thys/Registers/Classical_Extra.thy b/thys/Registers/Classical_Extra.thy
--- a/thys/Registers/Classical_Extra.thy
+++ b/thys/Registers/Classical_Extra.thy
@@ -1,141 +1,144 @@
 section \<open>Derived facts about classical registers\<close>
 
 theory Classical_Extra
   imports Laws_Classical Misc
 begin
 
 lemma register_from_getter_setter_of_getter_setter[simp]: \<open>register_from_getter_setter (getter F) (setter F) = F\<close> if \<open>register F\<close>
   by (metis getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter that)
 
 lemma valid_getter_setter_getter_setter[simp]: \<open>valid_getter_setter (getter F) (setter F)\<close> if \<open>register F\<close>
   by (metis getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter that)
 
 lemma register_register_from_getter_setter[simp]: \<open>register (register_from_getter_setter g s)\<close> if \<open>valid_getter_setter g s\<close>
   using register_def that by blast
 
 definition \<open>total_fun f = (\<forall>x. f x \<noteq> None)\<close>
 
 lemma register_total:
   assumes \<open>register F\<close>
   assumes \<open>total_fun a\<close>
   shows \<open>total_fun (F a)\<close>
   using assms 
   by (auto simp: register_def total_fun_def register_from_getter_setter_def option.case_eq_if)
 
 lemma register_apply:
   assumes \<open>register F\<close>
   shows \<open>Some o register_apply F a = F (Some o a)\<close>
 proof -
   have \<open>total_fun (F (Some o a))\<close>
     using assms apply (rule register_total)
     by (auto simp: total_fun_def)
   then show ?thesis
     by (auto simp: register_apply_def dom_def total_fun_def)
 qed
 
 lemma register_empty:
   assumes \<open>preregister F\<close>
   shows \<open>F Map.empty = Map.empty\<close>
   using assms unfolding preregister_def by auto
 
 lemma compatible_setter:
   fixes F :: \<open>('a,'c) preregister\<close> and G :: \<open>('b,'c) preregister\<close>
   assumes [simp]: \<open>register F\<close> \<open>register G\<close>
   shows \<open>compatible F G \<longleftrightarrow> (\<forall>a b. setter F a o setter G b = setter G b o setter F a)\<close>
 proof (intro allI iffI)
   fix a b
   assume \<open>compatible F G\<close>
   then show \<open>setter F a o setter G b = setter G b o setter F a\<close>
     apply (rule_tac compatible_setter)
     unfolding compatible_def by auto
 next
   assume commute[rule_format, THEN fun_cong, unfolded o_def]: \<open>\<forall>a b. setter F a \<circ> setter G b = setter G b \<circ> setter F a\<close>
   have \<open>valid_getter_setter (getter F) (setter F)\<close>
     by auto
   then have \<open>F a \<circ>\<^sub>m G b = G b \<circ>\<^sub>m F a\<close> for a b
     apply (subst (2) register_from_getter_setter_of_getter_setter[symmetric, of F], simp)
     apply (subst (1) register_from_getter_setter_of_getter_setter[symmetric, of F], simp)
     apply (subst (2) register_from_getter_setter_of_getter_setter[symmetric, of G], simp)
     apply (subst (1) register_from_getter_setter_of_getter_setter[symmetric, of G], simp)
     unfolding register_from_getter_setter_def valid_getter_setter_def
     apply (auto intro!: ext simp: option.case_eq_if map_comp_def) (* Sledgehammer: *)
           apply ((metis commute option.distinct option.simps)+)[4]
       apply (smt (verit, ccfv_threshold) assms(2) commute valid_getter_setter_def valid_getter_setter_getter_setter)
      apply (smt (verit, ccfv_threshold) assms(2) commute valid_getter_setter_def valid_getter_setter_getter_setter)
     by (smt (verit, del_insts) assms(2) commute option.inject valid_getter_setter_def valid_getter_setter_getter_setter)
   then show \<open>compatible F G\<close>
     unfolding compatible_def by auto
 qed
 
 lemma register_from_getter_setter_compatibleI[intro]:
   assumes [simp]: \<open>valid_getter_setter g s\<close> \<open>valid_getter_setter g' s'\<close>
   assumes \<open>\<And>x y m. s x (s' y m) = s' y (s x m)\<close>
   shows \<open>compatible (register_from_getter_setter g s) (register_from_getter_setter g' s')\<close>
   apply (subst compatible_setter)
   using assms by auto
 
 lemma separating_update1:
   \<open>separating TYPE(_) {update1 x y | x y. True}\<close>
   by (smt (verit) mem_Collect_eq separating_def update1_extensionality)
 
 definition "permutation_register (p::'b\<Rightarrow>'a) = register_from_getter_setter p (\<lambda>a _. inv p a)"
 
 lemma permutation_register_register[simp]: 
   fixes p :: "'b \<Rightarrow> 'a"
   assumes [simp]: "bij p"
   shows "register (permutation_register p)"
   apply (auto intro!: register_register_from_getter_setter simp: permutation_register_def valid_getter_setter_def bij_inv_eq_iff)
   by (meson assms bij_inv_eq_iff)
 
 lemma getter_permutation_register: \<open>bij p \<Longrightarrow> getter (permutation_register p) = p\<close>
   by (smt (verit, ccfv_threshold) bij_inv_eq_iff getter_of_register_from_getter_setter permutation_register_def valid_getter_setter_def)
 
 lemma setter_permutation_register: \<open>bij p \<Longrightarrow> setter (permutation_register p) a m = inv p a\<close>
   by (metis bij_inv_eq_iff getter_permutation_register permutation_register_register valid_getter_setter_def valid_getter_setter_getter_setter)
 
 definition empty_var :: \<open>'a::{CARD_1} update \<Rightarrow> 'b update\<close> where
   "empty_var = register_from_getter_setter (\<lambda>_. undefined) (\<lambda>_ m. m)"
 
 lemma valid_empty_var[simp]: \<open>valid_getter_setter (\<lambda>_. (undefined::_::CARD_1)) (\<lambda>_ m. m)\<close>
   by (simp add: valid_getter_setter_def)
 
 lemma register_empty_var[simp]: \<open>register empty_var\<close>
   using empty_var_def register_def valid_empty_var by blast
 
 lemma getter_empty_var[simp]: \<open>getter empty_var m = undefined\<close>
   by (rule everything_the_same)
 
 lemma setter_empty_var[simp]: \<open>setter empty_var a m = m\<close>
   by (simp add: empty_var_def setter_of_register_from_getter_setter)
 
 lemma empty_var_compatible[simp]: \<open>compatible empty_var X\<close> if [simp]: \<open>register X\<close>
   apply (subst compatible_setter) by auto
 
 lemma empty_var_compatible'[simp]: \<open>register X \<Longrightarrow> compatible X empty_var\<close>
   using compatible_sym empty_var_compatible by blast
 
 paragraph \<open>Example\<close>
 
 record memory = 
   x :: "int*int"
   y :: nat
 
 definition "X = register_from_getter_setter x (\<lambda>a b. b\<lparr>x:=a\<rparr>)"
 definition "Y = register_from_getter_setter y (\<lambda>a b. b\<lparr>y:=a\<rparr>)"
 
 lemma validX[simp]: \<open>valid_getter_setter x (\<lambda>a b. b\<lparr>x:=a\<rparr>)\<close>
   unfolding valid_getter_setter_def by auto
 
 lemma registerX[simp]: \<open>register X\<close>
   using X_def register_def validX by blast
 
 lemma validY[simp]: \<open>valid_getter_setter y (\<lambda>a b. b\<lparr>y:=a\<rparr>)\<close>
   unfolding valid_getter_setter_def by auto
 
 lemma registerY[simp]: \<open>register Y\<close>
   using Y_def register_def validY by blast
 
 lemma compatibleXY[simp]: \<open>compatible X Y\<close>
   unfolding X_def Y_def by auto
 
+(* Avoiding namespace pollution *)
+hide_const (open) x y x_update y_update X Y
+
 end
diff --git a/thys/Registers/Quantum_Extra.thy b/thys/Registers/Quantum_Extra.thy
--- a/thys/Registers/Quantum_Extra.thy
+++ b/thys/Registers/Quantum_Extra.thy
@@ -1,151 +1,162 @@
 section \<open>Derived facts about quantum registers\<close>
 
 theory Quantum_Extra
   imports
     Laws_Quantum
     Quantum
 begin
 
 no_notation meet (infixl "\<sqinter>\<index>" 70)
 no_notation Group.mult (infixl "\<otimes>\<index>" 70)
 no_notation Order.top ("\<top>\<index>")
 unbundle register_notation
 unbundle cblinfun_notation
 
+lemma zero_not_register[simp]: \<open>~ register (\<lambda>_. 0)\<close>
+  unfolding register_def by simp
+
+lemma register_pair_is_register_converse:
+  \<open>register (F;G) \<Longrightarrow> register F\<close> \<open>register (F;G) \<Longrightarrow> register G\<close>
+  using [[simproc del: Laws_Quantum.compatibility_warn]]
+   apply (cases \<open>register F\<close>)
+    apply (auto simp: register_pair_def)[2]
+  apply (cases \<open>register G\<close>)
+  by (auto simp: register_pair_def)[2]
+
 lemma register_id'[simp]: \<open>register (\<lambda>x. x)\<close>
   using register_id by (simp add: id_def)
 
 lemma register_projector:
   assumes "register F"
   assumes "is_Proj a"
   shows "is_Proj (F a)"
   using assms unfolding register_def is_Proj_algebraic by metis
 
 lemma register_unitary:
   assumes "register F"
   assumes "unitary a"
   shows "unitary (F a)"
   using assms by (smt (verit, best) register_def unitary_def)
 
 lemma compatible_proj_intersect:
   (* I think this also holds without is_Proj premises, but my proof ideas use the Penrose-Moore 
      pseudoinverse or simultaneous diagonalization and we do not have an existence theorem for either. *)
   assumes "compatible R S" and "is_Proj a" and "is_Proj b"
   shows "(R a *\<^sub>S \<top>) \<sqinter> (S b *\<^sub>S \<top>) = ((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>)"
 proof (rule antisym)
   have "((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>) \<le> (S b *\<^sub>S \<top>)"
     apply (subst swap_registers[OF assms(1)])
     by (simp add: cblinfun_compose_image cblinfun_image_mono)
   moreover have "((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>) \<le> (R a *\<^sub>S \<top>)"
     by (simp add: cblinfun_compose_image cblinfun_image_mono)
   ultimately show \<open>((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>) \<le> (R a *\<^sub>S \<top>) \<sqinter> (S b *\<^sub>S \<top>)\<close>
     by auto
 
   have "is_Proj (R a)"
     using assms(1) assms(2) compatible_register1 register_projector by blast
   have "is_Proj (S b)"
     using assms(1) assms(3) compatible_register2 register_projector by blast
   show \<open>(R a *\<^sub>S \<top>) \<sqinter> (S b *\<^sub>S \<top>) \<le> (R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>\<close>
   proof (unfold less_eq_ccsubspace.rep_eq, rule)
     fix \<psi>
     assume asm: \<open>\<psi> \<in> space_as_set ((R a *\<^sub>S \<top>) \<sqinter> (S b *\<^sub>S \<top>))\<close>
     then have \<open>\<psi> \<in> space_as_set (R a *\<^sub>S \<top>)\<close>
       by auto
     then have R: \<open>R a *\<^sub>V \<psi> = \<psi>\<close>
       using \<open>is_Proj (R a)\<close> cblinfun_fixes_range is_Proj_algebraic by blast
     from asm have \<open>\<psi> \<in> space_as_set (S b *\<^sub>S \<top>)\<close>
       by auto
     then have S: \<open>S b *\<^sub>V \<psi> = \<psi>\<close>
       using \<open>is_Proj (S b)\<close> cblinfun_fixes_range is_Proj_algebraic by blast
     from R S have \<open>\<psi> = (R a o\<^sub>C\<^sub>L S b) *\<^sub>V \<psi>\<close>
       by (simp add: cblinfun_apply_cblinfun_compose)
     also have \<open>\<dots> \<in> space_as_set ((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>)\<close>
       apply simp by (metis R S calculation cblinfun_apply_in_image)
     finally show \<open>\<psi> \<in> space_as_set ((R a o\<^sub>C\<^sub>L S b) *\<^sub>S \<top>)\<close>
       by -
   qed
 qed
 
 lemma compatible_proj_mult:
   assumes "compatible R S" and "is_Proj a" and "is_Proj b"
   shows "is_Proj (R a o\<^sub>C\<^sub>L S b)"
   using [[simproc del: Laws_Quantum.compatibility_warn]]
   using assms unfolding is_Proj_algebraic compatible_def
   apply auto
    apply (metis (no_types, lifting) cblinfun_compose_assoc register_mult)
   by (simp add: assms(2) assms(3) is_proj_selfadj register_projector)
 
 lemma unitary_sandwich_register: \<open>unitary a \<Longrightarrow> register (sandwich a)\<close>
   unfolding register_def
   apply (auto simp: sandwich_def)
    apply (metis (no_types, lifting) cblinfun_assoc_left(1) cblinfun_compose_id_right unitaryD1)
   by (simp add: lift_cblinfun_comp(2))
 
 lemma sandwich_tensor: 
   fixes a :: \<open>'a::finite ell2 \<Rightarrow>\<^sub>C\<^sub>L 'a ell2\<close> and b :: \<open>'b::finite ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b ell2\<close> 
   assumes \<open>unitary a\<close> \<open>unitary b\<close>
   shows "sandwich (a \<otimes>\<^sub>o b) = sandwich a \<otimes>\<^sub>r sandwich b"
   apply (rule tensor_extensionality)
   by (auto simp: unitary_sandwich_register assms sandwich_def register_tensor_is_register comp_tensor_op tensor_op_adjoint)
 
 lemma sandwich_grow_left: 
   fixes a :: \<open>'a::finite ell2 \<Rightarrow>\<^sub>C\<^sub>L 'a ell2\<close>
   assumes "unitary a"
   shows "sandwich a \<otimes>\<^sub>r id = sandwich (a \<otimes>\<^sub>o id_cblinfun)"
   by (simp add: unitary_sandwich_register assms sandwich_tensor sandwich_id)
 
 lemma register_sandwich: \<open>register F \<Longrightarrow> F (sandwich a b) = sandwich (F a) (F b)\<close>
   by (smt (verit, del_insts) register_def sandwich_def)
 
 lemma assoc_ell2_sandwich: \<open>assoc = sandwich assoc_ell2\<close>
   apply (rule tensor_extensionality3')
     apply (simp_all add: unitary_sandwich_register)[2]
   apply (rule equal_ket)
   apply (case_tac x)
   by (simp add: sandwich_def assoc_apply cblinfun_apply_cblinfun_compose tensor_op_ell2 assoc_ell2_tensor assoc_ell2'_tensor
            flip: tensor_ell2_ket)
 
 lemma assoc_ell2'_sandwich: \<open>assoc' = sandwich assoc_ell2'\<close>
   apply (rule tensor_extensionality3)
     apply (simp_all add: unitary_sandwich_register)[2]
   apply (rule equal_ket)
   apply (case_tac x)
   by (simp add: sandwich_def assoc'_apply cblinfun_apply_cblinfun_compose tensor_op_ell2 assoc_ell2_tensor assoc_ell2'_tensor 
            flip: tensor_ell2_ket)
 
 lemma swap_sandwich: "swap = sandwich Uswap"
   apply (rule tensor_extensionality)
     apply (auto simp: sandwich_def)[2]
   apply (rule tensor_ell2_extensionality)
   by (simp add: sandwich_def cblinfun_apply_cblinfun_compose tensor_op_ell2)
 
 lemma id_tensor_sandwich: 
   fixes a :: "'a::finite ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::finite ell2"
   assumes "unitary a"
   shows "id \<otimes>\<^sub>r sandwich a = sandwich (id_cblinfun \<otimes>\<^sub>o a)"
   apply (rule tensor_extensionality) 
   using assms by (auto simp: register_tensor_is_register comp_tensor_op sandwich_def tensor_op_adjoint unitary_sandwich_register)
 
 lemma compatible_selfbutter_join:
   assumes [register]: "compatible R S"
   shows "R (selfbutter \<psi>) o\<^sub>C\<^sub>L S (selfbutter \<phi>) = (R; S) (selfbutter (\<psi> \<otimes>\<^sub>s \<phi>))"
   apply (subst register_pair_apply[symmetric, where F=R and G=S])
   using assms by auto
 
 lemma register_mult':
   assumes \<open>register F\<close>
   shows \<open>F a *\<^sub>V F b *\<^sub>V c = F (a o\<^sub>C\<^sub>L b) *\<^sub>V c\<close>
   by (simp add: assms lift_cblinfun_comp(4) register_mult)
 
 lemma register_scaleC:
   assumes \<open>register F\<close> shows \<open>F (c *\<^sub>C a) = c *\<^sub>C F a\<close>
   by (simp add: assms complex_vector.linear_scale)
 
 lemma register_bounded_clinear: \<open>register F \<Longrightarrow> bounded_clinear F\<close>
   using bounded_clinear_finite_dim register_def by blast
 
 lemma register_adjoint: "F (a*) = (F a)*" if \<open>register F\<close>
   using register_def that by blast
 
 end
 
diff --git a/thys/Registers/ROOT b/thys/Registers/ROOT
--- a/thys/Registers/ROOT
+++ b/thys/Registers/ROOT
@@ -1,13 +1,14 @@
 chapter AFP
 
 session Registers (AFP) = Complex_Bounded_Operators +
   options [timeout = 1200]
   theories
     Laws_Complement
     Classical_Extra
     Teleport
     Laws_Complement_Quantum
     Pure_States
+    Check_Autogenerated_Files
   document_files 
     root.tex
     root.bib
diff --git a/thys/Registers/instantiate_laws.py b/thys/Registers/instantiate_laws.py
--- a/thys/Registers/instantiate_laws.py
+++ b/thys/Registers/instantiate_laws.py
@@ -1,127 +1,184 @@
 #!/usr/bin/python3
 import glob
 import os
 import re
 import sys
+from hashlib import sha1
 from stat import S_IREAD, S_IRGRP, S_IROTH
-from typing import Union, Collection, Match, Dict, Optional, Tuple
+from typing import Union, Collection, Match, Dict, Optional, Tuple, Any, Set
 
 had_errors = False
 
+source_files: set[str] = set()
+generated_files: set[str] = set()
+
 
 def multisubst(mappings: Collection[(Union[re.Pattern, str])], content: str) -> str:
     replacements = []
     patterns = []
     i = 0
     for pat, repl in mappings:
         if isinstance(pat, str):
             pat_str = re.escape(pat)
         else:
             pat_str = pat.pattern
         replacements.append(repl)
         patterns.append(f"(?P<GROUP_{i}>\\b(?:{pat_str})\\b)")
         i += 1
 
     pattern = re.compile("|".join(patterns))
 
     def repl_func(m: Match):
         # print(m)
         for name, text in m.groupdict().items():
             if text is None:
                 continue
             if text.startswith("GROUP_"):
                 continue
             idx = int(name[6:])
             # print(name, idx)
             return replacements[idx]
         assert False
 
     return pattern.sub(repl_func, content)
 
 def write_to_file(file, content):
+    global generated_files
+    generated_files.add(file)
     try:
         with open(file, 'rt') as f:
             old_content = f.read()
         if content == old_content:
             print("(Nothing changed, not writing.)")
             return
         os.remove(file)
     except FileNotFoundError: pass
 
     with open(file, 'wt') as f:
         f.write(content)
     os.chmod(file, S_IREAD | S_IRGRP | S_IROTH)
 
 
 def rewrite_laws(outputfile: str, template: str, substitutions: Dict[str, str]):
+    global source_files
     print(f"Rewriting {template} -> {outputfile}")
+    source_files.add(template)
     with open(template, 'rt') as f:
         content = f.read()
     new_content = multisubst(substitutions.items(), content)
 
     new_content = f"""(*
  * This is an autogenerated file. Do not edit.
  * The original is {template}. It was converted using instantiate_laws.py.
  *)
 
 """ + new_content
 
     write_to_file(outputfile, new_content)
 
 
 def read_instantiation_header(file: str) -> Optional[Tuple[str, Optional[str], Dict[str, str]]]:
+    global source_files
     global had_errors
+    source_files.add(file)
     with open(file, 'rt') as f:
         content = f.read()
 
     assert file.startswith("Axioms_")
     basename = file[len("Axioms_"):]
     assert basename.endswith(".thy")
     basename = basename[:-len(".thy")]
 
     m = re.compile(r"""\(\* AXIOM INSTANTIATION [^\n]*\n(.*?)\*\)""", re.DOTALL).search(content)
     if m is None:
         print(f"*** Could not find AXIOM INSTANTIATION header in {file}.")
         had_errors = True
         lines = []
     else:
         lines = m.group(1).splitlines()
     substitutions = {
         'theory Laws': f'theory Laws_{basename}',
         'imports Laws': f'imports Laws_{basename}',
         'theory Laws_Complement': f'theory Laws_Complement_{basename}',
         'Axioms': f'Axioms_{basename}',
         'Axioms_Complement': f'Axioms_Complement_{basename}'
     }
     # print(substitutions)
     for line in lines:
         if line.strip() == "":
             continue
         if re.match(r"^\s*#", line):
             continue
         m = re.match(r"^\s*(.+?)\s+\\<rightarrow>\s+(.+?)\s*$", line)
         if m is None:
             print(f"*** Invalid AXIOM INSTANTIATION line in {file}: {line}")
             had_errors = True
             continue
         key = m.group(1)
         val = m.group(2)
         if key in substitutions:
             print(f"*** Repeated AXIOM INSTANTIATION key in {file}: {line}")
             had_errors = True
         substitutions[key] = val
     # print(substitutions)
     laws_complement = f"Laws_Complement_{basename}.thy" if os.path.exists(f"Axioms_Complement_{basename}.thy") else None
     return (f"Laws_{basename}.thy", laws_complement, substitutions)
 
 def rewrite_all():
     for f in glob.glob("Axioms_*.thy"):
         if f.startswith("Axioms_Complement"): continue
         lawfile, lawfile_complement, substitutions = read_instantiation_header(f)
         rewrite_laws(lawfile, "Laws.thy", substitutions)
         if lawfile_complement is not None:
             rewrite_laws(lawfile_complement, "Laws_Complement.thy", substitutions)
 
+
+def create_check_theory():
+    global source_files, generated_files
+
+    print("Creating Check_Autogenerated_Files.thy")
+
+    hash_checks = []
+    for kind, files in (("Source", source_files), ("Generated", generated_files)):
+        for file in sorted(files):
+            with open(file, 'rb') as f:
+                hash = sha1(f.read()).hexdigest()
+            hash_checks.append(f'  check "{kind}" "{file}" "{hash}"')
+
+    hash_checks_concat = ";\n".join(hash_checks)
+
+    content = rf"""(*
+ * This is an autogenerated file. Do not edit.
+ * It was created using instantiate_laws.py.
+ * It checks whether the other autogenerated files are up-to-date.
+ *)
+
+theory Check_Autogenerated_Files
+  (* These imports are not actually needed, but in jEdit, they will conveniently trigger a re-execution of the checking code below upon changes. *)
+  imports Laws_Classical Laws_Quantum Laws_Complement_Quantum
+begin
+
+ML \<open>
+let
+  fun check kind file expected = let
+    val content = File.read (Path.append (Resources.master_directory \<^theory>) (Path.basic file))
+    val hash = SHA1.digest content |> SHA1.rep
+    in
+      if hash = expected then () else
+      error (kind ^ " file " ^ file ^ " has changed.\nPlease run \"python3 instantiate_laws.py\" to recreated autogenerated files.\nExpected SHA1 hash " ^ expected ^ ", got " ^ hash)
+    end
+in
+{hash_checks_concat}
+end
+\<close>
+
+end
+"""
+
+    write_to_file("Check_Autogenerated_Files.thy", content)
+
+
 rewrite_all()
+create_check_theory()
 if had_errors:
-    sys.exit(1)
\ No newline at end of file
+    sys.exit(1)