[STATEMENT]
lemma "Second \<in> normalfilters"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second \<in> normalfilters
[PROOF STEP]
apply (unfold normalfilters_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second \<in> {F \<in> filters. \<forall>a b. (a l\<rightarrow> b \<in> F) = (a r\<rightarrow> b \<in> F)}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Second \<in> filters
 2. \<And>a b. a l\<rightarrow> b \<in> Second \<Longrightarrow> a r\<rightarrow> b \<in> Second
 3. \<And>a b. a r\<rightarrow> b \<in> Second \<Longrightarrow> a l\<rightarrow> b \<in> Second
[PROOF STEP]
apply (unfold filters_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Second \<in> {F. F \<noteq> {} \<and> (\<forall>a b. a \<in> F \<and> b \<in> F \<longrightarrow> a * b \<in> F) \<and> (\<forall>a b. a \<in> F \<and> a \<le> b \<longrightarrow> b \<in> F)}
 2. \<And>a b. a l\<rightarrow> b \<in> Second \<Longrightarrow> a r\<rightarrow> b \<in> Second
 3. \<And>a b. a r\<rightarrow> b \<in> Second \<Longrightarrow> a l\<rightarrow> b \<in> Second
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. Second = {} \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>a \<in> Second; b \<in> Second\<rbrakk> \<Longrightarrow> a * b \<in> Second
 3. \<And>a b. \<lbrakk>a \<in> Second; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> Second
 4. \<And>a b. a l\<rightarrow> b \<in> Second \<Longrightarrow> a r\<rightarrow> b \<in> Second
 5. \<And>a b. a r\<rightarrow> b \<in> Second \<Longrightarrow> a l\<rightarrow> b \<in> Second
[PROOF STEP]
apply (unfold Second_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {x. \<exists>b. x = Abs_OrdSum (1::'a, b)} = {} \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>a \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}; b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}\<rbrakk> \<Longrightarrow> a * b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}
 3. \<And>a b. \<lbrakk>a \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}; a \<le> b\<rbrakk> \<Longrightarrow> b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}
 4. \<And>a b. a l\<rightarrow> b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)} \<Longrightarrow> a r\<rightarrow> b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}
 5. \<And>a b. a r\<rightarrow> b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)} \<Longrightarrow> a l\<rightarrow> b \<in> {x. \<exists>b. x = Abs_OrdSum (1::'a, b)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ba bb. \<exists>b. Abs_OrdSum (1::'a, ba) * Abs_OrdSum (1::'a, bb) = Abs_OrdSum (1::'a, b)
 2. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = "ba * bb" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ba bb. Abs_OrdSum (1::'a, ba) * Abs_OrdSum (1::'a, bb) = Abs_OrdSum (1::'a, ba * bb)
 2. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: times_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = "second b" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> b = Abs_OrdSum (1::'a, second b)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) \<le> b; Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)\<rbrakk> \<Longrightarrow> b = Abs_OrdSum (1::'a, second b)
 2. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) \<le> b; Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)\<rbrakk> \<Longrightarrow> b = Abs_OrdSum (first b, second b)
 2. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: first_def second_def Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "first b = 1")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) \<le> b; first b = (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, second b) = Abs_OrdSum (first b, second b)
 2. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> first b = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. Abs_OrdSum (1::'a, ba) \<le> b \<Longrightarrow> first b = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: order_OrdSum_def one_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. (if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first (Abs_OrdSum (1::'a, ba)) l\<rightarrow> first b, 1::'b) else if first (Abs_OrdSum (1::'a, ba)) = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second (Abs_OrdSum (1::'a, ba)) l\<rightarrow> second b) else if first (Abs_OrdSum (1::'a, ba)) = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b) \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (unfold second_def first_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. (if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b) \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 3. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 4. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b. \<lbrakk>snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b)); True\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 3. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 4. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 2. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); \<not> (ba = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "fst (Rep_OrdSum b) = (1::'a)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if fst (Rep_OrdSum (Abs_OrdSum (1::'a, ba))) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>(if snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "snd (Rep_OrdSum b) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b ba. \<lbrakk>(if snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>b ba. \<lbrakk>(if snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, 1::'b); ba \<noteq> (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> False
 3. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b ba. \<lbrakk>b = Abs_OrdSum (1::'a, 1::'b); ba \<noteq> (1::'b); fst (Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))) \<noteq> (1::'a); snd (Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))) = (1::'b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. (if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba) \<Longrightarrow> (fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> (fst (Rep_OrdSum b) = (1::'a) \<longrightarrow> (\<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b))) \<and> (fst (Rep_OrdSum b) \<noteq> (1::'a) \<longrightarrow> (\<exists>ba. b = Abs_OrdSum (1::'a, ba)))) \<and> ((fst (Rep_OrdSum a) = (1::'a) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) \<longrightarrow> (\<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba))) \<and> ((fst (Rep_OrdSum a) = (1::'a) \<longrightarrow> fst (Rep_OrdSum b) \<noteq> (1::'a)) \<longrightarrow> (snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> (\<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba))) \<and> ((snd (Rep_OrdSum a) = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (\<exists>b. Abs_OrdSum (1::'a, b) = 1))))
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 8. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 10. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a l\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a l\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
A total of 14 subgoals...
[PROOF STEP]
apply (unfold second_def first_def)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 8. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 10. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
A total of 14 subgoals...
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 8. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 8. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, ba) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, ba) = Abs_OrdSum (1::'a, b)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 8. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = 1 in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ba. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba)); True\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = 1 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b)
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba)); True\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 2. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. a r\<rightarrow> b = Abs_OrdSum (1::'a, ba) \<Longrightarrow> \<exists>ba. a l\<rightarrow> b = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. (if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba) \<Longrightarrow> (fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> (fst (Rep_OrdSum b) = (1::'a) \<longrightarrow> (\<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b))) \<and> (fst (Rep_OrdSum b) \<noteq> (1::'a) \<longrightarrow> (\<exists>ba. b = Abs_OrdSum (1::'a, ba)))) \<and> ((fst (Rep_OrdSum a) = (1::'a) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) \<longrightarrow> (\<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba))) \<and> ((fst (Rep_OrdSum a) = (1::'a) \<longrightarrow> fst (Rep_OrdSum b) \<noteq> (1::'a)) \<longrightarrow> (snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> (\<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba))) \<and> ((snd (Rep_OrdSum a) = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (\<exists>b. Abs_OrdSum (1::'a, b) = 1))))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 8. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 10. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (first a r\<rightarrow> first b, 1::'b) else if first a = (1::'a) \<and> first b = (1::'a) then Abs_OrdSum (1::'a, second a r\<rightarrow> second b) else if first a = (1::'a) \<and> second b = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
A total of 13 subgoals...
[PROOF STEP]
apply (unfold second_def first_def)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 8. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 9. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 10. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
A total of 13 subgoals...
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
[PROOF STEP]
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, b)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 8. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, ba) = Abs_OrdSum (1::'a, b)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, ba) = Abs_OrdSum (1::'a, b)
 3. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 5. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
 6. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 7. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) = Abs_OrdSum (1::'a, ba)
 8. \<And>a b ba. \<lbrakk>Abs_OrdSum (1::'a, ba) = 1; fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>b. Abs_OrdSum (1::'a, b) = 1
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (case_tac "snd (Rep_OrdSum a) = (1::'b)")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>(if snd (Rep_OrdSum a) = (1::'b) then Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) else if fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) then Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b)) else if fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) then b else 1) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. b = Abs_OrdSum (1::'a, ba)
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 4. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = 1 in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba)); True\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 3. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> \<exists>ba. Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba)
[PROOF STEP]
apply (rule_tac x = 1 in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, 1::'b)
[PROOF STEP]
apply (rule Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, 1::'b))
[PROOF STEP]
apply (simp_all add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba)); True\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
[PROOF STEP]
apply (simp add: second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b) = (1::'a)\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b) = (1::'a)
 2. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
[PROOF STEP]
apply (simp add: left_lesseq [THEN sym] right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b) = Abs_OrdSum (1::'a, ba); fst (Rep_OrdSum a) \<noteq> (1::'a); fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) = Rep_OrdSum (Abs_OrdSum (1::'a, ba))
[PROOF STEP]
by simp