[STATEMENT]
lemma ElemLambdaFun : "(\<And> x .Elem x u \<Longrightarrow> Elem (f x) U) \<Longrightarrow> Elem (Lambda u f) (Fun u U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. Elem x u \<Longrightarrow> Elem (f x) U) \<Longrightarrow> Elem (Lambda u f) (Fun u U)
[PROOF STEP]
apply (subst Elem_Lambda_Fun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. Elem x u \<Longrightarrow> Elem (f x) U) \<Longrightarrow> u = u \<and> (\<forall>x. Elem x u \<longrightarrow> Elem (f x) U)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma RangeRepl: "Range (Lambda A f) = Repl A f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.Range (Lambda A f) = Repl A f
[PROOF STEP]
apply (subst Ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. Elem z (HOLZF.Range (Lambda A f)) = Elem z (Repl A f)
[PROOF STEP]
apply (subst Range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (\<exists>x. Elem (Opair x z) (Lambda A f)) = Elem z (Repl A f)
[PROOF STEP]
apply (simp add: Repl Opair Lambda_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Universe) Utrans: "\<lbrakk>Elem a U ; Elem b a\<rbrakk> \<Longrightarrow> Elem b U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem a U; Elem b a\<rbrakk> \<Longrightarrow> Elem b U
[PROOF STEP]
apply (drule Usubset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem b a; HOLZF.subset a U\<rbrakk> \<Longrightarrow> Elem b U
[PROOF STEP]
apply (insert HOLZF.subset_def [of a U])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem b a; HOLZF.subset a U; HOLZF.subset a U \<equiv> \<forall>x. Elem x a \<longrightarrow> Elem x U\<rbrakk> \<Longrightarrow> Elem b U
[PROOF STEP]
apply (auto simp add: Usubset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ReplId: "Repl A id = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Repl A id = A
[PROOF STEP]
by (subst Ext, simp add: Repl)


[STATEMENT]
lemma (in Universe) UniverseSum : "Elem u U \<Longrightarrow> Elem (Sum u) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem u U \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (frule_tac u = "Lambda u id" in Uim)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Elem u U \<Longrightarrow> Elem (Lambda u id) (Fun u U)
 2. \<lbrakk>Elem u U; Elem (HOLZF.Sum (HOLZF.Range (Lambda u id))) U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (subst Elem_Lambda_Fun)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Elem u U \<Longrightarrow> u = u \<and> (\<forall>x. Elem x u \<longrightarrow> Elem (id x) U)
 2. \<lbrakk>Elem u U; Elem (HOLZF.Sum (HOLZF.Range (Lambda u id))) U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (frule Usubset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Elem u U; HOLZF.subset u U\<rbrakk> \<Longrightarrow> u = u \<and> (\<forall>x. Elem x u \<longrightarrow> Elem (id x) U)
 2. \<lbrakk>Elem u U; Elem (HOLZF.Sum (HOLZF.Range (Lambda u id))) U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (simp add: subset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem (HOLZF.Sum (HOLZF.Range (Lambda u id))) U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum u) U
[PROOF STEP]
apply (simp only: RangeRepl ReplId)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Universe) UniverseUnion:
  assumes "Elem u U" and "Elem v U"
  shows "Elem (union u v) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
let ?f = "(% x. if x = Empty then u else v)"
    and ?S = "(Power (Power Empty))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
have 1: "(Upair u v) = Range (Lambda ?S ?f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Upair u v = HOLZF.Range (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v))
[PROOF STEP]
by (subst RangeRepl, simp add: Upair_def)
[PROOF STATE]
proof (state)
this:
Upair u v = HOLZF.Range (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v))

goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
have 2: "\<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda ?S ?f) (Fun ?S U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)) (Fun (Power (Power Empty)) U)
[PROOF STEP]
by (rule ElemLambdaFun, simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)) (Fun (Power (Power Empty)) U)

goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Elem u U
Elem v U

goal (1 subgoal):
 1. Elem (HOLZF.union u v) U
[PROOF STEP]
apply (subst HOLZF.union_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (Upair u v)) U
[PROOF STEP]
apply (subst 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (HOLZF.Range (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)))) U
[PROOF STEP]
apply (rule_tac I="?S" in Uim)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Power (Power Empty)) U
 2. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)) (Fun (Power (Power Empty)) U)
[PROOF STEP]
apply (rule Upow)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem Empty U
 2. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)) (Fun (Power (Power Empty)) U)
[PROOF STEP]
apply (rule Uempty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda (Power (Power Empty)) (\<lambda>x. if x = Empty then u else v)) (Fun (Power (Power Empty)) U)
[PROOF STEP]
apply (rule 2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem u U
 2. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem v U
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Elem (HOLZF.union u v) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma UPairSingleton: "Upair u v = union (Singleton u) (Singleton v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Upair u v = HOLZF.union (Singleton u) (Singleton v)
[PROOF STEP]
apply (subst Ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. Elem z (Upair u v) = Elem z (HOLZF.union (Singleton u) (Singleton v))
[PROOF STEP]
apply (subst Upair)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (z = u \<or> z = v) = Elem z (HOLZF.union (Singleton u) (Singleton v))
[PROOF STEP]
apply (subst union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (z = u \<or> z = v) = (Elem z (Singleton u) \<or> Elem z (Singleton v))
[PROOF STEP]
apply (subst Singleton)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (z = u \<or> z = v) = (z = u \<or> z = v)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Universe) UniverseUPair: "\<lbrakk>Elem u U ; Elem v U\<rbrakk> \<Longrightarrow> Elem (Upair u v) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Upair u v) U
[PROOF STEP]
apply (subst UPairSingleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.union (Singleton u) (Singleton v)) U
[PROOF STEP]
apply (rule UniverseUnion)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Singleton u) U
 2. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Singleton v) U
[PROOF STEP]
apply (rule Usingle, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Universe) UniversePair: "\<lbrakk>Elem u U ; Elem v U\<rbrakk> \<Longrightarrow> Elem (Opair u v) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Opair u v) U
[PROOF STEP]
apply (subst Opair_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Upair (Upair u u) (Upair u v)) U
[PROOF STEP]
apply ((rule UniverseUPair)+, simp+)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Universe) "\<lbrakk>Elem u U ; Elem v U\<rbrakk> \<Longrightarrow> Elem (Sum (Repl u (%x . Singleton (Opair x v)))) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (Repl u (\<lambda>x. Singleton (Opair x v)))) U
[PROOF STEP]
apply (rule RangeRepl [THEN subst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (HOLZF.Range (Lambda u (\<lambda>x. Singleton (Opair x v))))) U
[PROOF STEP]
apply (rule Uim [of u], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda u (\<lambda>x. Singleton (Opair x v))) (Fun u U)
[PROOF STEP]
apply (rule ElemLambdaFun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Singleton (Opair x v)) U
[PROOF STEP]
apply (rule Usingle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Opair x v) U
[PROOF STEP]
apply (rule UniversePair)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem x U
 2. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem v U
[PROOF STEP]
apply (rule Utrans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (?a13 x) U
 2. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem x (?a13 x)
 3. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem v U
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SumRepl: "Sum (Repl A (Singleton o f)) = Repl A f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.Sum (Repl A (Singleton \<circ> f)) = Repl A f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HOLZF.Sum (Repl A (Singleton \<circ> f)) = Repl A f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.Sum (Repl A (Singleton \<circ> f)) = Repl A f
[PROOF STEP]
apply (subst Ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. Elem z (HOLZF.Sum (Repl A (Singleton \<circ> f))) = Elem z (Repl A f)
[PROOF STEP]
apply (subst Sum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (\<exists>y. Elem z y \<and> Elem y (Repl A (Singleton \<circ> f))) = Elem z (Repl A f)
[PROOF STEP]
apply (subst Repl)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. (\<exists>y. Elem z y \<and> (\<exists>a. Elem a A \<and> y = (Singleton \<circ> f) a)) = (\<exists>a. Elem a A \<and> z = f a)
[PROOF STEP]
apply (auto simp add: Singleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))
[PROOF STEP]
show "Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))
[PROOF STEP]
apply (rule exI [of _ "Singleton (f a)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem a A \<Longrightarrow> Elem (f a) (Singleton (f a)) \<and> (\<exists>aa. Elem aa A \<and> Singleton (f a) = Singleton (f aa))
[PROOF STEP]
apply (subst Singleton, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem a A \<Longrightarrow> \<exists>aa. Elem aa A \<and> Singleton (f a) = Singleton (f aa)
[PROOF STEP]
apply (rule exI [of _ "a"], simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Elem a A \<Longrightarrow> \<exists>y. Elem (f a) y \<and> (\<exists>a. Elem a A \<and> y = Singleton (f a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HOLZF.Sum (Repl A (Singleton \<circ> f)) = Repl A f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Universe) UniverseProd:
  assumes "Elem u U" and "Elem v U"
  shows   "Elem (CartProd u v) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem (CartProd u v) U
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Elem (CartProd u v) U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem (CartProd u v) U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Elem u U
Elem v U

goal (1 subgoal):
 1. Elem (CartProd u v) U
[PROOF STEP]
apply (subst CartProd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (Repl u (\<lambda>a. Repl v (Opair a)))) U
[PROOF STEP]
apply (rule RangeRepl [of u "% x . (Repl v (Opair x))", THEN subst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (HOLZF.Range (Lambda u (\<lambda>x. Repl v (Opair x))))) U
[PROOF STEP]
apply (rule Uim [of u], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U\<rbrakk> \<Longrightarrow> Elem (Lambda u (\<lambda>x. Repl v (Opair x))) (Fun u U)
[PROOF STEP]
apply (rule ElemLambdaFun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U
[PROOF STEP]
show "\<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U
[PROOF STEP]
apply (drule Utrans [of u x], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem x u; Elem x U\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U
[PROOF STEP]
apply (rule SumRepl [THEN subst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem x u; Elem x U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (Repl v (Singleton \<circ> Opair x))) U
[PROOF STEP]
apply (rule RangeRepl [THEN subst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem x u; Elem x U\<rbrakk> \<Longrightarrow> Elem (HOLZF.Sum (HOLZF.Range (Lambda v (Singleton \<circ> Opair x)))) U
[PROOF STEP]
apply (rule Uim [of v], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem x u; Elem x U\<rbrakk> \<Longrightarrow> Elem (Lambda v (Singleton \<circ> Opair x)) (Fun v U)
[PROOF STEP]
apply (rule ElemLambdaFun,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem (Singleton (Opair x xa)) U
[PROOF STEP]
apply (rule Usingle)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem (Opair x xa) U
[PROOF STEP]
apply (rule UniversePair)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem x U
 2. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U
[PROOF STEP]
apply (drule Usubset, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U
[PROOF STEP]
show "\<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U
[PROOF STEP]
by (rule Utrans, simp+)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Elem v U; Elem x u; Elem x U; Elem xa v\<rbrakk> \<Longrightarrow> Elem xa U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Elem u U; Elem v U; Elem x u\<rbrakk> \<Longrightarrow> Elem (Repl v (Opair x)) U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Elem (CartProd u v) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Universe) UniverseSubset: "\<lbrakk>subset u v ; Elem v U\<rbrakk> \<Longrightarrow> Elem u U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HOLZF.subset u v; Elem v U\<rbrakk> \<Longrightarrow> Elem u U
[PROOF STEP]
apply (drule_tac HOLZF.Power [of u v, THEN ssubst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem v U; Elem u (Power v)\<rbrakk> \<Longrightarrow> Elem u U
[PROOF STEP]
apply (drule Upow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Elem u (Power v); Elem (Power v) U\<rbrakk> \<Longrightarrow> Elem u U
[PROOF STEP]
apply (rule Utrans, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SepSubset: "subset (Sep A p) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Sep A p) A
[PROOF STEP]
apply (subst subset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. Elem x (Sep A p) \<longrightarrow> Elem x A
[PROOF STEP]
apply (subst Sep, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SubsetSmall:
  assumes "subset A' A" and "subset A B" shows "subset A' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset A' B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HOLZF.subset A' B
[PROOF STEP]
have "(subset A' A \<and> subset A B) \<longrightarrow> subset A' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset A' A \<and> HOLZF.subset A B \<longrightarrow> HOLZF.subset A' B
[PROOF STEP]
by ((subst subset_def)+, simp+)
[PROOF STATE]
proof (state)
this:
HOLZF.subset A' A \<and> HOLZF.subset A B \<longrightarrow> HOLZF.subset A' B

goal (1 subgoal):
 1. HOLZF.subset A' B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
HOLZF.subset A' A \<and> HOLZF.subset A B \<longrightarrow> HOLZF.subset A' B

goal (1 subgoal):
 1. HOLZF.subset A' B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
HOLZF.subset A' A \<and> HOLZF.subset A B \<longrightarrow> HOLZF.subset A' B
HOLZF.subset A' A
HOLZF.subset A B

goal (1 subgoal):
 1. HOLZF.subset A' B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HOLZF.subset A' B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SubsetTrans:
  assumes "(subset a b)" and "(subset b c)"
  shows "(subset a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset a c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HOLZF.subset a c
[PROOF STEP]
have "(subset a b) \<and> (subset b c) \<longrightarrow> (subset a c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset a b \<and> HOLZF.subset b c \<longrightarrow> HOLZF.subset a c
[PROOF STEP]
by ((subst subset_def)+, simp)
[PROOF STATE]
proof (state)
this:
HOLZF.subset a b \<and> HOLZF.subset b c \<longrightarrow> HOLZF.subset a c

goal (1 subgoal):
 1. HOLZF.subset a c
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
HOLZF.subset a b \<and> HOLZF.subset b c \<longrightarrow> HOLZF.subset a c

goal (1 subgoal):
 1. HOLZF.subset a c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
HOLZF.subset a b \<and> HOLZF.subset b c \<longrightarrow> HOLZF.subset a c
HOLZF.subset a b
HOLZF.subset b c

goal (1 subgoal):
 1. HOLZF.subset a c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HOLZF.subset a c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SubsetSepTrans: "subset A B \<Longrightarrow> subset (Sep A p) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset A B \<Longrightarrow> HOLZF.subset (Sep A p) B
[PROOF STEP]
apply (rule SubsetSmall [of "Sep A p" A B])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. HOLZF.subset A B \<Longrightarrow> HOLZF.subset (Sep A p) A
 2. HOLZF.subset A B \<Longrightarrow> HOLZF.subset A B
[PROOF STEP]
apply (rule SepSubset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset A B \<Longrightarrow> HOLZF.subset A B
[PROOF STEP]
by simp


[STATEMENT]
lemma ProductSubset: "subset (Product u) (Power (CartProd u (Sum u)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Product u) (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
apply (subst Product_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Sep (Fun u (HOLZF.Sum u)) (\<lambda>f. \<forall>ua. Elem ua u \<longrightarrow> Elem (f \<acute> ua) ua)) (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
apply (subst Fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Sep (Sep (PFun u (HOLZF.Sum u)) (\<lambda>f. HOLZF.Domain f = u)) (\<lambda>f. \<forall>ua. Elem ua u \<longrightarrow> Elem (f \<acute> ua) ua)) (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
apply (subst PFun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Sep (Sep (Sep (Power (CartProd u (HOLZF.Sum u))) isFun) (\<lambda>f. HOLZF.Domain f = u)) (\<lambda>f. \<forall>ua. Elem ua u \<longrightarrow> Elem (f \<acute> ua) ua)) (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
apply (rule SubsetSepTrans)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOLZF.subset (Power (CartProd u (HOLZF.Sum u))) (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
apply (subst subset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. Elem x (Power (CartProd u (HOLZF.Sum u))) \<longrightarrow> Elem x (Power (CartProd u (HOLZF.Sum u)))
[PROOF STEP]
by simp


[STATEMENT]
lemma ZFImageRangeExplode: "x \<in> range explode \<Longrightarrow> f ` x \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> range explode \<Longrightarrow> f ` x \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> range explode \<Longrightarrow> f ` x \<in> range explode
[PROOF STEP]
assume "x \<in> range explode"
[PROOF STATE]
proof (state)
this:
x \<in> range explode

goal (1 subgoal):
 1. x \<in> range explode \<Longrightarrow> f ` x \<in> range explode
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> range explode
[PROOF STEP]
obtain y where "x = explode y"
[PROOF STATE]
proof (prove)
using this:
x \<in> range explode

goal (1 subgoal):
 1. (\<And>y. x = explode y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using range_ex1_eq
[PROOF STATE]
proof (prove)
using this:
x \<in> range explode
inj ?f \<Longrightarrow> (?b \<in> range ?f) = (\<exists>!x. ?b = ?f x)

goal (1 subgoal):
 1. (\<And>y. x = explode y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = explode y

goal (1 subgoal):
 1. x \<in> range explode \<Longrightarrow> f ` x \<in> range explode
[PROOF STEP]
hence "f ` x = explode (Repl y f)"
[PROOF STATE]
proof (prove)
using this:
x = explode y

goal (1 subgoal):
 1. f ` x = explode (Repl y f)
[PROOF STEP]
using explode_Repl_eq
[PROOF STATE]
proof (prove)
using this:
x = explode y
explode (Repl ?A ?f) = ?f ` explode ?A

goal (1 subgoal):
 1. f ` x = explode (Repl y f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` x = explode (Repl y f)

goal (1 subgoal):
 1. x \<in> range explode \<Longrightarrow> f ` x \<in> range explode
[PROOF STEP]
thus "f ` x \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
f ` x = explode (Repl y f)

goal (1 subgoal):
 1. f ` x \<in> range explode
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` x \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subsetFn: "\<lbrakk>Y \<noteq> {} ; Y \<subseteq> X \<rbrakk> \<Longrightarrow> (subsetFn X Y) ` X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Y \<noteq> {}; Y \<subseteq> X\<rbrakk> \<Longrightarrow> subsetFn X Y ` X = Y
[PROOF STEP]
proof(auto simp add: subsetFn_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xb. \<lbrakk>Y \<subseteq> X; x \<in> Y; xb \<in> X; xb \<notin> Y\<rbrakk> \<Longrightarrow> (SOME y. y \<in> Y) \<in> Y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xb. \<lbrakk>Y \<subseteq> X; x \<in> Y; xb \<in> X; xb \<notin> Y\<rbrakk> \<Longrightarrow> (SOME y. y \<in> Y) \<in> Y
[PROOF STEP]
assume "x \<in> Y"
[PROOF STATE]
proof (state)
this:
x \<in> Y

goal (1 subgoal):
 1. \<And>x xb. \<lbrakk>Y \<subseteq> X; x \<in> Y; xb \<in> X; xb \<notin> Y\<rbrakk> \<Longrightarrow> (SOME y. y \<in> Y) \<in> Y
[PROOF STEP]
thus "(SOME y. y \<in> Y) \<in> Y"
[PROOF STATE]
proof (prove)
using this:
x \<in> Y

goal (1 subgoal):
 1. (SOME y. y \<in> Y) \<in> Y
[PROOF STEP]
using someI_ex[of "\<lambda> x . x \<in> Y"]
[PROOF STATE]
proof (prove)
using this:
x \<in> Y
\<exists>x. x \<in> Y \<Longrightarrow> (SOME x. x \<in> Y) \<in> Y

goal (1 subgoal):
 1. (SOME y. y \<in> Y) \<in> Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SOME y. y \<in> Y) \<in> Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFSubsetRangeExplode: "\<lbrakk>X \<in> range explode ; Y \<subseteq> X\<rbrakk> \<Longrightarrow> Y \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> range explode; Y \<subseteq> X\<rbrakk> \<Longrightarrow> Y \<in> range explode
[PROOF STEP]
proof(cases "Y = {}", simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>X \<in> range explode; Y = {}\<rbrakk> \<Longrightarrow> {} \<in> range explode
 2. \<lbrakk>X \<in> range explode; Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> Y \<in> range explode
[PROOF STEP]
have "explode Empty = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. explode Empty = {}
[PROOF STEP]
using explode_Empty
[PROOF STATE]
proof (prove)
using this:
(explode ?x = {}) = (?x = Empty)

goal (1 subgoal):
 1. explode Empty = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
explode Empty = {}

goal (2 subgoals):
 1. \<lbrakk>X \<in> range explode; Y = {}\<rbrakk> \<Longrightarrow> {} \<in> range explode
 2. \<lbrakk>X \<in> range explode; Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> Y \<in> range explode
[PROOF STEP]
thus "{} \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
explode Empty = {}

goal (1 subgoal):
 1. {} \<in> range explode
[PROOF STEP]
by (auto simp add: explode_def)
[PROOF STATE]
proof (state)
this:
{} \<in> range explode

goal (1 subgoal):
 1. \<lbrakk>X \<in> range explode; Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> Y \<in> range explode
[PROOF STEP]
assume "Y \<noteq> {}" and "Y \<subseteq> X" and "X \<in> range explode"
[PROOF STATE]
proof (state)
this:
Y \<noteq> {}
Y \<subseteq> X
X \<in> range explode

goal (1 subgoal):
 1. \<lbrakk>X \<in> range explode; Y \<subseteq> X; Y \<noteq> {}\<rbrakk> \<Longrightarrow> Y \<in> range explode
[PROOF STEP]
thus "Y \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
Y \<noteq> {}
Y \<subseteq> X
X \<in> range explode

goal (1 subgoal):
 1. Y \<in> range explode
[PROOF STEP]
using ZFImageRangeExplode[of X "subsetFn X Y"] subsetFn[of Y X]
[PROOF STATE]
proof (prove)
using this:
Y \<noteq> {}
Y \<subseteq> X
X \<in> range explode
X \<in> range explode \<Longrightarrow> subsetFn X Y ` X \<in> range explode
\<lbrakk>Y \<noteq> {}; Y \<subseteq> X\<rbrakk> \<Longrightarrow> subsetFn X Y ` X = Y

goal (1 subgoal):
 1. Y \<in> range explode
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Y \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFUnionRangeExplode:
  assumes "\<And> x . x \<in> A \<Longrightarrow> f x \<in> range explode" and "A \<in> range explode"
  shows "(\<Union> x \<in> A . f x) \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (f ` A) \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (f ` A) \<in> range explode
[PROOF STEP]
let ?S = "Sep (Sum (Repl (implode A) (implode o f))) (\<lambda> y . \<exists> x  . (Elem x (implode A)) \<and> (Elem y (implode (f x))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (f ` A) \<in> range explode
[PROOF STEP]
have "explode ?S = (\<Union> x \<in> A . f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. explode (Sep (HOLZF.Sum (Repl (implode A) (implode \<circ> f))) (\<lambda>y. \<exists>x. Elem x (implode A) \<and> Elem y (implode (f x)))) = \<Union> (f ` A)
[PROOF STEP]
proof (auto simp add: UNION_eq explode_def Sep Sum Repl assms Elem_implode cong del: image_cong_simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> A; x \<in> f xa\<rbrakk> \<Longrightarrow> \<exists>y. Elem x y \<and> (\<exists>a. a \<in> A \<and> y = implode (f a))
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> A; x \<in> f xa\<rbrakk> \<Longrightarrow> \<exists>y. Elem x y \<and> (\<exists>a. a \<in> A \<and> y = implode (f a))
[PROOF STEP]
assume a: "y \<in> A" and b: "x \<in> f y"
[PROOF STATE]
proof (state)
this:
y \<in> A
x \<in> f y

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> A; x \<in> f xa\<rbrakk> \<Longrightarrow> \<exists>y. Elem x y \<and> (\<exists>a. a \<in> A \<and> y = implode (f a))
[PROOF STEP]
show "\<exists>z. Elem x z \<and> (\<exists>a. a \<in> A \<and> z = implode (f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. Elem x z \<and> (\<exists>a. a \<in> A \<and> z = implode (f a))
[PROOF STEP]
apply (rule exI [where ?x = "implode (f y)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem x (implode (f y)) \<and> (\<exists>a. a \<in> A \<and> implode (f y) = implode (f a))
[PROOF STEP]
apply (auto simp add: explode_def Sep Sum Repl assms Elem_implode a b cong del: image_cong_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. a \<in> A \<and> implode (f y) = implode (f a)
[PROOF STEP]
apply (rule exI [where ?x = y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> A \<and> implode (f y) = implode (f y)
[PROOF STEP]
apply (simp add: a)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>z. Elem x z \<and> (\<exists>a. a \<in> A \<and> z = implode (f a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
explode (Sep (HOLZF.Sum (Repl (implode A) (implode \<circ> f))) (\<lambda>y. \<exists>x. Elem x (implode A) \<and> Elem y (implode (f x)))) = \<Union> (f ` A)

goal (1 subgoal):
 1. \<Union> (f ` A) \<in> range explode
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
explode (Sep (HOLZF.Sum (Repl (implode A) (implode \<circ> f))) (\<lambda>y. \<exists>x. Elem x (implode A) \<and> Elem y (implode (f x)))) = \<Union> (f ` A)

goal (1 subgoal):
 1. \<Union> (f ` A) \<in> range explode
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (f ` A) \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFUnionNatInRangeExplode: "(\<And> (n :: nat) . f n \<in> range explode) \<Longrightarrow> (\<Union> n . f n) \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
assume a: "(\<And> (n :: nat) . f n \<in> range explode)"
[PROOF STATE]
proof (state)
this:
f ?n \<in> range explode

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
have "explode Nat \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. explode HOLZF.Nat \<in> range explode
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
explode HOLZF.Nat \<in> range explode

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
explode HOLZF.Nat \<in> range explode

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
have "\<And> n . n \<in> (explode Nat) \<Longrightarrow> (f o Nat2nat) n \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) n \<in> range explode
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> range explode

goal (1 subgoal):
 1. \<And>n. n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) n \<in> range explode
[PROOF STEP]
by(auto simp add: explode_def)
[PROOF STATE]
proof (state)
this:
?n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) ?n \<in> range explode

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) ?n \<in> range explode

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
have "(\<Union> n . f n) = (\<Union> n \<in> (explode Nat) . (f o Nat2nat) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range f) = \<Union> ((f \<circ> Nat2nat) ` explode HOLZF.Nat)
[PROOF STEP]
proof(auto simp add: Nat2nat_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n. x \<in> f n \<Longrightarrow> \<exists>xa\<in>explode HOLZF.Nat. x \<in> f (inv nat2Nat xa)
[PROOF STEP]
fix x n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n. x \<in> f n \<Longrightarrow> \<exists>xa\<in>explode HOLZF.Nat. x \<in> f (inv nat2Nat xa)
[PROOF STEP]
assume aa: "x \<in> f n"
[PROOF STATE]
proof (state)
this:
x \<in> f n

goal (1 subgoal):
 1. \<And>x n. x \<in> f n \<Longrightarrow> \<exists>xa\<in>explode HOLZF.Nat. x \<in> f (inv nat2Nat xa)
[PROOF STEP]
show "\<exists> n \<in> (explode Nat) . x \<in> f (inv nat2Nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n\<in>explode HOLZF.Nat. x \<in> f (inv nat2Nat n)
[PROOF STEP]
apply(rule bexI[where ?x = "nat2Nat n"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> f (inv nat2Nat (nat2Nat n))
 2. nat2Nat n \<in> explode HOLZF.Nat
[PROOF STEP]
by(auto simp add: aa inj_nat2Nat explode_Elem)
[PROOF STATE]
proof (state)
this:
\<exists>n\<in>explode HOLZF.Nat. x \<in> f (inv nat2Nat n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (range f) = \<Union> ((f \<circ> Nat2nat) ` explode HOLZF.Nat)

goal (1 subgoal):
 1. (\<And>n. f n \<in> range explode) \<Longrightarrow> \<Union> (range f) \<in> range explode
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
explode HOLZF.Nat \<in> range explode
?n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) ?n \<in> range explode
\<Union> (range f) = \<Union> ((f \<circ> Nat2nat) ` explode HOLZF.Nat)
[PROOF STEP]
show "(\<Union> n . f n) \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
explode HOLZF.Nat \<in> range explode
?n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) ?n \<in> range explode
\<Union> (range f) = \<Union> ((f \<circ> Nat2nat) ` explode HOLZF.Nat)

goal (1 subgoal):
 1. \<Union> (range f) \<in> range explode
[PROOF STEP]
using ZFUnionRangeExplode
[PROOF STATE]
proof (prove)
using this:
explode HOLZF.Nat \<in> range explode
?n \<in> explode HOLZF.Nat \<Longrightarrow> (f \<circ> Nat2nat) ?n \<in> range explode
\<Union> (range f) = \<Union> ((f \<circ> Nat2nat) ` explode HOLZF.Nat)
\<lbrakk>\<And>x. x \<in> ?A \<Longrightarrow> ?f x \<in> range explode; ?A \<in> range explode\<rbrakk> \<Longrightarrow> \<Union> (?f ` ?A) \<in> range explode

goal (1 subgoal):
 1. \<Union> (range f) \<in> range explode
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (range f) \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFProdFnInRangeExplode: "\<lbrakk>A \<in> range explode ; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
assume a: "A \<in> range explode" and b: "B \<in> range explode"
[PROOF STATE]
proof (state)
this:
A \<in> range explode
B \<in> range explode

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
let ?X = "(explode (CartProd (implode A) (implode B)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
have "f ` (A \<times> B) = (f  o (\<lambda> z . (Fst z, Snd z))) ` ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))
[PROOF STEP]
proof(auto simp add: explode_def CartProd image_def Fst Snd)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>xa \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (xa, y) = f (Fst x, Snd x)
 2. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>xa \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (xa, y) = f (Fst x, Snd x)
 2. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
fix z y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>xa \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (xa, y) = f (Fst x, Snd x)
 2. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
assume z: "z \<in> A" and y: "y \<in> B"
[PROOF STATE]
proof (state)
this:
z \<in> A
y \<in> B

goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>xa \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (xa, y) = f (Fst x, Snd x)
 2. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
show "\<exists>x. (\<exists>a. Elem a (implode A) \<and>
        (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (z, y) = f (Fst x, Snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (z, y) = f (Fst x, Snd x)
[PROOF STEP]
apply(insert z y a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<in> A; y \<in> B; A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (z, y) = f (Fst x, Snd x)
[PROOF STEP]
apply(rule exI[where ?x = "Opair z y"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<in> A; y \<in> B; A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> Opair z y = Opair a b)) \<and> f (z, y) = f (Fst (Opair z y), Snd (Opair z y))
[PROOF STEP]
apply(auto simp add: Opair explode_Elem Fst Snd)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (z, y) = f (Fst x, Snd x)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z2 \<in> A; ?y2 \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (?z2, ?y2) = f (Fst x, Snd x)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z2 \<in> A; ?y2 \<in> B\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>a. Elem a (implode A) \<and> (\<exists>b. Elem b (implode B) \<and> x = Opair a b)) \<and> f (?z2, ?y2) = f (Fst x, Snd x)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
assume aa: "Elem a (implode A)" and bb: "Elem b (implode B)"
[PROOF STATE]
proof (state)
this:
Elem a (implode A)
Elem b (implode B)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>Elem a (implode A); Elem b (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
show "\<exists> x \<in> A . \<exists> y \<in> B . f (a,b) = f (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)
[PROOF STEP]
by(rule bexI[where ?x = a], rule bexI[where ?x = b], simp, insert a b aa bb, auto simp add: explode_Elem)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>A. \<exists>y\<in>B. f (a, b) = f (x, y)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Elem ?a2 (implode A); Elem ?b2 (implode B)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<exists>y\<in>B. f (?a2, ?b2) = f (x, y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
have "?X \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. explode (CartProd (implode A) (implode B)) \<in> range explode
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
explode (CartProd (implode A) (implode B)) \<in> range explode

goal (1 subgoal):
 1. \<lbrakk>A \<in> range explode; B \<in> range explode\<rbrakk> \<Longrightarrow> f ` (A \<times> B) \<in> range explode
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))
explode (CartProd (implode A) (implode B)) \<in> range explode
[PROOF STEP]
show "f ` (A \<times> B) \<in> range explode"
[PROOF STATE]
proof (prove)
using this:
f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))
explode (CartProd (implode A) (implode B)) \<in> range explode

goal (1 subgoal):
 1. f ` (A \<times> B) \<in> range explode
[PROOF STEP]
using ZFImageRangeExplode
[PROOF STATE]
proof (prove)
using this:
f ` (A \<times> B) = (f \<circ> (\<lambda>z. (Fst z, Snd z))) ` explode (CartProd (implode A) (implode B))
explode (CartProd (implode A) (implode B)) \<in> range explode
?x \<in> range explode \<Longrightarrow> ?f ` ?x \<in> range explode

goal (1 subgoal):
 1. f ` (A \<times> B) \<in> range explode
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` (A \<times> B) \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SingletonInRangeExplode: "{x} \<in> range explode"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} \<in> range explode
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {x} \<in> range explode
[PROOF STEP]
have "explode (Singleton x) = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. explode (Singleton x) = {x}
[PROOF STEP]
by(auto simp add: explode_def Singleton)
[PROOF STATE]
proof (state)
this:
explode (Singleton x) = {x}

goal (1 subgoal):
 1. {x} \<in> range explode
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
explode (Singleton x) = {x}

goal (1 subgoal):
 1. {x} \<in> range explode
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x} \<in> range explode

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFTFst: "ZFTFst (ZFTriple a b c) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFTFst (ZFTriple a b c) = a
[PROOF STEP]
by(auto simp add: ZFTriple_def ZFTFst_def Fst)


[STATEMENT]
lemma ZFTSnd: "ZFTSnd (ZFTriple a b c) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFTSnd (ZFTriple a b c) = b
[PROOF STEP]
by(auto simp add: ZFTriple_def ZFTSnd_def Snd Fst)


[STATEMENT]
lemma ZFTThd: "ZFTThd (ZFTriple a b c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFTThd (ZFTriple a b c) = c
[PROOF STEP]
by(auto simp add: ZFTriple_def ZFTThd_def Snd Fst)


[STATEMENT]
lemma ZFTriple: "ZFTriple a b c = ZFTriple a' b' c' \<Longrightarrow> (a = a' \<and> b = b' \<and> c = c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFTriple a b c = ZFTriple a' b' c' \<Longrightarrow> a = a' \<and> b = b' \<and> c = c'
[PROOF STEP]
by(auto simp add: ZFTriple_def Opair)


[STATEMENT]
lemma ZFSucZero: "Nat2nat (SucNat Empty) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
have "nat2Nat 0 = Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat2Nat 0 = Empty
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat2Nat 0 = Empty

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
hence "(SucNat Empty) = nat2Nat (Suc 0)"
[PROOF STATE]
proof (prove)
using this:
nat2Nat 0 = Empty

goal (1 subgoal):
 1. SucNat Empty = nat2Nat (Suc 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
SucNat Empty = nat2Nat (Suc 0)

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
hence "Nat2nat (SucNat Empty) = Nat2nat (nat2Nat (Suc 0))"
[PROOF STATE]
proof (prove)
using this:
SucNat Empty = nat2Nat (Suc 0)

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = Nat2nat (nat2Nat (Suc 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Nat2nat (SucNat Empty) = Nat2nat (nat2Nat (Suc 0))

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Nat2nat (SucNat Empty) = Nat2nat (nat2Nat (Suc 0))

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
have "... = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nat2nat (nat2Nat (Suc 0)) = Suc 0
[PROOF STEP]
using Nat2nat_nat2Nat[of "Suc 0"]
[PROOF STATE]
proof (prove)
using this:
Nat2nat (nat2Nat (Suc 0)) = Suc 0

goal (1 subgoal):
 1. Nat2nat (nat2Nat (Suc 0)) = Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Nat2nat (nat2Nat (Suc 0)) = Suc 0

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Nat2nat (SucNat Empty) = Suc 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Nat2nat (SucNat Empty) = Suc 0

goal (1 subgoal):
 1. Nat2nat (SucNat Empty) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Nat2nat (SucNat Empty) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFZero: "Nat2nat Empty = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
have "nat2Nat 0 = Empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat2Nat 0 = Empty
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat2Nat 0 = Empty

goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
hence "Nat2nat Empty = Nat2nat (nat2Nat 0)"
[PROOF STATE]
proof (prove)
using this:
nat2Nat 0 = Empty

goal (1 subgoal):
 1. Nat2nat Empty = Nat2nat (nat2Nat 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Nat2nat Empty = Nat2nat (nat2Nat 0)

goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Nat2nat Empty = Nat2nat (nat2Nat 0)

goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
using Nat2nat_nat2Nat[of "0"]
[PROOF STATE]
proof (prove)
using this:
Nat2nat Empty = Nat2nat (nat2Nat 0)
Nat2nat (nat2Nat 0) = 0

goal (1 subgoal):
 1. Nat2nat Empty = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Nat2nat Empty = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZFSucNeq0: "Elem x Nat \<Longrightarrow> Nat2nat (SucNat x) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Elem x HOLZF.Nat \<Longrightarrow> Nat2nat (SucNat x) \<noteq> 0
[PROOF STEP]
by(auto simp add: Nat2nat_SucNat)


[STATEMENT]
lemma is_lub_set:
  "S <<| \<Union>S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S <<| \<Union> S
[PROOF STEP]
by(auto simp add: is_lub_def below_set_def is_ub_def)


[STATEMENT]
lemma lub_set: "lub S = \<Union>S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lub S = \<Union> S
[PROOF STEP]
by (metis is_lub_set lub_eqI)


[STATEMENT]
lemma minimal_set: "{} \<sqsubseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<sqsubseteq> S
[PROOF STEP]
unfolding below_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> S
[PROOF STEP]
by simp


[STATEMENT]
lemma set_contI:
  assumes  "\<And> Y. chain Y \<Longrightarrow> f (\<Squnion> i. Y i) = \<Union> (f ` range Y)"
  shows "cont f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont f
[PROOF STEP]
proof(rule contI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
fix Y :: "nat \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
assume "chain Y"
[PROOF STATE]
proof (state)
this:
chain Y

goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
hence "f (\<Squnion> i. Y i) = \<Union> (f ` range Y)"
[PROOF STATE]
proof (prove)
using this:
chain Y

goal (1 subgoal):
 1. f (\<Squnion>i. Y i) = \<Union> (f ` range Y)
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
f (\<Squnion>i. Y i) = \<Union> (f ` range Y)

goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (\<Squnion>i. Y i) = \<Union> (f ` range Y)

goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
have "\<dots> = \<Union> (range (\<lambda>i. f (Y i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (f ` range Y) = (\<Union>i. f (Y i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (f ` range Y) = (\<Union>i. f (Y i))

goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (\<Squnion>i. Y i) = (\<Union>i. f (Y i))
[PROOF STEP]
show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion> i. Y i)"
[PROOF STATE]
proof (prove)
using this:
f (\<Squnion>i. Y i) = (\<Union>i. f (Y i))

goal (1 subgoal):
 1. range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
using is_lub_set
[PROOF STATE]
proof (prove)
using this:
f (\<Squnion>i. Y i) = (\<Union>i. f (Y i))
?S <<| \<Union> ?S

goal (1 subgoal):
 1. range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_set_contI:
  assumes  "\<And> S. f (\<Union>S) = \<Union> (f ` S)"
  shows "cont f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont f
[PROOF STEP]
by (metis set_contI assms is_lub_set  lub_eqI)


[STATEMENT]
lemma adm_subseteq[simp]:
  assumes "cont f"
  shows "adm (\<lambda>a. f a \<subseteq> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>a. f a \<subseteq> S)
[PROOF STEP]
by (rule admI)(auto simp add: cont2contlubE[OF assms] lub_set)


[STATEMENT]
lemma adm_Ball[simp]: "adm (\<lambda>S. \<forall>x\<in>S. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>S. \<forall>x\<in>S. P x)
[PROOF STEP]
by (auto intro!: admI  simp add: lub_set)


[STATEMENT]
lemma diff_cont[THEN cont_compose, simp, cont2cont]:
  fixes S' :: "'a set"
  shows  "cont (\<lambda>S. S - S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>S. S - S')
[PROOF STEP]
by (rule set_set_contI) simp


[STATEMENT]
lemma HMA_diagonal_step[transfer_rule]:
  "((Mod_Type_Connect.HMA_M :: _ \<Rightarrow> 'a :: comm_ring_1 ^ 'nc :: mod_type ^ 'nr :: mod_type \<Rightarrow> _)
    ===> (=) ===> (=) ===> Mod_Type_Connect.HMA_M)
    (\<lambda>A. diagonal_step_JNF A i j) (\<lambda>B. diagonal_step B i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mod_Type_Connect.HMA_M ===> (=) ===> (=) ===> Mod_Type_Connect.HMA_M) (\<lambda>A. diagonal_step_JNF A i j) (\<lambda>B. diagonal_step B i j)
[PROOF STEP]
by (intro rel_funI, goal_cases, auto simp add: Mod_Type_Connect.HMA_M_def
      diagonal_step_JNF_def diagonal_step_def)
 (rule eq_matI, auto simp add: Mod_Type_Connect.from_hma\<^sub>m_def, insert from_nat_eq_imp_eq i j, auto)


[STATEMENT]
lemma HMA_diagonal_step_PQ[transfer_rule]:
  "((Mod_Type_Connect.HMA_M :: _ \<Rightarrow> 'a :: bezout_ring ^ 'nc :: mod_type ^ 'nr :: mod_type \<Rightarrow> _)
    ===> (=) ===> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M)
    (\<lambda>A bezout. diagonal_step_PQ_JNF A i k bezout) (\<lambda>A bezout. diagonal_step_PQ A i k bezout)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mod_Type_Connect.HMA_M ===> (=) ===> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M) (\<lambda>A. diagonal_step_PQ_JNF A i k) (\<lambda>A. diagonal_step_PQ A i k)
[PROOF STEP]
proof (intro rel_funI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
case (1 A A' bezout bezout')
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A A'
bezout = bezout'

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
note HMA_M_AA'[transfer_rule] = 1(1)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
let ?d_JNF = "(diagonal_step_PQ_JNF A i k bezout)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
let ?d_HA = "(diagonal_step_PQ A' i k bezout)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_I k (from_nat k::'nc)"
    and [transfer_rule]: "Mod_Type_Connect.HMA_I k (from_nat k::'nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_I k (from_nat k) &&& Mod_Type_Connect.HMA_I k (from_nat k)
[PROOF STEP]
by (metis Mod_Type_Connect.HMA_I_def k min.strict_boundedE to_nat_from_nat_id)+
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_I k (from_nat k)
Mod_Type_Connect.HMA_I k (from_nat k)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_I i (from_nat i::'nc)"
    and [transfer_rule]: "Mod_Type_Connect.HMA_I i (from_nat i::'nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_I i (from_nat i) &&& Mod_Type_Connect.HMA_I i (from_nat i)
[PROOF STEP]
by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE to_nat_from_nat_id)+
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_I i (from_nat i)
Mod_Type_Connect.HMA_I i (from_nat i)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have [transfer_rule]: "A $$ (i,i) = A' $h from_nat i $h from_nat i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
have "A $$ (i,i) = index_hma A' (from_nat i) (from_nat i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
have "... = A' $h from_nat i $h from_nat i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_hma A' (from_nat i) (from_nat i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
unfolding index_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $h from_nat i $h from_nat i = A' $h from_nat i $h from_nat i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index_hma A' (from_nat i) (from_nat i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have [transfer_rule]: "A $$ (k,k) = A' $h from_nat k $h from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
have "A $$ (k,k) = index_hma A' (from_nat k) (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (k, k) = index_hma A' (from_nat k) (from_nat k)
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
A $$ (k, k) = index_hma A' (from_nat k) (from_nat k)

goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (k, k) = index_hma A' (from_nat k) (from_nat k)

goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
have "... = A' $h from_nat k $h from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_hma A' (from_nat k) (from_nat k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
unfolding index_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $h from_nat k $h from_nat k = A' $h from_nat k $h from_nat k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index_hma A' (from_nat k) (from_nat k) = A' $h from_nat k $h from_nat k

goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (k, k) = A' $h from_nat k $h from_nat k

goal (1 subgoal):
 1. A $$ (k, k) = A' $h from_nat k $h from_nat k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $$ (k, k) = A' $h from_nat k $h from_nat k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $$ (k, k) = A' $h from_nat k $h from_nat k

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have dim_row_CARD: "dim_row A = CARD('nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = CARD('nr)
[PROOF STEP]
using HMA_M_AA' Mod_Type_Connect.dim_row_transfer_rule
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M A A'
Mod_Type_Connect.HMA_M ?A ?A' \<Longrightarrow> dim_row ?A = CARD(?'nr)

goal (1 subgoal):
 1. dim_row A = CARD('nr)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dim_row A = CARD('nr)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have dim_col_CARD: "dim_col A = CARD('nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col A = CARD('nc)
[PROOF STEP]
using HMA_M_AA' Mod_Type_Connect.dim_col_transfer_rule
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M A A'
Mod_Type_Connect.HMA_M ?A ?A' \<Longrightarrow> dim_col ?A = CARD(?'nc)

goal (1 subgoal):
 1. dim_col A = CARD('nc)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dim_col A = CARD('nc)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
let ?p = "fst (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
let ?v = "fst (snd (snd (snd (bezout (A $$ (i, i)) (A $$ (k, k))))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have "Mod_Type_Connect.HMA_M (fst ?d_JNF) (fst ?d_HA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))
[PROOF STEP]
unfolding diagonal_step_PQ_JNF_def diagonal_step_PQ_def Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (let m = dim_row A; n = dim_col A; (p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (k, k)); P = addrow (- v) k i (swaprows i k (addrow p k i (1\<^sub>m m))) in Let (multcol k (- (1::'a)) (addcol u k i (addcol q i k (1\<^sub>m n)))) (Pair P)) = Mod_Type_Connect.from_hma\<^sub>m (fst (let i_row = from_nat i; k_row = from_nat k; i_col = from_nat i; k_col = from_nat k; (p, q, u, v, d) = bezout (A' $h i_row $h from_nat i) (A' $h k_row $h from_nat k); P = row_add (interchange_rows (row_add (mat (1::'a)) k_row i_row p) i_row k_row) k_row i_row (- v) in Let (mult_column (column_add (column_add (mat (1::'a)) i_col k_col q) k_col i_col u) k_col (- (1::'a))) (Pair P)))
[PROOF STEP]
unfolding Let_def split_beta dim_row_CARD
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (addrow (- fst (snd (snd (snd (bezout (A $$ (i, i)) (A $$ (k, k))))))) k i (swaprows i k (addrow (fst (bezout (A $$ (i, i)) (A $$ (k, k)))) k i (1\<^sub>m CARD('nr)))), multcol k (- (1::'a)) (addcol (fst (snd (snd (bezout (A $$ (i, i)) (A $$ (k, k)))))) k i (addcol (fst (snd (bezout (A $$ (i, i)) (A $$ (k, k))))) i k (1\<^sub>m (dim_col A))))) = Mod_Type_Connect.from_hma\<^sub>m (fst (row_add (interchange_rows (row_add (mat (1::'a)) (from_nat k) (from_nat i) (fst (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))) (from_nat i) (from_nat k)) (from_nat k) (from_nat i) (- fst (snd (snd (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))))), mult_column (column_add (column_add (mat (1::'a)) (from_nat i) (from_nat k) (fst (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k))))) (from_nat k) (from_nat i) (fst (snd (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))))) (from_nat k) (- (1::'a))))
[PROOF STEP]
by (auto, transfer, auto simp add: Mod_Type_Connect.HMA_M_def Rel_def rel_funI)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
have "Mod_Type_Connect.HMA_M (snd ?d_JNF) (snd ?d_HA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))
[PROOF STEP]
unfolding diagonal_step_PQ_JNF_def diagonal_step_PQ_def Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let m = dim_row A; n = dim_col A; (p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (k, k)); P = addrow (- v) k i (swaprows i k (addrow p k i (1\<^sub>m m))) in Let (multcol k (- (1::'a)) (addcol u k i (addcol q i k (1\<^sub>m n)))) (Pair P)) = Mod_Type_Connect.from_hma\<^sub>m (snd (let i_row = from_nat i; k_row = from_nat k; i_col = from_nat i; k_col = from_nat k; (p, q, u, v, d) = bezout (A' $h i_row $h from_nat i) (A' $h k_row $h from_nat k); P = row_add (interchange_rows (row_add (mat (1::'a)) k_row i_row p) i_row k_row) k_row i_row (- v) in Let (mult_column (column_add (column_add (mat (1::'a)) i_col k_col q) k_col i_col u) k_col (- (1::'a))) (Pair P)))
[PROOF STEP]
unfolding Let_def split_beta dim_col_CARD
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (addrow (- fst (snd (snd (snd (bezout (A $$ (i, i)) (A $$ (k, k))))))) k i (swaprows i k (addrow (fst (bezout (A $$ (i, i)) (A $$ (k, k)))) k i (1\<^sub>m (dim_row A)))), multcol k (- (1::'a)) (addcol (fst (snd (snd (bezout (A $$ (i, i)) (A $$ (k, k)))))) k i (addcol (fst (snd (bezout (A $$ (i, i)) (A $$ (k, k))))) i k (1\<^sub>m CARD('nc))))) = Mod_Type_Connect.from_hma\<^sub>m (snd (row_add (interchange_rows (row_add (mat (1::'a)) (from_nat k) (from_nat i) (fst (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))) (from_nat i) (from_nat k)) (from_nat k) (from_nat i) (- fst (snd (snd (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))))), mult_column (column_add (column_add (mat (1::'a)) (from_nat i) (from_nat k) (fst (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k))))) (from_nat k) (from_nat i) (fst (snd (snd (bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat k $h from_nat k)))))) (from_nat k) (- (1::'a))))
[PROOF STEP]
by (auto, transfer, auto simp add: Mod_Type_Connect.HMA_M_def Rel_def rel_funI)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>Mod_Type_Connect.HMA_M x y; xa = ya\<rbrakk> \<Longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i k xa) (diagonal_step_PQ y i k ya)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))
Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))
Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))

goal (1 subgoal):
 1. rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i k bezout) (diagonal_step_PQ A' i k bezout')
[PROOF STEP]
unfolding rel_prod_conv
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))
Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))

goal (1 subgoal):
 1. (case diagonal_step_PQ_JNF A i k bezout of (a, b) \<Rightarrow> \<lambda>(c, d). Mod_Type_Connect.HMA_M a c \<and> Mod_Type_Connect.HMA_M b d) (diagonal_step_PQ A' i k bezout')
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i k bezout)) (fst (diagonal_step_PQ A' i k bezout))
Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i k bezout)) (snd (diagonal_step_PQ A' i k bezout))
Mod_Type_Connect.HMA_M A A'
bezout = bezout'

goal (1 subgoal):
 1. (case diagonal_step_PQ_JNF A i k bezout of (a, b) \<Rightarrow> \<lambda>(c, d). Mod_Type_Connect.HMA_M a c \<and> Mod_Type_Connect.HMA_M b d) (diagonal_step_PQ A' i k bezout')
[PROOF STEP]
by (simp add: split_beta)
[PROOF STATE]
proof (state)
this:
rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i k bezout) (diagonal_step_PQ A' i k bezout')

goal:
No subgoals!
[PROOF STEP]
qed