[STATEMENT]
lemma prod_1: "((a::'a N) l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> c) l\<rightarrow> c
[PROOF STEP]
apply (unfold impl_N_def times_N_def Abs_N_inverse Rep_N_inverse order_N_def one_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a))) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N c - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N c - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N c - (Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N c - (Rep_N c - Rep_N (Abs_N ((Rep_N a - Rep_N b) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N a - Rep_N b) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - Rep_N (Abs_N ((Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - Rep_N (Abs_N ((Rep_N b - Rep_N a) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N b - Rep_N a) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subgoal_tac "inf (inf (Rep_N c - inf (Rep_N c - inf (Rep_N a - Rep_N b) 0) 0) 0 - inf (Rep_N c - inf (Rep_N b - Rep_N a) 0) 0) 0 = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> Abs_N (((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
 2. ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (rule inf_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N c - (Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N c + - ((Rep_N c - (Rep_N a - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a))) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N c + - ((Rep_N c + - ((Rep_N a - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a))) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N c + - ((Rep_N c + - ((Rep_N a + - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a))) \<sqinter> (0::'a) - (Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N c + - ((Rep_N c + - ((Rep_N a + - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a))) \<sqinter> (0::'a) + - ((Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a))
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) + - (- ((Rep_N c - (Rep_N b - Rep_N a) \<sqinter> (0::'a)) \<sqinter> (0::'a))) \<le> (Rep_N c + - ((Rep_N c + - ((Rep_N a + - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a))) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c - (Rep_N b - Rep_N a) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (Rep_N c + - (Rep_N c + - (Rep_N a + - Rep_N b))) \<sqinter> (0::'a) \<squnion> Rep_N c
[PROOF STEP]
apply (simp add: diff_minus minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)) \<sqinter> (0::'a) \<squnion> Rep_N c
[PROOF STEP]
(*apply (subst sup_inf_distrib2) - why it does not work*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)) \<sqinter> (0::'a) \<squnion> Rep_N c
[PROOF STEP]
apply (subst sup_inf_distrib2_lgroup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c) \<sqinter> ((0::'a) \<squnion> Rep_N c)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
(*apply safe*)
  (*apply (subst inf_sup_distrib2) - why it does not work*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b) \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
apply (subst inf_sup_distrib2_lgroup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<squnion> Rep_N c \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
(*apply safe*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
apply (rule_tac y="Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)
 2. Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c) \<squnion> Rep_N c
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)
[PROOF STEP]
apply (rule_tac y="Rep_N c + (Rep_N a + - Rep_N b)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N c + (Rep_N a + - Rep_N b)) \<sqinter> (0::'a) \<le> Rep_N c + (Rep_N a + - Rep_N b)
 2. Rep_N c + (Rep_N a + - Rep_N b) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c + (Rep_N a + - Rep_N b) \<le> Rep_N c + (Rep_N a + - Rep_N b + - Rep_N c)
[PROOF STEP]
apply (rule add_order_preserving_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a + - Rep_N b \<le> Rep_N a + - Rep_N b + - Rep_N c
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a + - Rep_N b \<le> Rep_N a + (- Rep_N b + - Rep_N c)
[PROOF STEP]
apply (rule add_order_preserving_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b \<le> - Rep_N b + - Rep_N c
[PROOF STEP]
apply (rule left_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- Rep_N b) + - Rep_N b \<le> - Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> - Rep_N c
[PROOF STEP]
apply (cut_tac x = c in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c \<in> N \<Longrightarrow> (0::'a) \<le> - Rep_N c
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> - Rep_N c
[PROOF STEP]
apply (rule minus_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c \<le> (0::'a) \<Longrightarrow> - (- Rep_N c) \<le> - (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma prod_2: "((a::'a N) r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> c) r\<rightarrow> c
[PROOF STEP]
apply (unfold impr_N_def times_N_def Abs_N_inverse Rep_N_inverse right_lesseq one_N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N a + Rep_N b) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N (Abs_N ((- Rep_N a + Rep_N b) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- ((- Rep_N (Abs_N ((- Rep_N a + Rep_N b) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) + Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- ((- Rep_N (Abs_N ((- Rep_N a + Rep_N b) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) + Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N a + Rep_N b) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- Rep_N (Abs_N ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- Rep_N (Abs_N ((- Rep_N b + Rep_N a) \<sqinter> (0::'a))) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + Rep_N a) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subgoal_tac "inf (- inf (- inf (- Rep_N a + Rep_N b) (0::'a) + Rep_N c) (0::'a) + inf (- inf (- inf (- Rep_N b + Rep_N a) (0::'a) + Rep_N c) (0::'a) + Rep_N c) (0::'a))
            (0::'a) = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> Abs_N ((- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
 2. (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (rule inf_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> - ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (rule minus_order)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. - (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) \<le> - (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst minus_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. - ((- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + - (- ((- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a))) \<le> - (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst minus_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. - ((- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a) \<le> - (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst minus_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. - ((- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + (- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (rule left_move_to_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a) \<le> - (- ((- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a))) + (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst minus_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- ((- Rep_N a + Rep_N b) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a) \<le> (- ((- ((- Rep_N b + Rep_N a) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a)) + Rep_N c) \<sqinter> (0::'a) + (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- (- Rep_N a + Rep_N b) + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (- (- (- Rep_N b + Rep_N a) + Rep_N c) + Rep_N c) \<sqinter> (0::'a) \<squnion> Rep_N c
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (simp add: minus_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c) \<sqinter> (0::'a) \<squnion> Rep_N c
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c) \<sqinter> (0::'a) \<squnion> Rep_N c
[PROOF STEP]
(*apply (subst sup_inf_distrib2) - why it does not work*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c) \<sqinter> (0::'a) \<squnion> Rep_N c
[PROOF STEP]
apply (subst sup_inf_distrib2_lgroup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> (- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c) \<sqinter> ((0::'a) \<squnion> Rep_N c)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
(*  apply safe*)
  (*apply (subst inf_sup_distrib2) - why it does not work*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c \<squnion> Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
apply (subst inf_sup_distrib2_lgroup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<squnion> Rep_N c \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
(*  apply safe*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
apply (rule_tac y = "- Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c
 2. - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c \<squnion> Rep_N c
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c
[PROOF STEP]
apply (rule_tac y = "- Rep_N b + Rep_N a + Rep_N c" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + Rep_N a + Rep_N c) \<sqinter> (0::'a) \<le> - Rep_N b + Rep_N a + Rep_N c
 2. - Rep_N b + Rep_N a + Rep_N c \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b + Rep_N a + Rep_N c \<le> - Rep_N c + (- Rep_N b + Rep_N a) + Rep_N c
[PROOF STEP]
apply (rule add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b + Rep_N a \<le> - Rep_N c + (- Rep_N b + Rep_N a)
[PROOF STEP]
apply (simp add: add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b + Rep_N a \<le> - Rep_N c + - Rep_N b + Rep_N a
[PROOF STEP]
apply (rule add_order_preserving_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_N b \<le> - Rep_N c + - Rep_N b
[PROOF STEP]
apply (rule left_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- Rep_N c) + - Rep_N b \<le> - Rep_N b
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- Rep_N c) \<le> - Rep_N b + - (- Rep_N b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c \<le> (0::'a)
[PROOF STEP]
apply (cut_tac x = c in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N c \<in> N \<Longrightarrow> Rep_N c \<le> (0::'a)
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma prod_3: "(b::'a N) l\<rightarrow> b * b \<le> a \<sqinter> (a l\<rightarrow> b) l\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> b * b \<le> a \<sqinter> (a l\<rightarrow> b) l\<rightarrow> b
[PROOF STEP]
apply (simp add: impl_N_def times_N_def Abs_N_inverse Rep_N_inverse order_N_def one_N_def Rep_N_inf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N (Abs_N ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a))) - Rep_N (Abs_N (Rep_N b \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - Rep_N (Abs_N (Rep_N b \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (simp add: add.assoc N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - Rep_N (Abs_N (Rep_N b \<sqinter> (0::'a)))) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> (0::'a) \<in> N
 2. Abs_N (((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - Rep_N b \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (simp add: add.assoc N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - Rep_N b \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
[PROOF STEP]
apply (subgoal_tac "inf (inf (sup (Rep_N b - Rep_N a) (sup (Rep_N b - (Rep_N b - Rep_N a)) (Rep_N b))) (0::'a) - inf (Rep_N b + Rep_N b - Rep_N b) (0::'a)) (0::'a) = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a) \<Longrightarrow> Abs_N (((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - Rep_N b \<sqinter> (0::'a)) \<sqinter> (0::'a)) = Abs_N (0::'a)
 2. ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a) = (0::'a)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a) \<le> (0::'a)
 2. (0::'a) \<le> ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b + - Rep_N a \<squnion> (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) - (Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a)) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) + - ((Rep_N b + Rep_N b - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> ((Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) + - ((Rep_N b + Rep_N b + - Rep_N b) \<sqinter> (0::'a))) \<sqinter> (0::'a)
[PROOF STEP]
apply (rule inf_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) \<le> (Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a) + - ((Rep_N b + Rep_N b + - Rep_N b) \<sqinter> (0::'a))
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) + - (- ((Rep_N b + Rep_N b + - Rep_N b) \<sqinter> (0::'a))) \<le> (Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply (subst minus_minus)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (0::'a) + (Rep_N b + Rep_N b + - Rep_N b) \<sqinter> (0::'a) \<le> (Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)) \<sqinter> (0::'a)
 2. (0::'a) \<le> (0::'a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + Rep_N b + - Rep_N b) \<sqinter> (0::'a) \<le> Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)
[PROOF STEP]
apply (simp add: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<sqinter> (0::'a) \<le> Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)
[PROOF STEP]
apply (rule_tac y = "Rep_N b" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> (0::'a) \<le> Rep_N b
 2. Rep_N b \<le> Rep_N b + - Rep_N a \<squnion> (Rep_N b + - (Rep_N b + - Rep_N a) \<squnion> Rep_N b)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma prod_4: "(b::'a N) r\<rightarrow> b * b \<le> a \<sqinter> (a r\<rightarrow> b) r\<rightarrow> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> b * b \<le> a \<sqinter> (a r\<rightarrow> b) r\<rightarrow> b
[PROOF STEP]
apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N b \<sqinter> (0::'a)) \<le> Abs_N ((- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst order_Abs_N [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. Rep_N b \<sqinter> (0::'a) \<in> N
 2. (- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a) \<in> N
 3. Rep_N b \<sqinter> (0::'a) \<le> (- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add:  N_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a) \<in> N
 2. Rep_N b \<sqinter> (0::'a) \<le> (- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add:  N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<sqinter> (0::'a) \<le> (- Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)) \<sqinter> (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<sqinter> (0::'a) \<le> - Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)
[PROOF STEP]
apply (rule_tac y = "- Rep_N a + Rep_N b" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> (0::'a) \<le> - Rep_N a + Rep_N b
 2. - Rep_N a + Rep_N b \<le> - Rep_N a + Rep_N b \<squnion> (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<sqinter> (0::'a) \<le> - Rep_N a + Rep_N b
[PROOF STEP]
apply (rule_tac y = "Rep_N b" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Rep_N b \<sqinter> (0::'a) \<le> Rep_N b
 2. Rep_N b \<le> - Rep_N a + Rep_N b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b \<le> - Rep_N a + Rep_N b
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N b + - Rep_N b \<le> - Rep_N a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> - Rep_N a
[PROOF STEP]
apply (rule minus_order)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (- Rep_N a) \<le> - (0::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<le> (0::'a)
[PROOF STEP]
apply (cut_tac x = a in Rep_N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_N a \<in> N \<Longrightarrow> Rep_N a \<le> (0::'a)
[PROOF STEP]
by (simp add: N_def)


[STATEMENT]
lemma prod_5: "(((a::'a N) l\<rightarrow> b) l\<rightarrow> b) * (c * a l\<rightarrow> f * a) * (c * b l\<rightarrow> f * b) \<le> c l\<rightarrow> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a l\<rightarrow> b) l\<rightarrow> b) * (c * a l\<rightarrow> f * a) * (c * b l\<rightarrow> f * b) \<le> c l\<rightarrow> f
[PROOF STEP]
apply (simp add: impl_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N (Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a))) + Rep_N (Abs_N ((Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)))) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + Rep_N (Abs_N ((Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)))) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + Rep_N (Abs_N ((Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)))) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + Rep_N (Abs_N ((Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)))) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + Rep_N (Abs_N ((Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)))) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a)) \<le> Abs_N ((Rep_N f - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst order_Abs_N [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a) \<in> N
 2. (Rep_N f - Rep_N c) \<sqinter> (0::'a) \<in> N
 3. (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a) \<le> (Rep_N f - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add: N_def inf_assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Rep_N f - Rep_N c) \<sqinter> (0::'a) \<in> N
 2. (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a) \<le> (Rep_N f - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b - (Rep_N b - Rep_N a) \<squnion> Rep_N b) \<sqinter> (0::'a) + (Rep_N f + Rep_N a - (Rep_N c + Rep_N a)) \<sqinter> (0::'a) + (Rep_N f + Rep_N b - (Rep_N c + Rep_N b)) \<sqinter> (0::'a) \<le> (Rep_N f - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp only: diff_minus minus_add minus_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + (Rep_N a + - Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((Rep_N f + (Rep_N a + (- Rep_N a + - Rep_N c))) \<sqinter> (0::'a) + (Rep_N f + (Rep_N b + (- Rep_N b + - Rep_N c))) \<sqinter> (0::'a)) \<le> (Rep_N f + - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst (4) add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + (Rep_N a + - Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((Rep_N f + (Rep_N a + - Rep_N a + - Rep_N c)) \<sqinter> (0::'a) + (Rep_N f + (Rep_N b + (- Rep_N b + - Rep_N c))) \<sqinter> (0::'a)) \<le> (Rep_N f + - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst (5) add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + (Rep_N a + - Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((Rep_N f + (Rep_N a + - Rep_N a + - Rep_N c)) \<sqinter> (0::'a) + (Rep_N f + (Rep_N b + - Rep_N b + - Rep_N c)) \<sqinter> (0::'a)) \<le> (Rep_N f + - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp only: right_minus add_0_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + (Rep_N a + - Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((Rep_N f + - Rep_N c) \<sqinter> (0::'a) + (Rep_N f + - Rep_N c) \<sqinter> (0::'a)) \<le> (Rep_N f + - Rep_N c) \<sqinter> (0::'a)
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + (Rep_N a + - Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) \<le> (Rep_N f + - Rep_N c) \<sqinter> (0::'a) + - ((Rep_N f + - Rep_N c) \<sqinter> (0::'a) + (Rep_N f + - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp only: minus_add add.assoc [THEN sym] add_0_left right_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_N b + Rep_N a + - Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) \<le> - ((Rep_N f + - Rep_N c) \<sqinter> (0::'a))
[PROOF STEP]
by (simp add: minus_add)


[STATEMENT]
lemma prod_6: "(((a::'a N) r\<rightarrow> b) r\<rightarrow> b) * (a * c r\<rightarrow> a * f) * (b * c r\<rightarrow> b * f) \<le> c r\<rightarrow> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a r\<rightarrow> b) r\<rightarrow> b) * (a * c r\<rightarrow> a * f) * (b * c r\<rightarrow> b * f) \<le> c r\<rightarrow> f
[PROOF STEP]
apply (simp add: impr_N_def times_N_def Abs_N_inverse Rep_N_inverse Rep_N_inf minus_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N (Rep_N (Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a))) + Rep_N (Abs_N ((- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)))) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + Rep_N (Abs_N ((- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)))) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + Rep_N (Abs_N ((- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a))) + Rep_N (Abs_N ((- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)))) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + Rep_N (Abs_N ((- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)))) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + Rep_N (Abs_N ((- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)))) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst Abs_N_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a) \<in> N
 2. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_N ((- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a)) \<le> Abs_N ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (subst order_Abs_N [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a) \<in> N
 2. (- Rep_N c + Rep_N f) \<sqinter> (0::'a) \<in> N
 3. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add: N_def inf_assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (- Rep_N c + Rep_N f) \<sqinter> (0::'a) \<in> N
 2. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp add: N_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N a + (Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + - Rep_N b + (Rep_N b + Rep_N f)) \<sqinter> (0::'a) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp only: diff_minus minus_add minus_minus add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (Rep_N a + Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((- Rep_N c + (- Rep_N a + (Rep_N a + Rep_N f))) \<sqinter> (0::'a) + (- Rep_N c + (- Rep_N b + (Rep_N b + Rep_N f))) \<sqinter> (0::'a)) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst (4) add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (Rep_N a + Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((- Rep_N c + (- Rep_N a + Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + (- Rep_N b + (Rep_N b + Rep_N f))) \<sqinter> (0::'a)) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (subst (5) add.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (Rep_N a + Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((- Rep_N c + (- Rep_N a + Rep_N a + Rep_N f)) \<sqinter> (0::'a) + (- Rep_N c + (- Rep_N b + Rep_N b + Rep_N f)) \<sqinter> (0::'a)) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (simp only: left_minus add_0_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (Rep_N a + Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) + ((- Rep_N c + Rep_N f) \<sqinter> (0::'a) + (- Rep_N c + Rep_N f) \<sqinter> (0::'a)) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a)
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + (Rep_N a + Rep_N b) \<squnion> Rep_N b) \<sqinter> (0::'a) \<le> (- Rep_N c + Rep_N f) \<sqinter> (0::'a) + - ((- Rep_N c + Rep_N f) \<sqinter> (0::'a) + (- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
apply (simp only: minus_add add.assoc [THEN sym] add_0_left right_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rep_N b + Rep_N a + Rep_N b \<squnion> Rep_N b) \<sqinter> (0::'a) \<le> - ((- Rep_N c + Rep_N f) \<sqinter> (0::'a))
[PROOF STEP]
by (simp add: minus_add)


[STATEMENT]
lemma [simp]: "(1, b) \<in> OrdSum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a, b) \<in> OrdSum
[PROOF STEP]
by (simp add: OrdSum_def)


[STATEMENT]
lemma if_unfold_left: "((if a then b else c) = d) = ((a\<longrightarrow> b = d) \<and> (\<not> a \<longrightarrow> c = d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if a then b else c) = d) = ((a \<longrightarrow> b = d) \<and> (\<not> a \<longrightarrow> c = d))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma if_unfold_right: "(d = (if a then b else c)) = ((a \<longrightarrow> d = b) \<and> (\<not> a \<longrightarrow> d = c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d = (if a then b else c)) = ((a \<longrightarrow> d = b) \<and> (\<not> a \<longrightarrow> d = c))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fst_snd_eq: "fst a = x \<Longrightarrow> snd a = y \<Longrightarrow> (x, y) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst a = x; snd a = y\<rbrakk> \<Longrightarrow> (x, y) = a
[PROOF STEP]
apply (subgoal_tac "x = fst a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst a = x; snd a = y; x = fst a\<rbrakk> \<Longrightarrow> (x, y) = a
 2. \<lbrakk>fst a = x; snd a = y\<rbrakk> \<Longrightarrow> x = fst a
[PROOF STEP]
apply (subgoal_tac "y = snd a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>fst a = x; snd a = y; x = fst a; y = snd a\<rbrakk> \<Longrightarrow> (x, y) = a
 2. \<lbrakk>fst a = x; snd a = y; x = fst a\<rbrakk> \<Longrightarrow> y = snd a
 3. \<lbrakk>fst a = x; snd a = y\<rbrakk> \<Longrightarrow> x = fst a
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>snd a = y; x = fst a; y = snd a; True\<rbrakk> \<Longrightarrow> (x, y) = a
 2. \<lbrakk>fst a = x; snd a = y; x = fst a\<rbrakk> \<Longrightarrow> y = snd a
 3. \<lbrakk>fst a = x; snd a = y\<rbrakk> \<Longrightarrow> x = fst a
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x = fst a; y = snd a; True; True\<rbrakk> \<Longrightarrow> (x, y) = a
 2. \<lbrakk>fst a = x; snd a = y; x = fst a\<rbrakk> \<Longrightarrow> y = snd a
 3. \<lbrakk>fst a = x; snd a = y\<rbrakk> \<Longrightarrow> x = fst a
[PROOF STEP]
by simp_all


[STATEMENT]
lemma OrdSum_first [simp]: "(a, 1) \<in> OrdSum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, 1::'d) \<in> OrdSum
[PROOF STEP]
by (simp add: OrdSum_def)


[STATEMENT]
lemma OrdSum_second [simp]: "(1, b) \<in> OrdSum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'c, b) \<in> OrdSum
[PROOF STEP]
by (simp add: OrdSum_def)


[STATEMENT]
lemma Rep_OrdSum_eq: "Rep_OrdSum x = Rep_OrdSum y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_OrdSum x = Rep_OrdSum y \<Longrightarrow> x = y
[PROOF STEP]
apply (subgoal_tac "Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_OrdSum x = Rep_OrdSum y; Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)\<rbrakk> \<Longrightarrow> x = y
 2. Rep_OrdSum x = Rep_OrdSum y \<Longrightarrow> Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y); True\<rbrakk> \<Longrightarrow> x = y
 2. Rep_OrdSum x = Rep_OrdSum y \<Longrightarrow> Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)
[PROOF STEP]
apply (simp add: Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_OrdSum x = Rep_OrdSum y \<Longrightarrow> Abs_OrdSum (Rep_OrdSum x) = Abs_OrdSum (Rep_OrdSum y)
[PROOF STEP]
by simp


[STATEMENT]
lemma Abs_OrdSum_eq: "x \<in> OrdSum \<Longrightarrow> y \<in> OrdSum \<Longrightarrow> Abs_OrdSum x = Abs_OrdSum y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (subgoal_tac "Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y; Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)
[PROOF STEP]
apply (unfold Abs_OrdSum_inverse) [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y; x = y\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>x \<in> OrdSum; y \<in> OrdSum; Abs_OrdSum x = Abs_OrdSum y\<rbrakk> \<Longrightarrow> Rep_OrdSum (Abs_OrdSum x) = Rep_OrdSum (Abs_OrdSum y)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma [simp]: "fst (Rep_OrdSum a) \<noteq> 1 \<Longrightarrow> (snd (Rep_OrdSum a) \<noteq> 1 = False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum a) \<noteq> (1::'c) \<Longrightarrow> (snd (Rep_OrdSum a) \<noteq> (1::'d)) = False
[PROOF STEP]
apply (cut_tac x = a in Rep_OrdSum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'c); Rep_OrdSum a \<in> OrdSum\<rbrakk> \<Longrightarrow> (snd (Rep_OrdSum a) \<noteq> (1::'d)) = False
[PROOF STEP]
apply (simp add: OrdSum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'c); (\<exists>aa. Rep_OrdSum a = (aa, 1::'d)) \<or> (\<exists>b. Rep_OrdSum a = (1::'c, b))\<rbrakk> \<Longrightarrow> snd (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_not_one_snd: "fst (Rep_OrdSum a) \<noteq> 1 \<Longrightarrow> (snd (Rep_OrdSum a) = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum a) \<noteq> (1::'c) \<Longrightarrow> snd (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
apply (cut_tac x = a in Rep_OrdSum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'c); Rep_OrdSum a \<in> OrdSum\<rbrakk> \<Longrightarrow> snd (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
apply (simp add: OrdSum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'c); (\<exists>aa. Rep_OrdSum a = (aa, 1::'d)) \<or> (\<exists>b. Rep_OrdSum a = (1::'c, b))\<rbrakk> \<Longrightarrow> snd (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
by auto


[STATEMENT]
lemma snd_not_one_fst: "snd (Rep_OrdSum a) \<noteq> 1 \<Longrightarrow> (fst (Rep_OrdSum a) = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_OrdSum a) \<noteq> (1::'c) \<Longrightarrow> fst (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
apply (cut_tac x = a in Rep_OrdSum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd (Rep_OrdSum a) \<noteq> (1::'c); Rep_OrdSum a \<in> OrdSum\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
apply (simp add: OrdSum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd (Rep_OrdSum a) \<noteq> (1::'c); (\<exists>aa. Rep_OrdSum a = (aa, 1::'c)) \<or> (\<exists>b. Rep_OrdSum a = (1::'d, b))\<rbrakk> \<Longrightarrow> fst (Rep_OrdSum a) = (1::'d)
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_not_one_simp [simp]: "fst (Rep_OrdSum c) \<noteq> 1 \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum c), 1) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum c), 1::'d) = c
[PROOF STEP]
apply (rule  Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (fst (Rep_OrdSum c), 1::'d)) = Rep_OrdSum c
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> (fst (Rep_OrdSum c), 1::'d) = Rep_OrdSum c
[PROOF STEP]
apply (rule fst_snd_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> fst (Rep_OrdSum c) = fst (Rep_OrdSum c)
 2. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> snd (Rep_OrdSum c) = (1::'d)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> snd (Rep_OrdSum c) = (1::'d)
[PROOF STEP]
by (simp add: fst_not_one_snd)


[STATEMENT]
lemma snd_not_one_simp [simp]: "snd (Rep_OrdSum c) \<noteq> 1 \<Longrightarrow> Abs_OrdSum (1, snd (Rep_OrdSum c)) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> Abs_OrdSum (1::'d, snd (Rep_OrdSum c)) = c
[PROOF STEP]
apply (rule  Rep_OrdSum_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> Rep_OrdSum (Abs_OrdSum (1::'d, snd (Rep_OrdSum c))) = Rep_OrdSum c
[PROOF STEP]
apply (simp add: Abs_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> (1::'d, snd (Rep_OrdSum c)) = Rep_OrdSum c
[PROOF STEP]
apply (rule fst_snd_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> fst (Rep_OrdSum c) = (1::'d)
 2. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> snd (Rep_OrdSum c) = snd (Rep_OrdSum c)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_OrdSum c) \<noteq> (1::'c) \<Longrightarrow> fst (Rep_OrdSum c) = (1::'d)
[PROOF STEP]
by (simp add: snd_not_one_fst)


[STATEMENT]
lemma  A: fixes a b::"('a, 'b) OrdSum" shows "(a l\<rightarrow> b) * a = a * (a r\<rightarrow> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) * a = a * (a r\<rightarrow> b)
[PROOF STEP]
apply (simp add: one_OrdSum_def impr_OrdSum_def impl_OrdSum_def second_def first_def Abs_OrdSum_inverse Rep_OrdSum_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (Rep_OrdSum a) = (1::'a) \<and> fst (Rep_OrdSum b) = (1::'a) \<longrightarrow> (snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)) \<and> ((snd (Rep_OrdSum a) = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)) \<and> (snd (Rep_OrdSum b) \<noteq> (1::'b) \<longrightarrow> Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) * a = a * Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b))))) \<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> (fst (Rep_OrdSum a) = (1::'a) \<longrightarrow> b * a = a * b) \<and> (fst (Rep_OrdSum a) \<noteq> (1::'a) \<longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) * a = a * Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b))) \<and> ((snd (Rep_OrdSum a) = (1::'b) \<longrightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)) \<longrightarrow> (fst (Rep_OrdSum a) = (1::'a) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> b * a = a * b) \<and> (fst (Rep_OrdSum a) \<noteq> (1::'a) \<longrightarrow> (snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) * a = a * Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)) \<and> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b))))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)
 2. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)
 3. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) * a = a * Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b))
 4. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b)) * a = a * Abs_OrdSum (1::'a, snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b))
 5. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) * a = a * Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)
 6. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)
 7. \<lbrakk>fst (Rep_OrdSum a) \<noteq> (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (1::'a, 1::'b) * a = a * Abs_OrdSum (1::'a, 1::'b)
 8. \<lbrakk>fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) = (1::'a)\<rbrakk> \<Longrightarrow> b * a = a * b
 9. \<lbrakk>fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum b) = (1::'b); fst (Rep_OrdSum a) \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> Abs_OrdSum (fst (Rep_OrdSum a) l\<rightarrow> fst (Rep_OrdSum b), 1::'b) * a = a * Abs_OrdSum (fst (Rep_OrdSum a) r\<rightarrow> fst (Rep_OrdSum b), 1::'b)
 10. \<lbrakk>fst (Rep_OrdSum b) \<noteq> (1::'a); snd (Rep_OrdSum a) \<noteq> (1::'b); fst (Rep_OrdSum a) = (1::'a); snd (Rep_OrdSum b) = (1::'b)\<rbrakk> \<Longrightarrow> b * a = a * b
A total of 12 subgoals...
[PROOF STEP]
apply (simp_all add: fst_snd_eq times_OrdSum_def left_right_impl_times first_def second_def Abs_OrdSum_inverse Rep_OrdSum_inverse )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> (snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b) = (1::'b) \<and> snd (Rep_OrdSum a) = (1::'b) \<longrightarrow> a = b) \<and> ((snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> snd (Rep_OrdSum a) \<noteq> (1::'b)) \<longrightarrow> snd (Rep_OrdSum a) = (1::'b) \<and> snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b) = (1::'b) \<longrightarrow> b = a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b); snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b) = (1::'b); snd (Rep_OrdSum a) = (1::'b)\<rbrakk> \<Longrightarrow> a = b
 2. \<lbrakk>fst (Rep_OrdSum a) = (1::'a); fst (Rep_OrdSum b) = (1::'a); snd (Rep_OrdSum b) \<noteq> (1::'b); snd (Rep_OrdSum a) = (1::'b); snd (Rep_OrdSum a) r\<rightarrow> snd (Rep_OrdSum b) = (1::'b); snd (Rep_OrdSum a) l\<rightarrow> snd (Rep_OrdSum b) \<noteq> (1::'b)\<rbrakk> \<Longrightarrow> b = a
[PROOF STEP]
by simp_all