--- a/src/CTT/ex/Elimination.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/CTT/ex/Elimination.thy Wed Oct 26 21:59:16 2022 +0200
@@ -19,17 +19,17 @@
done
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
-apply pc
-back
-done
+ apply pc
+ back
+ done
text "Double negation of the Excluded Middle"
schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
-apply intr
-apply (rule ProdE)
-apply assumption
-apply pc
-done
+ apply intr
+ apply (rule ProdE)
+ apply assumption
+ apply pc
+ done
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
apply pc
@@ -39,13 +39,12 @@
text "Binary sums and products"
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
-apply pc
-done
+ apply pc
+ done
(*A distributive law*)
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"
-apply pc
-done
+ by pc
(*more general version, same proof*)
schematic_goal
@@ -53,13 +52,13 @@
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x. x:A \<Longrightarrow> C(x) type"
shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
text "Construction of the currying functional"
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
-apply pc
-done
+ apply pc
+ done
(*more general goal with same proof*)
schematic_goal
@@ -68,13 +67,13 @@
and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> C(z) type"
shows "?a : \<Prod>f: (\<Prod>z : (\<Sum>x:A . B(x)) . C(z)).
(\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
-apply pc
-done
+ apply pc
+ done
(*more general goal with same proof*)
schematic_goal
@@ -83,13 +82,13 @@
and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"
shows "?a : (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))
\<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
text "Function application"
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
-apply pc
-done
+ apply pc
+ done
text "Basic test of quantifier reasoning"
schematic_goal
@@ -99,8 +98,8 @@
shows
"?a : (\<Sum>y:B . \<Prod>x:A . C(x,y))
\<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
text "Martin-Löf (1984) pages 36-7: the combinator S"
schematic_goal
@@ -109,8 +108,8 @@
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
shows "?a : (\<Prod>x:A. \<Prod>y:B(x). C(x,y))
\<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
schematic_goal
@@ -119,14 +118,14 @@
and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))
\<longrightarrow> (\<Prod>z: A+B. C(z))"
-apply (pc assms)
-done
+ apply (pc assms)
+ done
(*towards AXIOM OF CHOICE*)
schematic_goal [folded basic_defs]:
"\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"
-apply pc
-done
+ apply pc
+ done
(*Martin-Löf (1984) page 50*)
@@ -136,16 +135,16 @@
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
-apply (intr assms)
-prefer 2 apply add_mp
-prefer 2 apply add_mp
-apply (erule SumE_fst)
-apply (rule replace_type)
-apply (rule subst_eqtyparg)
-apply (rule comp_rls)
-apply (rule_tac [4] SumE_snd)
-apply (typechk SumE_fst assms)
-done
+ apply (intr assms)
+ prefer 2 apply add_mp
+ prefer 2 apply add_mp
+ apply (erule SumE_fst)
+ apply (rule replace_type)
+ apply (rule subst_eqtyparg)
+ apply (rule comp_rls)
+ apply (rule_tac [4] SumE_snd)
+ apply (typechk SumE_fst assms)
+ done
text "Axiom of choice. Proof without fst, snd. Harder still!"
schematic_goal [folded basic_defs]:
@@ -153,42 +152,42 @@
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
-apply (intr assms)
-(*Must not use add_mp as subst_prodE hides the construction.*)
-apply (rule ProdE [THEN SumE])
-apply assumption
-apply assumption
-apply assumption
-apply (rule replace_type)
-apply (rule subst_eqtyparg)
-apply (rule comp_rls)
-apply (erule_tac [4] ProdE [THEN SumE])
-apply (typechk assms)
-apply (rule replace_type)
-apply (rule subst_eqtyparg)
-apply (rule comp_rls)
-apply (typechk assms)
-apply assumption
-done
+ apply (intr assms)
+ (*Must not use add_mp as subst_prodE hides the construction.*)
+ apply (rule ProdE [THEN SumE])
+ apply assumption
+ apply assumption
+ apply assumption
+ apply (rule replace_type)
+ apply (rule subst_eqtyparg)
+ apply (rule comp_rls)
+ apply (erule_tac [4] ProdE [THEN SumE])
+ apply (typechk assms)
+ apply (rule replace_type)
+ apply (rule subst_eqtyparg)
+ apply (rule comp_rls)
+ apply (typechk assms)
+ apply assumption
+ done
text "Example of sequent-style deduction"
-(*When splitting z:A \<times> B, the assumption C(z) is affected; ?a becomes
+ (*When splitting z:A \<times> B, the assumption C(z) is affected; ?a becomes
\<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w) *)
schematic_goal
assumes "A type"
and "B type"
and "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"
shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"
-apply (rule intr_rls)
-apply (tactic \<open>biresolve_tac \<^context> safe_brls 2\<close>)
-(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
-apply (rule_tac [2] a = "y" in ProdE)
-apply (typechk assms)
-apply (rule SumE, assumption)
-apply intr
-defer 1
-apply assumption+
-apply (typechk assms)
-done
+ apply (rule intr_rls)
+ apply (tactic \<open>biresolve_tac \<^context> safe_brls 2\<close>)
+ (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
+ apply (rule_tac [2] a = "y" in ProdE)
+ apply (typechk assms)
+ apply (rule SumE, assumption)
+ apply intr
+ defer 1
+ apply assumption+
+ apply (typechk assms)
+ done
end
--- a/src/CTT/ex/Equality.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/CTT/ex/Equality.thy Wed Oct 26 21:59:16 2022 +0200
@@ -6,63 +6,62 @@
section "Equality reasoning by rewriting"
theory Equality
-imports "../CTT"
+ imports "../CTT"
begin
lemma split_eq: "p : Sum(A,B) \<Longrightarrow> split(p,pair) = p : Sum(A,B)"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+ apply (rule EqE)
+ apply (rule elim_rls, assumption)
+ apply rew
+ done
lemma when_eq: "\<lbrakk>A type; B type; p : A+B\<rbrakk> \<Longrightarrow> when(p,inl,inr) = p : A + B"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+ apply (rule EqE)
+ apply (rule elim_rls, assumption)
+ apply rew
+ done
-(*in the "rec" formulation of addition, 0+n=n *)
+text \<open>in the "rec" formulation of addition, $0+n=n$\<close>
lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(y)) = p : N"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply rew
-done
+ apply (rule EqE)
+ apply (rule elim_rls, assumption)
+ apply rew
+ done
-(*the harder version, n+0=n: recursive, uses induction hypothesis*)
+text \<open>the harder version, $n+0=n$: recursive, uses induction hypothesis\<close>
lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(z)) = p : N"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply hyp_rew
-done
+ apply (rule EqE)
+ apply (rule elim_rls, assumption)
+ apply hyp_rew
+ done
-(*Associativity of addition*)
+text \<open>Associativity of addition\<close>
lemma "\<lbrakk>a:N; b:N; c:N\<rbrakk>
\<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) =
rec(a, rec(b, c, \<lambda>x y. succ(y)), \<lambda>x y. succ(y)) : N"
-apply (NE a)
-apply hyp_rew
-done
+ apply (NE a)
+ apply hyp_rew
+ done
-(*Martin-Löf (1984) page 62: pairing is surjective*)
+text \<open>Martin-Löf (1984) page 62: pairing is surjective\<close>
lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>x y. y)> = p : Sum(A,B)"
-apply (rule EqE)
-apply (rule elim_rls, assumption)
-apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
-done
+ apply (rule EqE)
+ apply (rule elim_rls, assumption)
+ apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
+ done
lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"
-apply rew
-done
+ by rew
-(*a contrived, complicated simplication, requires sum-elimination also*)
+text \<open>a contrived, complicated simplication, requires sum-elimination also\<close>
lemma "(\<^bold>\<lambda>f. \<^bold>\<lambda>x. f`(f`x)) ` (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) =
\<^bold>\<lambda>x. x : \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"
-apply (rule reduction_rls)
-apply (rule_tac [3] intrL_rls)
-apply (rule_tac [4] EqE)
-apply (erule_tac [4] SumE)
-(*order of unifiers is essential here*)
-apply rew
-done
+ apply (rule reduction_rls)
+ apply (rule_tac [3] intrL_rls)
+ apply (rule_tac [4] EqE)
+ apply (erule_tac [4] SumE)
+ (*order of unifiers is essential here*)
+ apply rew
+ done
end
--- a/src/CTT/ex/Synthesis.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/CTT/ex/Synthesis.thy Wed Oct 26 21:59:16 2022 +0200
@@ -6,40 +6,40 @@
section "Synthesis examples, using a crude form of narrowing"
theory Synthesis
-imports "../CTT"
+ imports "../CTT"
begin
text "discovery of predecessor function"
schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
-apply intr
-apply eqintr
-apply (rule_tac [3] reduction_rls)
-apply (rule_tac [5] comp_rls)
-apply rew
-done
+ apply intr
+ apply eqintr
+ apply (rule_tac [3] reduction_rls)
+ apply (rule_tac [5] comp_rls)
+ apply rew
+ done
text "the function fst as an element of a function type"
schematic_goal [folded basic_defs]:
"A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
-apply intr
-apply eqintr
-apply (rule_tac [2] reduction_rls)
-apply (rule_tac [4] comp_rls)
-apply typechk
-txt "now put in A everywhere"
-apply assumption+
-done
+ apply intr
+ apply eqintr
+ apply (rule_tac [2] reduction_rls)
+ apply (rule_tac [4] comp_rls)
+ apply typechk
+ txt "now put in A everywhere"
+ apply assumption+
+ done
text "An interesting use of the eliminator, when"
-(*The early implementation of unification caused non-rigid path in occur check
+ (*The early implementation of unification caused non-rigid path in occur check
See following example.*)
schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0 , i>)
\<times> Eq(?A, ?b(inr(i)), <succ(0), i>)"
-apply intr
-apply eqintr
-apply (rule comp_rls)
-apply rew
-done
+ apply intr
+ apply eqintr
+ apply (rule comp_rls)
+ apply rew
+ done
(*Here we allow the type to depend on i.
This prevents the cycle in the first unification (no longer needed).
@@ -47,58 +47,58 @@
Simpler still: make ?A into a constant type N \<times> N.*)
schematic_goal "?a : \<Prod>i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
\<times> Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
-oops
+ oops
-text "A tricky combination of when and split"
-(*Now handled easily, but caused great problems once*)
+ text "A tricky combination of when and split"
+ (*Now handled easily, but caused great problems once*)
schematic_goal [folded basic_defs]:
"?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
\<times> Eq(?A, ?b(inr(<i,j>)), j)"
-apply intr
-apply eqintr
-apply (rule PlusC_inl [THEN trans_elem])
-apply (rule_tac [4] comp_rls)
-apply (rule_tac [7] reduction_rls)
-apply (rule_tac [10] comp_rls)
-apply typechk
-done
+ apply intr
+ apply eqintr
+ apply (rule PlusC_inl [THEN trans_elem])
+ apply (rule_tac [4] comp_rls)
+ apply (rule_tac [7] reduction_rls)
+ apply (rule_tac [10] comp_rls)
+ apply typechk
+ done
(*similar but allows the type to depend on i and j*)
schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
\<times> Eq(?A(i,j), ?b(inr(<i,j>)), j)"
-oops
+ oops
(*similar but specifying the type N simplifies the unification problems*)
schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(N, ?b(inl(<i,j>)), i)
\<times> Eq(N, ?b(inr(<i,j>)), j)"
-oops
+ oops
-text "Deriving the addition operator"
+ text "Deriving the addition operator"
schematic_goal [folded arith_defs]:
"?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
\<times> (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
-apply intr
-apply eqintr
-apply (rule comp_rls)
-apply rew
-done
+ apply intr
+ apply eqintr
+ apply (rule comp_rls)
+ apply rew
+ done
text "The addition function -- using explicit lambdas"
schematic_goal [folded arith_defs]:
"?c : \<Sum>plus : ?A .
\<Prod>x:N. Eq(N, plus`0`x, x)
\<times> (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
-apply intr
-apply eqintr
-apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
-apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
-apply (rule_tac [3] p = "y" in NC_succ)
- (** by (resolve_tac @{context} comp_rls 3); caused excessive branching **)
-apply rew
-done
+ apply intr
+ apply eqintr
+ apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+ apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
+ apply (tactic "resolve_tac \<^context> [TSimp.split_eqn] 3")
+ apply (tactic "SELECT_GOAL (rew_tac \<^context> []) 4")
+ apply (rule_tac [3] p = "y" in NC_succ)
+ (** by (resolve_tac @{context} comp_rls 3); caused excessive branching **)
+ apply rew
+ done
end
--- a/src/CTT/ex/Typechecking.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/CTT/ex/Typechecking.thy Wed Oct 26 21:59:16 2022 +0200
@@ -12,77 +12,69 @@
subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
schematic_goal "?A type"
-apply (rule form_rls)
-done
+ by (rule form_rls)
schematic_goal "?A type"
-apply (rule form_rls)
-back
-apply (rule form_rls)
-apply (rule form_rls)
-done
+ apply (rule form_rls)
+ back
+ apply (rule form_rls)
+ apply (rule form_rls)
+ done
schematic_goal "\<Prod>z:?A . N + ?B(z) type"
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-apply (rule form_rls)
-done
+ apply (rule form_rls)
+ apply (rule form_rls)
+ apply (rule form_rls)
+ apply (rule form_rls)
+ apply (rule form_rls)
+ done
subsection \<open>Multi-step proofs: Type inference\<close>
lemma "\<Prod>w:N. N + N type"
-apply form
-done
+ by form
schematic_goal "<0, succ(0)> : ?A"
-apply intr
-done
+ apply intr done
schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
-apply typechk
-done
+ apply typechk done
schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
-apply typechk
-done
+ apply typechk done
text "typechecking an application of fst"
schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
-apply typechk
-done
+ apply typechk done
text "typechecking the predecessor function"
schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
-apply typechk
-done
+ apply typechk done
text "typechecking the addition function"
schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
-apply typechk
-done
+ apply typechk done
-(*Proofs involving arbitrary types.
- For concreteness, every type variable left over is forced to be N*)
+text \<open>Proofs involving arbitrary types.
+ For concreteness, every type variable left over is forced to be @{term N}\<close>
method_setup N =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
-apply typechk
-apply N
-done
+ apply typechk
+ apply N
+ done
schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
-apply typechk
-apply N
-done
+ apply typechk
+ apply N
+ done
text "typechecking fst (as a function object)"
schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
-apply typechk
-apply N
-done
+ apply typechk
+ apply N
+ done
end
--- a/src/HOL/Complex.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/HOL/Complex.thy Wed Oct 26 21:59:16 2022 +0200
@@ -143,14 +143,23 @@
subsection \<open>Numerals, Arithmetic, and Embedding from R\<close>
-abbreviation complex_of_real :: "real \<Rightarrow> complex"
- where "complex_of_real \<equiv> of_real"
-
declare [[coercion "of_real :: real \<Rightarrow> complex"]]
declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
declare [[coercion "of_int :: int \<Rightarrow> complex"]]
declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]
+abbreviation complex_of_nat::"nat \<Rightarrow> complex"
+ where "complex_of_nat \<equiv> of_nat"
+
+abbreviation complex_of_int::"int \<Rightarrow> complex"
+ where "complex_of_int \<equiv> of_int"
+
+abbreviation complex_of_rat::"rat \<Rightarrow> complex"
+ where "complex_of_rat \<equiv> of_rat"
+
+abbreviation complex_of_real :: "real \<Rightarrow> complex"
+ where "complex_of_real \<equiv> of_real"
+
lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
by (induct n) simp_all
@@ -1312,4 +1321,28 @@
lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
by (metis Reals_of_real complex_of_real_def)
+text \<open>Express a complex number as a linear combination of two others, not collinear with the origin\<close>
+lemma complex_axes:
+ assumes "Im (y/x) \<noteq> 0"
+ obtains a b where "z = of_real a * x + of_real b * y"
+proof -
+ define dd where "dd \<equiv> Re y * Im x - Im y * Re x"
+ define a where "a = (Im z * Re y - Re z * Im y) / dd"
+ define b where "b = (Re z * Im x - Im z * Re x) / dd"
+ have "dd \<noteq> 0"
+ using assms by (auto simp: dd_def Im_complex_div_eq_0)
+ have "a * Re x + b * Re y = Re z"
+ using \<open>dd \<noteq> 0\<close>
+ apply (simp add: a_def b_def field_simps)
+ by (metis dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
+ moreover have "a * Im x + b * Im y = Im z"
+ using \<open>dd \<noteq> 0\<close>
+ apply (simp add: a_def b_def field_simps)
+ by (metis (no_types) dd_def diff_add_cancel distrib_right mult.assoc mult.commute)
+ ultimately have "z = of_real a * x + of_real b * y"
+ by (simp add: complex_eqI)
+ then show ?thesis using that by simp
+qed
+
+
end
--- a/src/HOL/List.thy Wed Oct 26 16:26:23 2022 +0200
+++ b/src/HOL/List.thy Wed Oct 26 21:59:16 2022 +0200
@@ -1743,7 +1743,6 @@
lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
by(cases xs) simp_all
-
lemma list_eq_iff_nth_eq:
"(xs = ys) = (length xs = length ys \<and> (\<forall>i<length xs. xs!i = ys!i))"
proof (induct xs arbitrary: ys)
@@ -1751,11 +1750,14 @@
show ?case
proof (cases ys)
case (Cons y ys)
- then show ?thesis
- using Cons.hyps by fastforce
+ with Cons.hyps show ?thesis by fastforce
qed simp
qed force
+lemma map_equality_iff:
+ "map f xs = map g ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>i<length ys. f (xs!i) = g (ys!i))"
+ by (fastforce simp: list_eq_iff_nth_eq)
+
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
proof (induct xs)
case (Cons x xs)