Basics.thy:

- Line 104. Lemma without a name with [simp] attribute.

lemma [simp]:

shows "2 * (cmod (1 / complex_of_real (sqrt 2)))⇧2 = 1"

using cmod_def by (simp add: power_divide)

I suggest two_div_sqr_of_cmd_sqrt_two to stay within the name convention used for the other lemmas in the theory but shorter names are welcome.

Tensor.thy:

line 461. Fact linordered_field_class.sign_simps(4) cannot be found. Proof can be replaced with

by (smt ab_semigroup_mult_class.mult_ac(1) length_greater_0_conv length_mat_to_cols_list

mat_to_cols_list_is_mat mult.Tensor.simps(1) mult.Tensor_null plus_mult_cpx plus_mult_def)

Changed one metis proof in Deutsch_Joza by one that requires less time.

Theory No_Cloning line 193. Assumptions have [simp] attributes. Do they need a name too? I am not sure what the [simp] does here.

Added Measurement to ROOT since all theory files of the submission must be contained in at least one session.

Last updated: Sep 25 2022 at 23:25 UTC