[STATEMENT]
lemma OclOr1[simp]: "(invalid or true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid or true) = true
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)


[STATEMENT]
lemma OclOr2[simp]: "(invalid or false) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid or false) = invalid
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)


[STATEMENT]
lemma OclOr3[simp]: "(invalid or null) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid or null) = invalid
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma OclOr4[simp]: "(invalid or invalid) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid or invalid) = invalid
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def)


[STATEMENT]
lemma OclOr5[simp]: "(null or true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null or true) = true
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma OclOr6[simp]: "(null or false) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null or false) = null
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma OclOr7[simp]: "(null or null) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null or null) = null
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma OclOr8[simp]: "(null or invalid) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (null or invalid) = invalid
[PROOF STEP]
by(rule ext, simp add: OclOr_def OclNot_def OclAnd_def null_def invalid_def true_def false_def
                       bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma OclOr_commute: "(X or Y) = (Y or X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X or Y) = (Y or X)
[PROOF STEP]
by(simp add: OclOr_def OclAnd_commute)


[STATEMENT]
lemma OclOr_false1[simp]: "(false or Y) = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false or Y) = Y
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma OclOr_false2[simp]: "(Y or false) = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Y or false) = Y
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma OclOr_true1[simp]: "(true or Y) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true or Y) = true
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma OclOr_true2: "(Y or true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Y or true) = true
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma OclOr_bot1[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> (bot or X) \<tau> = bot \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> (UML_Types.bot_class.bot or X) \<tau> = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
apply(simp add: OclOr_def OclAnd_def OclNot_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> (case case case UML_Types.bot_class.bot \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> case case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor>) = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
apply(auto simp:true_def false_def bot_fun_def bot_option_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OclOr_bot2[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> (X or bot) \<tau> = bot \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> (X or UML_Types.bot_class.bot) \<tau> = UML_Types.bot_class.bot \<tau>
[PROOF STEP]
by(simp add: OclOr_commute)


[STATEMENT]
lemma OclOr_null1[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> X \<tau> \<noteq> bot \<tau> \<Longrightarrow> (null or X) \<tau> = null \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>X \<tau> \<noteq> true \<tau>; X \<tau> \<noteq> UML_Types.bot_class.bot \<tau>\<rbrakk> \<Longrightarrow> (null or X) \<tau> = null \<tau>
[PROOF STEP]
apply(simp add: OclOr_def OclAnd_def OclNot_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>X \<tau> \<noteq> true \<tau>; X \<tau> \<noteq> UML_Types.bot_class.bot \<tau>\<rbrakk> \<Longrightarrow> (case case case null \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> case case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<bottom> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> case case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> case X \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>xa\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>\<not> xa\<rfloor>\<rfloor>) = null \<tau>
[PROOF STEP]
apply(auto simp:true_def false_def bot_fun_def bot_option_def null_fun_def null_option_def
             split: option.split option.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x2. \<lbrakk>X (a, b) = \<lfloor>\<lfloor>x2\<rfloor>\<rfloor>; (case \<not> x2 of True \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | False \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<bottom>\<rbrakk> \<Longrightarrow> x2
 2. \<And>a b x2 x2a. \<lbrakk>X (a, b) = \<lfloor>\<lfloor>x2\<rfloor>\<rfloor>; (case \<not> x2 of True \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | False \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>\<lfloor>x2a\<rfloor>\<rfloor>\<rbrakk> \<Longrightarrow> x2
[PROOF STEP]
apply (metis (full_types) bool.simps(3) bot_option_def null_is_valid null_option_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x2a. \<lbrakk>X (a, b) = \<lfloor>\<lfloor>x2\<rfloor>\<rfloor>; (case \<not> x2 of True \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | False \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>\<lfloor>x2a\<rfloor>\<rfloor>\<rbrakk> \<Longrightarrow> x2
[PROOF STEP]
by (metis (full_types) bool.simps(3) option.distinct(1) option.sel)


[STATEMENT]
lemma OclOr_null2[simp]: "\<And>\<tau>. X \<tau> \<noteq> true \<tau> \<Longrightarrow> X \<tau> \<noteq> bot \<tau> \<Longrightarrow> (X or null) \<tau> = null \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>X \<tau> \<noteq> true \<tau>; X \<tau> \<noteq> UML_Types.bot_class.bot \<tau>\<rbrakk> \<Longrightarrow> (X or null) \<tau> = null \<tau>
[PROOF STEP]
by(simp add: OclOr_commute)


[STATEMENT]
lemma OclOr_assoc: "(X or (Y or Z)) = (X or Y or Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X or (Y or Z)) = (X or Y or Z)
[PROOF STEP]
by(simp add: OclOr_def OclAnd_assoc)


[STATEMENT]
lemma deMorgan1: "not(X and Y) = ((not X) or (not Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (X and Y) = (not X or not Y)
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma deMorgan2: "not(X or Y) = ((not X) and (not Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (X or Y) = (not X and not Y)
[PROOF STEP]
by(simp add: OclOr_def)


[STATEMENT]
lemma OclImplies_true1[simp]:"(true implies X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (true implies X) = X
[PROOF STEP]
by(simp add: OclImplies_def)


[STATEMENT]
lemma OclImplies_true2[simp]: "(X implies true) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X implies true) = true
[PROOF STEP]
by(simp add: OclImplies_def OclOr_true2)


[STATEMENT]
lemma OclImplies_false1[simp]:"(false implies X) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (false implies X) = true
[PROOF STEP]
by(simp add: OclImplies_def)


[STATEMENT]
lemma transform1: "P = true \<Longrightarrow> \<tau> \<Turnstile> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = true \<Longrightarrow> \<tau> \<Turnstile> P
[PROOF STEP]
by(simp add: OclValid_def)


[STATEMENT]
lemma transform1_rev: "\<forall> \<tau>. \<tau> \<Turnstile> P \<Longrightarrow> P = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau>. \<tau> \<Turnstile> P \<Longrightarrow> P = true
[PROOF STEP]
by(rule ext, auto simp: OclValid_def true_def)


[STATEMENT]
lemma transform2: "(P = Q) \<Longrightarrow> ((\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = Q \<Longrightarrow> (\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> Q)
[PROOF STEP]
by(auto simp: OclValid_def)


[STATEMENT]
lemma transform2_rev: "\<forall> \<tau>. (\<tau> \<Turnstile> \<delta> P) \<and> (\<tau> \<Turnstile> \<delta> Q) \<and> (\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> Q) \<Longrightarrow> P = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau>. \<tau> \<Turnstile> \<delta> P \<and> \<tau> \<Turnstile> \<delta> Q \<and> (\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> Q) \<Longrightarrow> P = Q
[PROOF STEP]
apply(rule ext,auto simp: OclValid_def true_def defined_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>a b. (if P (a, b) = UML_Types.bot_class.bot (a, b) \<or> P (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (if Q (a, b) = UML_Types.bot_class.bot (a, b) \<or> Q (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (P (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) = (Q (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) \<Longrightarrow> P (a, b) = Q (a, b)
[PROOF STEP]
apply(erule_tac x=a in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>b. (if P (a, b) = UML_Types.bot_class.bot (a, b) \<or> P (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (if Q (a, b) = UML_Types.bot_class.bot (a, b) \<or> Q (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (P (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) = (Q (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) \<Longrightarrow> P (a, b) = Q (a, b)
[PROOF STEP]
apply(erule_tac x=b in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (if P (a, b) = UML_Types.bot_class.bot (a, b) \<or> P (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (if Q (a, b) = UML_Types.bot_class.bot (a, b) \<or> Q (a, b) = null (a, b) then false (a, b) else true (a, b)) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<and> (P (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) = (Q (a, b) = \<lfloor>\<lfloor>True\<rfloor>\<rfloor>) \<Longrightarrow> P (a, b) = Q (a, b)
[PROOF STEP]
apply(auto simp: false_def true_def defined_def bot_Boolean_def null_Boolean_def
                 split: option.split_asm HOL.if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (*transform3:*)
assumes H : "P = true \<Longrightarrow> Q = true"
shows "\<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> Q
[PROOF STEP]
apply(simp add: OclValid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tau> = true \<tau> \<Longrightarrow> Q \<tau> = true \<tau>
[PROOF STEP]
apply(rule H[THEN fun_cong])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tau> = true \<tau> \<Longrightarrow> P = true
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. P \<tau> = true \<tau> \<Longrightarrow> P x = true x
[PROOF STEP]
oops


[STATEMENT]
lemma foundation1[simp]: "\<tau> \<Turnstile> true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> true
[PROOF STEP]
by(auto simp: OclValid_def)


[STATEMENT]
lemma foundation2[simp]: "\<not>(\<tau> \<Turnstile> false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> false
[PROOF STEP]
by(auto simp: OclValid_def true_def false_def)


[STATEMENT]
lemma foundation3[simp]: "\<not>(\<tau> \<Turnstile> invalid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> invalid
[PROOF STEP]
by(auto simp: OclValid_def true_def false_def invalid_def bot_option_def)


[STATEMENT]
lemma foundation4[simp]: "\<not>(\<tau> \<Turnstile> null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> null
[PROOF STEP]
by(auto simp: OclValid_def true_def false_def null_def null_fun_def null_option_def bot_option_def)


[STATEMENT]
lemma bool_split[simp]:
"(\<tau> \<Turnstile> (x \<triangleq> invalid)) \<or> (\<tau> \<Turnstile> (x \<triangleq> null)) \<or> (\<tau> \<Turnstile> (x \<triangleq> true)) \<or> (\<tau> \<Turnstile> (x \<triangleq> false))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null \<or> \<tau> \<Turnstile> x \<triangleq> true \<or> \<tau> \<Turnstile> x \<triangleq> false
[PROOF STEP]
apply(insert bool_split_0[of x \<tau>], auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid; \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> x \<triangleq> false; x \<tau> = invalid \<tau>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> x \<triangleq> true
 2. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid; \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> x \<triangleq> false; x \<tau> = null \<tau>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> x \<triangleq> true
 3. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid; \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> x \<triangleq> false; x \<tau> = true \<tau>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> x \<triangleq> true
 4. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid; \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> x \<triangleq> false; x \<tau> = false \<tau>\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> x \<triangleq> true
[PROOF STEP]
apply(simp_all add: OclValid_def StrongEq_def true_def null_def invalid_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma defined_split:
"(\<tau> \<Turnstile> \<delta> x) = ((\<not>(\<tau> \<Turnstile> (x \<triangleq> invalid))) \<and> (\<not> (\<tau> \<Turnstile> (x \<triangleq> null))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> x) = (\<tau> |\<noteq> x \<triangleq> invalid \<and> \<tau> |\<noteq> x \<triangleq> null)
[PROOF STEP]
by(simp add:defined_def true_def false_def invalid_def null_def
               StrongEq_def OclValid_def bot_fun_def null_fun_def)


[STATEMENT]
lemma valid_bool_split: "(\<tau> \<Turnstile> \<upsilon> A) = ((\<tau> \<Turnstile> A \<triangleq> null) \<or> (\<tau> \<Turnstile> A) \<or>  (\<tau> \<Turnstile> not A)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<upsilon> A) = (\<tau> \<Turnstile> A \<triangleq> null \<or> \<tau> \<Turnstile> A \<or> \<tau> \<Turnstile> not A)
[PROOF STEP]
by(auto simp:valid_def true_def false_def invalid_def null_def OclNot_def
             StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma defined_bool_split: "(\<tau> \<Turnstile> \<delta> A) = ((\<tau> \<Turnstile> A) \<or> (\<tau> \<Turnstile> not A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> A) = (\<tau> \<Turnstile> A \<or> \<tau> \<Turnstile> not A)
[PROOF STEP]
by(auto simp:defined_def true_def false_def invalid_def null_def OclNot_def
             StrongEq_def OclValid_def bot_fun_def bot_option_def null_option_def null_fun_def)


[STATEMENT]
lemma foundation5:
"\<tau> \<Turnstile> (P and Q) \<Longrightarrow> (\<tau> \<Turnstile> P) \<and> (\<tau> \<Turnstile> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P and Q \<Longrightarrow> \<tau> \<Turnstile> P \<and> \<tau> \<Turnstile> Q
[PROOF STEP]
by(simp add: OclAnd_def OclValid_def true_def false_def defined_def
             split: option.split option.split_asm bool.split bool.split_asm)


[STATEMENT]
lemma foundation6:
"\<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> \<delta> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> \<delta> P
[PROOF STEP]
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
                null_option_def null_fun_def bot_option_def bot_fun_def
             split: option.split option.split_asm)


[STATEMENT]
lemma foundation7[simp]:
"(\<tau> \<Turnstile> not (\<delta> x)) = (\<not> (\<tau> \<Turnstile> \<delta> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> not (\<delta> x)) = (\<tau> |\<noteq> \<delta> x)
[PROOF STEP]
by(simp add: OclNot_def OclValid_def true_def false_def defined_def
             split: option.split option.split_asm)


[STATEMENT]
lemma foundation7'[simp]:
"(\<tau> \<Turnstile> not (\<upsilon> x)) = (\<not> (\<tau> \<Turnstile> \<upsilon> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> not (\<upsilon> x)) = (\<tau> |\<noteq> \<upsilon> x)
[PROOF STEP]
by(simp add: OclNot_def OclValid_def true_def false_def valid_def
             split: option.split option.split_asm)


[STATEMENT]
lemma foundation8:
"(\<tau> \<Turnstile> \<delta> x) \<or> (\<tau> \<Turnstile> (x \<triangleq> invalid)) \<or> (\<tau> \<Turnstile> (x \<triangleq> null))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null
[PROOF STEP]
have 1 : "(\<tau> \<Turnstile> \<delta> x) \<or> (\<not>(\<tau> \<Turnstile> \<delta> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> |\<noteq> \<delta> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> \<delta> x \<or> \<tau> |\<noteq> \<delta> x

goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null
[PROOF STEP]
have 2 : "(\<not>(\<tau> \<Turnstile> \<delta> x)) = ((\<tau> \<Turnstile> (x \<triangleq> invalid)) \<or> (\<tau> \<Turnstile> (x \<triangleq> null)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> |\<noteq> \<delta> x) = (\<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null)
[PROOF STEP]
by(simp only: defined_split, simp)
[PROOF STATE]
proof (state)
this:
(\<tau> |\<noteq> \<delta> x) = (\<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null)

goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null
[PROOF STEP]
by(insert 1, simp add:2)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> \<delta> x \<or> \<tau> \<Turnstile> x \<triangleq> invalid \<or> \<tau> \<Turnstile> x \<triangleq> null

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foundation9:
"\<tau> \<Turnstile> \<delta> x \<Longrightarrow> (\<tau> \<Turnstile> not x) = (\<not> (\<tau> \<Turnstile> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<Longrightarrow> (\<tau> \<Turnstile> not x) = (\<tau> |\<noteq> x)
[PROOF STEP]
apply(simp add: defined_split )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> x \<triangleq> invalid \<and> \<tau> |\<noteq> x \<triangleq> null \<Longrightarrow> (\<tau> \<Turnstile> not x) = (\<tau> |\<noteq> x)
[PROOF STEP]
by(auto simp: OclNot_def null_fun_def null_option_def bot_option_def
                 OclValid_def invalid_def true_def null_def StrongEq_def)


[STATEMENT]
lemma foundation9':
"\<tau> \<Turnstile> not x \<Longrightarrow> \<not> (\<tau> \<Turnstile> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not x \<Longrightarrow> \<tau> |\<noteq> x
[PROOF STEP]
by(auto simp: foundation6 foundation9)


[STATEMENT]
lemma foundation9'':
"            \<tau> \<Turnstile> not x \<Longrightarrow> \<tau> \<Turnstile> \<delta> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not x \<Longrightarrow> \<tau> \<Turnstile> \<delta> x
[PROOF STEP]
by(metis OclNot3 OclNot_not OclValid_def cp_OclNot cp_defined defined4)


[STATEMENT]
lemma foundation10:
"\<tau> \<Turnstile> \<delta> x \<Longrightarrow> \<tau> \<Turnstile> \<delta> y \<Longrightarrow> (\<tau> \<Turnstile> (x and y)) = ( (\<tau> \<Turnstile> x) \<and> (\<tau> \<Turnstile> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; \<tau> \<Turnstile> \<delta> y\<rbrakk> \<Longrightarrow> (\<tau> \<Turnstile> x and y) = (\<tau> \<Turnstile> x \<and> \<tau> \<Turnstile> y)
[PROOF STEP]
apply(simp add: defined_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid \<and> \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> y \<triangleq> invalid \<and> \<tau> |\<noteq> y \<triangleq> null\<rbrakk> \<Longrightarrow> (\<tau> \<Turnstile> x and y) = (\<tau> \<Turnstile> x \<and> \<tau> \<Turnstile> y)
[PROOF STEP]
by(auto simp: OclAnd_def OclValid_def invalid_def
              true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
        split:bool.split_asm)


[STATEMENT]
lemma foundation10': "(\<tau> \<Turnstile> (A and B)) = ((\<tau> \<Turnstile> A) \<and> (\<tau> \<Turnstile> B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> A and B) = (\<tau> \<Turnstile> A \<and> \<tau> \<Turnstile> B)
[PROOF STEP]
(* stronger than foundation !*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> A and B) = (\<tau> \<Turnstile> A \<and> \<tau> \<Turnstile> B)
[PROOF STEP]
by(auto dest:foundation5 simp:foundation6 foundation10)


[STATEMENT]
lemma foundation11:
"\<tau> \<Turnstile> \<delta> x \<Longrightarrow>  \<tau> \<Turnstile> \<delta> y \<Longrightarrow> (\<tau> \<Turnstile> (x or y)) = ( (\<tau> \<Turnstile> x) \<or> (\<tau> \<Turnstile> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; \<tau> \<Turnstile> \<delta> y\<rbrakk> \<Longrightarrow> (\<tau> \<Turnstile> x or y) = (\<tau> \<Turnstile> x \<or> \<tau> \<Turnstile> y)
[PROOF STEP]
apply(simp add: defined_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> |\<noteq> x \<triangleq> invalid \<and> \<tau> |\<noteq> x \<triangleq> null; \<tau> |\<noteq> y \<triangleq> invalid \<and> \<tau> |\<noteq> y \<triangleq> null\<rbrakk> \<Longrightarrow> (\<tau> \<Turnstile> x or y) = (\<tau> \<Turnstile> x \<or> \<tau> \<Turnstile> y)
[PROOF STEP]
by(auto simp: OclNot_def OclOr_def OclAnd_def OclValid_def invalid_def
              true_def null_def StrongEq_def null_fun_def null_option_def bot_option_def
        split:bool.split_asm bool.split)


[STATEMENT]
lemma foundation12:
"\<tau> \<Turnstile> \<delta> x \<Longrightarrow> (\<tau> \<Turnstile> (x implies y)) = ( (\<tau> \<Turnstile> x) \<longrightarrow> (\<tau> \<Turnstile> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<Longrightarrow> (\<tau> \<Turnstile> x implies y) = (\<tau> \<Turnstile> x \<longrightarrow> \<tau> \<Turnstile> y)
[PROOF STEP]
apply(simp add: defined_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> x \<triangleq> invalid \<and> \<tau> |\<noteq> x \<triangleq> null \<Longrightarrow> (\<tau> \<Turnstile> x implies y) = (\<tau> \<Turnstile> x \<longrightarrow> \<tau> \<Turnstile> y)
[PROOF STEP]
by(auto simp: OclNot_def OclOr_def OclAnd_def OclImplies_def bot_option_def
              OclValid_def invalid_def true_def null_def StrongEq_def null_fun_def null_option_def
        split:bool.split_asm bool.split option.split_asm)


[STATEMENT]
lemma foundation13:"(\<tau> \<Turnstile> A \<triangleq> true)    = (\<tau> \<Turnstile> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> A \<triangleq> true) = (\<tau> \<Turnstile> A)
[PROOF STEP]
by(auto simp: OclNot_def  OclValid_def invalid_def true_def null_def StrongEq_def
              split:bool.split_asm bool.split)


[STATEMENT]
lemma foundation14:"(\<tau> \<Turnstile> A \<triangleq> false)   = (\<tau> \<Turnstile> not A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> A \<triangleq> false) = (\<tau> \<Turnstile> not A)
[PROOF STEP]
by(auto simp: OclNot_def  OclValid_def invalid_def false_def true_def null_def StrongEq_def
        split:bool.split_asm bool.split option.split)


[STATEMENT]
lemma foundation15:"(\<tau> \<Turnstile> A \<triangleq> invalid) = (\<tau> \<Turnstile> not(\<upsilon> A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> A \<triangleq> invalid) = (\<tau> \<Turnstile> not (\<upsilon> A))
[PROOF STEP]
by(auto simp: OclNot_def OclValid_def valid_def invalid_def false_def true_def null_def
              StrongEq_def bot_option_def null_fun_def null_option_def bot_option_def bot_fun_def
        split:bool.split_asm bool.split option.split)


[STATEMENT]
lemma foundation16: "\<tau> \<Turnstile> (\<delta> X) = (X \<tau> \<noteq> bot \<and> X \<tau> \<noteq> null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> X) = (X \<tau> \<noteq> UML_Types.bot_class.bot \<and> X \<tau> \<noteq> null)
[PROOF STEP]
by(auto simp: OclValid_def defined_def false_def true_def  bot_fun_def null_fun_def
        split:if_split_asm)


[STATEMENT]
lemma foundation16'': "\<not>(\<tau> \<Turnstile> (\<delta> X)) = ((\<tau> \<Turnstile> (X \<triangleq> invalid)) \<or> (\<tau> \<Turnstile> (X \<triangleq> null)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> X) \<noteq> (\<tau> \<Turnstile> X \<triangleq> invalid \<or> \<tau> \<Turnstile> X \<triangleq> null)
[PROOF STEP]
apply(simp add: foundation16)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X \<tau> \<noteq> UML_Types.bot_class.bot \<and> X \<tau> \<noteq> null) = (\<tau> |\<noteq> X \<triangleq> invalid \<and> \<tau> |\<noteq> X \<triangleq> null)
[PROOF STEP]
by(auto simp:defined_def false_def true_def  bot_fun_def null_fun_def OclValid_def StrongEq_def invalid_def)


[STATEMENT]
lemma foundation16': "(\<tau> \<Turnstile> (\<delta> X)) = (X \<tau> \<noteq> invalid \<tau> \<and> X \<tau> \<noteq> null \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> X) = (X \<tau> \<noteq> invalid \<tau> \<and> X \<tau> \<noteq> null \<tau>)
[PROOF STEP]
apply(simp add:invalid_def null_def null_fun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> X) = (X \<tau> \<noteq> UML_Types.bot_class.bot \<and> X \<tau> \<noteq> null)
[PROOF STEP]
by(auto simp: OclValid_def defined_def false_def true_def  bot_fun_def null_fun_def
        split:if_split_asm)


[STATEMENT]
lemma foundation18: "(\<tau> \<Turnstile> (\<upsilon> X)) = (X \<tau> \<noteq> invalid \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<upsilon> X) = (X \<tau> \<noteq> invalid \<tau>)
[PROOF STEP]
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def invalid_def
        split:if_split_asm)


[STATEMENT]
lemma foundation18': "(\<tau> \<Turnstile> (\<upsilon> X)) = (X \<tau> \<noteq> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<upsilon> X) = (X \<tau> \<noteq> UML_Types.bot_class.bot)
[PROOF STEP]
by(auto simp: OclValid_def valid_def false_def true_def bot_fun_def
        split:if_split_asm)


[STATEMENT]
lemma foundation18'': "(\<tau> \<Turnstile> (\<upsilon> X) )=  (\<not>(\<tau> \<Turnstile> (X \<triangleq> invalid)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<upsilon> X) = (\<tau> |\<noteq> X \<triangleq> invalid)
[PROOF STEP]
by(auto simp:foundation15)


[STATEMENT]
lemma foundation20 : "\<tau> \<Turnstile> (\<delta> X) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> X \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> X
[PROOF STEP]
by(simp add: foundation18 foundation16 invalid_def)


[STATEMENT]
lemma foundation21: "(not A \<triangleq> not B) = (A \<triangleq> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (not A \<triangleq> not B) = (A \<triangleq> B)
[PROOF STEP]
by(rule ext, auto simp: OclNot_def StrongEq_def
                     split: bool.split_asm HOL.if_split_asm option.split)


[STATEMENT]
lemma foundation22: "(\<tau> \<Turnstile> (X \<triangleq> Y)) = (X \<tau> = Y \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> X \<triangleq> Y) = (X \<tau> = Y \<tau>)
[PROOF STEP]
by(auto simp: StrongEq_def OclValid_def true_def)


[STATEMENT]
lemma foundation23: "(\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> (\<lambda> _ . P \<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> P) = (\<tau> \<Turnstile> \<lambda>_. P \<tau>)
[PROOF STEP]
by(auto simp: OclValid_def true_def)


[STATEMENT]
lemma foundation24:"(\<tau> \<Turnstile> not(X \<triangleq> Y)) = (X \<tau> \<noteq> Y \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> not (X \<triangleq> Y)) = (X \<tau> \<noteq> Y \<tau>)
[PROOF STEP]
by(simp add: StrongEq_def  OclValid_def OclNot_def true_def)


[STATEMENT]
lemma foundation25: "\<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> (P or Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> P or Q
[PROOF STEP]
by(simp add: OclOr_def OclNot_def OclAnd_def OclValid_def true_def)


[STATEMENT]
lemma foundation25': "\<tau> \<Turnstile> Q \<Longrightarrow> \<tau> \<Turnstile> (P or Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> Q \<Longrightarrow> \<tau> \<Turnstile> P or Q
[PROOF STEP]
by(subst OclOr_commute, simp add: foundation25)


[STATEMENT]
lemma foundation26:
assumes defP: "\<tau> \<Turnstile> \<delta> P"
assumes defQ: "\<tau> \<Turnstile> \<delta> Q"
assumes H: "\<tau> \<Turnstile> (P or Q)"
assumes P: "\<tau> \<Turnstile> P \<Longrightarrow> R"
assumes Q: "\<tau> \<Turnstile> Q \<Longrightarrow> R"
shows "R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R
[PROOF STEP]
by(insert H, subst (asm) foundation11[OF defP defQ], erule disjE, simp_all add: P Q)


[STATEMENT]
lemma foundation27: "\<tau> \<Turnstile> A \<Longrightarrow> (\<tau> \<Turnstile> A implies B) = (\<tau> \<Turnstile> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> A \<Longrightarrow> (\<tau> \<Turnstile> A implies B) = (\<tau> \<Turnstile> B)
[PROOF STEP]
by (simp add: foundation12 foundation6)


[STATEMENT]
lemma defined_not_I : "\<tau> \<Turnstile> \<delta> (x) \<Longrightarrow> \<tau> \<Turnstile> \<delta> (not x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> x \<Longrightarrow> \<tau> \<Turnstile> \<delta> not x
[PROOF STEP]
by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)


[STATEMENT]
lemma valid_not_I : "\<tau> \<Turnstile> \<upsilon> (x) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> (not x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<upsilon> x \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> not x
[PROOF STEP]
by(auto simp: OclNot_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
          split: option.split_asm option.split HOL.if_split_asm)


[STATEMENT]
lemma defined_and_I : "\<tau> \<Turnstile> \<delta> (x) \<Longrightarrow>  \<tau> \<Turnstile> \<delta> (y) \<Longrightarrow> \<tau> \<Turnstile> \<delta> (x and y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; \<tau> \<Turnstile> \<delta> y\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> \<delta> (x and y)
[PROOF STEP]
apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>(\<exists>ya. y \<tau> = \<lfloor>ya\<rfloor>) \<and> y \<tau> \<noteq> \<lfloor>\<bottom>\<rfloor>; \<exists>y. ya = \<lfloor>y\<rfloor>; x \<tau> = \<lfloor>ya\<rfloor>\<rbrakk> \<Longrightarrow> (\<exists>yb. (case ya of \<bottom> \<Rightarrow> case y \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>True\<rfloor> \<Rightarrow> y \<tau> | \<lfloor>False\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>yb\<rfloor>) \<and> (case ya of \<bottom> \<Rightarrow> case y \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>True\<rfloor> \<Rightarrow> y \<tau> | \<lfloor>False\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) \<noteq> \<lfloor>\<bottom>\<rfloor>
[PROOF STEP]
apply(auto simp: null_option_def split: bool.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya yb. \<lbrakk>x \<tau> = \<lfloor>\<lfloor>ya\<rfloor>\<rfloor>; y \<tau> = \<lfloor>\<lfloor>yb\<rfloor>\<rfloor>; (case ya of True \<Rightarrow> y \<tau> | False \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>\<bottom>\<rfloor>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(case_tac "ya",simp_all)


[STATEMENT]
lemma valid_and_I :   "\<tau> \<Turnstile> \<upsilon> (x) \<Longrightarrow>  \<tau> \<Turnstile> \<upsilon> (y) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> (x and y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<upsilon> x; \<tau> \<Turnstile> \<upsilon> y\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> (x and y)
[PROOF STEP]
apply(simp add: OclAnd_def null_def invalid_def defined_def valid_def OclValid_def
                  true_def false_def bot_option_def null_option_def null_fun_def bot_fun_def
             split: option.split_asm HOL.if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ya. \<lbrakk>\<exists>ya. y \<tau> = \<lfloor>ya\<rfloor>; x \<tau> = \<lfloor>ya\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>yb. (case ya of \<bottom> \<Rightarrow> case y \<tau> of \<bottom> \<Rightarrow> \<bottom> | \<lfloor>\<bottom>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<bottom>\<rfloor> | \<lfloor>\<lfloor>False\<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor> | \<lfloor>True\<rfloor> \<Rightarrow> y \<tau> | \<lfloor>False\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>) = \<lfloor>yb\<rfloor>
[PROOF STEP]
by(auto simp: null_option_def split: option.split bool.split)


[STATEMENT]
lemma defined_or_I : "\<tau> \<Turnstile> \<delta> (x) \<Longrightarrow>  \<tau> \<Turnstile> \<delta> (y) \<Longrightarrow> \<tau> \<Turnstile> \<delta> (x or y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<delta> x; \<tau> \<Turnstile> \<delta> y\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> \<delta> (x or y)
[PROOF STEP]
by(simp add: OclOr_def defined_and_I defined_not_I)


[STATEMENT]
lemma valid_or_I :   "\<tau> \<Turnstile> \<upsilon> (x) \<Longrightarrow>  \<tau> \<Turnstile> \<upsilon> (y) \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> (x or y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> \<upsilon> x; \<tau> \<Turnstile> \<upsilon> y\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> \<upsilon> (x or y)
[PROOF STEP]
by(simp add: OclOr_def valid_and_I valid_not_I)


[STATEMENT]
lemma StrongEq_L_refl: "\<tau> \<Turnstile> (x \<triangleq> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> x \<triangleq> x
[PROOF STEP]
by(simp add: OclValid_def StrongEq_def)


[STATEMENT]
lemma StrongEq_L_sym: "\<tau> \<Turnstile> (x \<triangleq> y) \<Longrightarrow> \<tau> \<Turnstile> (y \<triangleq> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> x \<triangleq> y \<Longrightarrow> \<tau> \<Turnstile> y \<triangleq> x
[PROOF STEP]
by(simp add: StrongEq_sym)


[STATEMENT]
lemma StrongEq_L_trans: "\<tau> \<Turnstile> (x \<triangleq> y) \<Longrightarrow> \<tau> \<Turnstile> (y \<triangleq> z) \<Longrightarrow> \<tau> \<Turnstile> (x \<triangleq> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> x \<triangleq> y; \<tau> \<Turnstile> y \<triangleq> z\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> x \<triangleq> z
[PROOF STEP]
by(simp add: OclValid_def StrongEq_def true_def)


[STATEMENT]
lemma StrongEq_L_subst1: "\<And> \<tau>. cp P \<Longrightarrow> \<tau> \<Turnstile> (x \<triangleq> y) \<Longrightarrow> \<tau> \<Turnstile> (P x \<triangleq> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>cp P; \<tau> \<Turnstile> x \<triangleq> y\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> P x \<triangleq> P y
[PROOF STEP]
by(auto simp: OclValid_def StrongEq_def true_def cp_def)


[STATEMENT]
lemma StrongEq_L_subst2:
"\<And> \<tau>.  cp P \<Longrightarrow> \<tau> \<Turnstile> (x \<triangleq> y) \<Longrightarrow> \<tau> \<Turnstile> (P x) \<Longrightarrow> \<tau> \<Turnstile> (P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrakk>cp P; \<tau> \<Turnstile> x \<triangleq> y; \<tau> \<Turnstile> P x\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> P y
[PROOF STEP]
by(auto simp: OclValid_def StrongEq_def true_def cp_def)


[STATEMENT]
lemma StrongEq_L_subst2_rev: "\<tau> \<Turnstile> y \<triangleq> x \<Longrightarrow> cp P \<Longrightarrow> \<tau> \<Turnstile> P x \<Longrightarrow> \<tau> \<Turnstile> P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> y \<triangleq> x; cp P; \<tau> \<Turnstile> P x\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> P y
[PROOF STEP]
apply(erule StrongEq_L_subst2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<tau> \<Turnstile> y \<triangleq> x; \<tau> \<Turnstile> P x\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> ?x \<triangleq> y
 2. \<lbrakk>\<tau> \<Turnstile> y \<triangleq> x; \<tau> \<Turnstile> P x\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> P ?x
[PROOF STEP]
apply(erule StrongEq_L_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau> \<Turnstile> y \<triangleq> x; \<tau> \<Turnstile> P x\<rbrakk> \<Longrightarrow> \<tau> \<Turnstile> P x
[PROOF STEP]
by assumption


[STATEMENT]
lemma  StrongEq_L_subst3:
assumes cp: "cp P"
and     eq: "\<tau> \<Turnstile> (x \<triangleq> y)"
shows       "(\<tau> \<Turnstile> P x) = (\<tau> \<Turnstile> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> P x) = (\<tau> \<Turnstile> P y)
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<tau> \<Turnstile> P x \<Longrightarrow> \<tau> \<Turnstile> P y
 2. \<tau> \<Turnstile> P y \<Longrightarrow> \<tau> \<Turnstile> P x
[PROOF STEP]
apply(rule StrongEq_L_subst2[OF cp,OF eq],simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P y \<Longrightarrow> \<tau> \<Turnstile> P x
[PROOF STEP]
apply(rule StrongEq_L_subst2[OF cp,OF eq[THEN StrongEq_L_sym]],simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  StrongEq_L_subst3_rev:
assumes eq: "\<tau> \<Turnstile> (x \<triangleq> y)"
and     cp: "cp P"
shows       "(\<tau> \<Turnstile> P x) = (\<tau> \<Turnstile> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> P x) = (\<tau> \<Turnstile> P y)
[PROOF STEP]
by(insert cp, erule StrongEq_L_subst3, rule eq)


[STATEMENT]
lemma  StrongEq_L_subst4_rev:
assumes eq: "\<tau> \<Turnstile> (x \<triangleq> y)"
and     cp: "cp P"
shows       "(\<not>(\<tau> \<Turnstile> P x)) = (\<not>(\<tau> \<Turnstile> P y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> |\<noteq> P x) = (\<tau> |\<noteq> P y)
[PROOF STEP]
thm arg_cong[of _ _ "Not"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> |\<noteq> P x) = (\<tau> |\<noteq> P y)
[PROOF STEP]
apply(rule arg_cong[of _ _ "Not"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> P x) = (\<tau> \<Turnstile> P y)
[PROOF STEP]
by(insert cp, erule StrongEq_L_subst3, rule eq)


[STATEMENT]
lemma cpI1:
"(\<forall> X \<tau>. f X \<tau> = f(\<lambda>_. X \<tau>) \<tau>) \<Longrightarrow> cp P \<Longrightarrow> cp(\<lambda>X. f (P X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>X \<tau>. f X \<tau> = f (\<lambda>_. X \<tau>) \<tau>; cp P\<rbrakk> \<Longrightarrow> cp (\<lambda>X. f (P X))
[PROOF STEP]
apply(auto simp: true_def cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>\<forall>X a b. f X (a, b) = f (\<lambda>_. X (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> \<exists>fa. \<forall>X a b. f (P X) (a, b) = fa (X (a, b)) (a, b)
[PROOF STEP]
apply(rule exI, (rule allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa X a b. \<lbrakk>\<forall>X a b. f X (a, b) = f (\<lambda>_. X (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> f (P X) (a, b) = ?f1 fa (X (a, b)) (a, b)
[PROOF STEP]
by(erule_tac x="P X" in allE, auto)


[STATEMENT]
lemma cpI2:
"(\<forall> X Y \<tau>. f X Y \<tau> = f(\<lambda>_. X \<tau>)(\<lambda>_. Y \<tau>) \<tau>) \<Longrightarrow>
 cp P \<Longrightarrow> cp Q \<Longrightarrow> cp(\<lambda>X. f (P X) (Q X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>X Y \<tau>. f X Y \<tau> = f (\<lambda>_. X \<tau>) (\<lambda>_. Y \<tau>) \<tau>; cp P; cp Q\<rbrakk> \<Longrightarrow> cp (\<lambda>X. f (P X) (Q X))
[PROOF STEP]
apply(auto simp: true_def cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa. \<lbrakk>\<forall>X Y a b. f X Y (a, b) = f (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> \<exists>fa. \<forall>X a b. f (P X) (Q X) (a, b) = fa (X (a, b)) (a, b)
[PROOF STEP]
apply(rule exI, (rule allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa X a b. \<lbrakk>\<forall>X Y a b. f X Y (a, b) = f (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> f (P X) (Q X) (a, b) = ?f2 fa faa (X (a, b)) (a, b)
[PROOF STEP]
by(erule_tac x="P X" in allE, auto)


[STATEMENT]
lemma cpI3:
"(\<forall> X Y Z \<tau>. f X Y Z \<tau> = f(\<lambda>_. X \<tau>)(\<lambda>_. Y \<tau>)(\<lambda>_. Z \<tau>) \<tau>) \<Longrightarrow>
 cp P \<Longrightarrow> cp Q \<Longrightarrow> cp R \<Longrightarrow> cp(\<lambda>X. f (P X) (Q X) (R X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>X Y Z \<tau>. f X Y Z \<tau> = f (\<lambda>_. X \<tau>) (\<lambda>_. Y \<tau>) (\<lambda>_. Z \<tau>) \<tau>; cp P; cp Q; cp R\<rbrakk> \<Longrightarrow> cp (\<lambda>X. f (P X) (Q X) (R X))
[PROOF STEP]
apply(auto simp: cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb. \<lbrakk>\<forall>X Y Z a b. f X Y Z (a, b) = f (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fb (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> \<exists>fa. \<forall>X a b. f (P X) (Q X) (R X) (a, b) = fa (X (a, b)) (a, b)
[PROOF STEP]
apply(rule exI, (rule allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb X a b. \<lbrakk>\<forall>X Y Z a b. f X Y Z (a, b) = f (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fb (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> f (P X) (Q X) (R X) (a, b) = ?f3 fa faa fb (X (a, b)) (a, b)
[PROOF STEP]
by(erule_tac x="P X" in allE, auto)


[STATEMENT]
lemma cpI4:
"(\<forall> W X Y Z \<tau>. f W X Y Z \<tau> = f(\<lambda>_. W \<tau>)(\<lambda>_. X \<tau>)(\<lambda>_. Y \<tau>)(\<lambda>_. Z \<tau>) \<tau>) \<Longrightarrow>
 cp P \<Longrightarrow> cp Q \<Longrightarrow> cp R \<Longrightarrow> cp S \<Longrightarrow> cp(\<lambda>X. f (P X) (Q X) (R X) (S X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>W X Y Z \<tau>. f W X Y Z \<tau> = f (\<lambda>_. W \<tau>) (\<lambda>_. X \<tau>) (\<lambda>_. Y \<tau>) (\<lambda>_. Z \<tau>) \<tau>; cp P; cp Q; cp R; cp S\<rbrakk> \<Longrightarrow> cp (\<lambda>X. f (P X) (Q X) (R X) (S X))
[PROOF STEP]
apply(auto simp: cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb fc. \<lbrakk>\<forall>W X Y Z a b. f W X Y Z (a, b) = f (\<lambda>_. W (a, b)) (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fb (X (a, b)) (a, b); \<forall>X a b. S X (a, b) = fc (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> \<exists>fa. \<forall>X a b. f (P X) (Q X) (R X) (S X) (a, b) = fa (X (a, b)) (a, b)
[PROOF STEP]
apply(rule exI, (rule allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb fc X a b. \<lbrakk>\<forall>W X Y Z a b. f W X Y Z (a, b) = f (\<lambda>_. W (a, b)) (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. P X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fb (X (a, b)) (a, b); \<forall>X a b. S X (a, b) = fc (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> f (P X) (Q X) (R X) (S X) (a, b) = ?f4 fa faa fb fc (X (a, b)) (a, b)
[PROOF STEP]
by(erule_tac x="P X" in allE, auto)


[STATEMENT]
lemma cpI5:
"(\<forall> V W X Y Z \<tau>. f V W X Y Z \<tau> = f(\<lambda>_. V \<tau>) (\<lambda>_. W \<tau>)(\<lambda>_. X \<tau>)(\<lambda>_. Y \<tau>)(\<lambda>_. Z \<tau>) \<tau>) \<Longrightarrow>
 cp N \<Longrightarrow> cp P \<Longrightarrow> cp Q \<Longrightarrow> cp R \<Longrightarrow> cp S \<Longrightarrow> cp(\<lambda>X. f (N X) (P X) (Q X) (R X) (S X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>V W X Y Z \<tau>. f V W X Y Z \<tau> = f (\<lambda>_. V \<tau>) (\<lambda>_. W \<tau>) (\<lambda>_. X \<tau>) (\<lambda>_. Y \<tau>) (\<lambda>_. Z \<tau>) \<tau>; cp N; cp P; cp Q; cp R; cp S\<rbrakk> \<Longrightarrow> cp (\<lambda>X. f (N X) (P X) (Q X) (R X) (S X))
[PROOF STEP]
apply(auto simp: cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb fc fd. \<lbrakk>\<forall>V W X Y Z a b. f V W X Y Z (a, b) = f (\<lambda>_. V (a, b)) (\<lambda>_. W (a, b)) (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. N X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. P X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = fb (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fc (X (a, b)) (a, b); \<forall>X a b. S X (a, b) = fd (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> \<exists>fa. \<forall>X a b. f (N X) (P X) (Q X) (R X) (S X) (a, b) = fa (X (a, b)) (a, b)
[PROOF STEP]
apply(rule exI, (rule allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fa faa fb fc fd X a b. \<lbrakk>\<forall>V W X Y Z a b. f V W X Y Z (a, b) = f (\<lambda>_. V (a, b)) (\<lambda>_. W (a, b)) (\<lambda>_. X (a, b)) (\<lambda>_. Y (a, b)) (\<lambda>_. Z (a, b)) (a, b); \<forall>X a b. N X (a, b) = fa (X (a, b)) (a, b); \<forall>X a b. P X (a, b) = faa (X (a, b)) (a, b); \<forall>X a b. Q X (a, b) = fb (X (a, b)) (a, b); \<forall>X a b. R X (a, b) = fc (X (a, b)) (a, b); \<forall>X a b. S X (a, b) = fd (X (a, b)) (a, b)\<rbrakk> \<Longrightarrow> f (N X) (P X) (Q X) (R X) (S X) (a, b) = ?f5 fa faa fb fc fd (X (a, b)) (a, b)
[PROOF STEP]
by(erule_tac x="N X" in allE, auto)


[STATEMENT]
lemma cp_const : "cp(\<lambda>_. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cp (\<lambda>_. c)
[PROOF STEP]
by (simp add: cp_def, fast)


[STATEMENT]
lemma cp_id :     "cp(\<lambda>X. X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cp (\<lambda>X. X)
[PROOF STEP]
by (simp add: cp_def, fast)


[STATEMENT]
lemma cp_OclIf:"((if C then B\<^sub>1 else B\<^sub>2 endif) \<tau> =
                  (if (\<lambda> _. C \<tau>) then (\<lambda> _. B\<^sub>1 \<tau>) else (\<lambda> _. B\<^sub>2 \<tau>) endif) \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if C then B\<^sub>1 else B\<^sub>2 endif) \<tau> = (if (\<lambda>_. C \<tau>) then (\<lambda>_. B\<^sub>1 \<tau>) else (\<lambda>_. B\<^sub>2 \<tau>) endif) \<tau>
[PROOF STEP]
by(simp only: OclIf_def, subst cp_defined, rule refl)


[STATEMENT]
lemma OclIf_invalid [simp]: "(if invalid then B\<^sub>1 else B\<^sub>2 endif) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if invalid then B\<^sub>1 else B\<^sub>2 endif) = invalid
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclIf_null [simp]: "(if null then B\<^sub>1 else B\<^sub>2 endif) = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if null then B\<^sub>1 else B\<^sub>2 endif) = invalid
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclIf_true [simp]: "(if true then B\<^sub>1 else B\<^sub>2 endif) = B\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if true then B\<^sub>1 else B\<^sub>2 endif) = B\<^sub>1
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclIf_true' [simp]: "\<tau> \<Turnstile> P \<Longrightarrow> (if P then B\<^sub>1 else B\<^sub>2 endif)\<tau> = B\<^sub>1 \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P \<Longrightarrow> (if P then B\<^sub>1 else B\<^sub>2 endif) \<tau> = B\<^sub>1 \<tau>
[PROOF STEP]
apply(subst cp_OclIf,auto simp: OclValid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tau> = true \<tau> \<Longrightarrow> (if (\<lambda>_. true \<tau>) then (\<lambda>_. B\<^sub>1 \<tau>) else (\<lambda>_. B\<^sub>2 \<tau>) endif) \<tau> = B\<^sub>1 \<tau>
[PROOF STEP]
by(simp add:cp_OclIf[symmetric])


[STATEMENT]
lemma OclIf_true'' [simp]: "\<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> (if P then B\<^sub>1 else B\<^sub>2 endif) \<triangleq> B\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> P \<Longrightarrow> \<tau> \<Turnstile> if P then B\<^sub>1 else B\<^sub>2 endif \<triangleq> B\<^sub>1
[PROOF STEP]
by(subst OclValid_def, simp add: StrongEq_def true_def)


[STATEMENT]
lemma OclIf_false [simp]: "(if false then B\<^sub>1 else B\<^sub>2 endif) = B\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if false then B\<^sub>1 else B\<^sub>2 endif) = B\<^sub>2
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclIf_false' [simp]: "\<tau> \<Turnstile> not P \<Longrightarrow> (if P then B\<^sub>1 else B\<^sub>2 endif)\<tau> = B\<^sub>2 \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not P \<Longrightarrow> (if P then B\<^sub>1 else B\<^sub>2 endif) \<tau> = B\<^sub>2 \<tau>
[PROOF STEP]
apply(subst cp_OclIf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not P \<Longrightarrow> (if (\<lambda>_. P \<tau>) then (\<lambda>_. B\<^sub>1 \<tau>) else (\<lambda>_. B\<^sub>2 \<tau>) endif) \<tau> = B\<^sub>2 \<tau>
[PROOF STEP]
apply(auto simp: foundation14[symmetric] foundation22)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tau> = false \<tau> \<Longrightarrow> (if (\<lambda>_. false \<tau>) then (\<lambda>_. B\<^sub>1 \<tau>) else (\<lambda>_. B\<^sub>2 \<tau>) endif) \<tau> = B\<^sub>2 \<tau>
[PROOF STEP]
by(auto simp: cp_OclIf[symmetric])


[STATEMENT]
lemma OclIf_idem1[simp]:"(if \<delta> X then A else A endif) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<delta> X then A else A endif) = A
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclIf_idem2[simp]:"(if \<upsilon> X then A else A endif) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<upsilon> X then A else A endif) = A
[PROOF STEP]
by(rule ext, auto simp: OclIf_def)


[STATEMENT]
lemma OclNot_if[simp]:
"not(if P then C else E endif) = (if P then not C else not E endif)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (if P then C else E endif) = (if P then not C else not E endif)
[PROOF STEP]
(* non-trivial but elementary *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not (if P then C else E endif) = (if P then not C else not E endif)
[PROOF STEP]
apply(rule OclNot_inject, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if P then C else E endif) = not (if P then not C else not E endif)
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (if P then C else E endif) x = not (if P then not C else not E endif) x
[PROOF STEP]
apply(subst cp_OclNot, simp add: OclIf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (P x = true x \<longrightarrow> ((\<delta> P) x = true x \<longrightarrow> C x = not (\<lambda>_. not C x) x) \<and> ((\<delta> P) x \<noteq> true x \<longrightarrow> invalid x = not (\<lambda>_. invalid x) x)) \<and> (P x \<noteq> true x \<longrightarrow> ((\<delta> P) x = true x \<longrightarrow> E x = not (\<lambda>_. not E x) x) \<and> ((\<delta> P) x \<noteq> true x \<longrightarrow> invalid x = not (\<lambda>_. invalid x) x))
[PROOF STEP]
apply(subst cp_OclNot[symmetric])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (P x = true x \<longrightarrow> ((\<delta> P) x = true x \<longrightarrow> C x = not (not C) x) \<and> ((\<delta> P) x \<noteq> true x \<longrightarrow> invalid x = not invalid x)) \<and> (P x \<noteq> true x \<longrightarrow> ((\<delta> P) x = true x \<longrightarrow> E x = not (not E) x) \<and> ((\<delta> P) x \<noteq> true x \<longrightarrow> invalid x = not invalid x))
[PROOF STEP]
by simp


[STATEMENT]
lemma OclNot_defargs:
"\<tau> \<Turnstile> (not P) \<Longrightarrow> \<tau> \<Turnstile> \<delta> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not P \<Longrightarrow> \<tau> \<Turnstile> \<delta> P
[PROOF STEP]
by(auto simp: OclNot_def OclValid_def true_def invalid_def defined_def false_def
                 bot_fun_def bot_option_def null_fun_def null_option_def
        split: bool.split_asm HOL.if_split_asm option.split option.split_asm)


[STATEMENT]
lemma OclNot_contrapos_nn:
 assumes A: "\<tau> \<Turnstile> \<delta> A"
 assumes B: "\<tau> \<Turnstile> not B"
 assumes C: "\<tau> \<Turnstile> A \<Longrightarrow> \<tau> \<Turnstile> B"
 shows      "\<tau> \<Turnstile> not A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not A
[PROOF STEP]
have D : "\<tau> \<Turnstile> \<delta> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> \<delta> B
[PROOF STEP]
by(rule B[THEN OclNot_defargs])
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> \<delta> B

goal (1 subgoal):
 1. \<tau> \<Turnstile> not A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<Turnstile> not A
[PROOF STEP]
apply(insert B,simp add: A D foundation9)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> |\<noteq> B \<Longrightarrow> \<tau> |\<noteq> A
[PROOF STEP]
by(erule contrapos_nn, auto intro: C)
[PROOF STATE]
proof (state)
this:
\<tau> \<Turnstile> not A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma const_charn: "const X \<Longrightarrow> X \<tau> = X \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const X \<Longrightarrow> X \<tau> = X \<tau>'
[PROOF STEP]
by(auto simp: const_def)


[STATEMENT]
lemma const_subst:
 assumes const_X: "const X"
     and const_Y: "const Y"
     and eq :     "X \<tau> = Y \<tau>"
     and cp_P:    "cp P"
     and pp :     "P Y \<tau> = P Y \<tau>'"
   shows "P X \<tau> = P X \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
have A: "\<And>Y. P Y \<tau> = P (\<lambda>_. Y \<tau>) \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. P Y \<tau> = P (\<lambda>_. Y \<tau>) \<tau>
[PROOF STEP]
apply(insert cp_P, unfold cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. \<exists>f. \<forall>X \<tau>. P X \<tau> = f (X \<tau>) \<tau> \<Longrightarrow> P Y \<tau> = P (\<lambda>_. Y \<tau>) \<tau>
[PROOF STEP]
apply(elim exE, erule_tac x=Y in allE', erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y f. \<lbrakk>\<forall>x \<tau>. P x \<tau> = f (x \<tau>) \<tau>; P Y \<tau> = f (Y \<tau>) \<tau>\<rbrakk> \<Longrightarrow> P Y \<tau> = P (\<lambda>_. Y \<tau>) \<tau>
[PROOF STEP]
apply(erule_tac x="(\<lambda>_. Y \<tau>)" in allE, erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y f. \<lbrakk>P Y \<tau> = f (Y \<tau>) \<tau>; P (\<lambda>_. Y \<tau>) \<tau> = f (Y \<tau>) \<tau>\<rbrakk> \<Longrightarrow> P Y \<tau> = P (\<lambda>_. Y \<tau>) \<tau>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P ?Y \<tau> = P (\<lambda>_. ?Y \<tau>) \<tau>

goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
have B: "\<And>Y. P Y \<tau>' = P (\<lambda>_. Y \<tau>') \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. P Y \<tau>' = P (\<lambda>_. Y \<tau>') \<tau>'
[PROOF STEP]
apply(insert cp_P, unfold cp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. \<exists>f. \<forall>X \<tau>. P X \<tau> = f (X \<tau>) \<tau> \<Longrightarrow> P Y \<tau>' = P (\<lambda>_. Y \<tau>') \<tau>'
[PROOF STEP]
apply(elim exE, erule_tac x=Y in allE', erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y f. \<lbrakk>\<forall>x \<tau>. P x \<tau> = f (x \<tau>) \<tau>; P Y \<tau>' = f (Y \<tau>') \<tau>'\<rbrakk> \<Longrightarrow> P Y \<tau>' = P (\<lambda>_. Y \<tau>') \<tau>'
[PROOF STEP]
apply(erule_tac x="(\<lambda>_. Y \<tau>')" in allE, erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y f. \<lbrakk>P Y \<tau>' = f (Y \<tau>') \<tau>'; P (\<lambda>_. Y \<tau>') \<tau>' = f (Y \<tau>') \<tau>'\<rbrakk> \<Longrightarrow> P Y \<tau>' = P (\<lambda>_. Y \<tau>') \<tau>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P ?Y \<tau>' = P (\<lambda>_. ?Y \<tau>') \<tau>'

goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
have C: "X \<tau>' = Y \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<tau>' = Y \<tau>'
[PROOF STEP]
apply(rule trans, subst const_charn[OF const_X],rule eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<tau> = Y \<tau>'
[PROOF STEP]
by(rule const_charn[OF const_Y])
[PROOF STATE]
proof (state)
this:
X \<tau>' = Y \<tau>'

goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P X \<tau> = P X \<tau>'
[PROOF STEP]
apply(subst A, subst B, simp add: eq C)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (\<lambda>_. Y \<tau>) \<tau> = P (\<lambda>_. Y \<tau>') \<tau>'
[PROOF STEP]
apply(subst A[symmetric],subst B[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Y \<tau> = P Y \<tau>'
[PROOF STEP]
by(simp add:pp)
[PROOF STATE]
proof (state)
this:
P X \<tau> = P X \<tau>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma const_imply2 :
 assumes "\<And>\<tau> \<tau>'. P \<tau> = P \<tau>' \<Longrightarrow> Q \<tau> = Q \<tau>'"
 shows "const P \<Longrightarrow> const Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const P \<Longrightarrow> const Q
[PROOF STEP]
by(simp add: const_def, insert assms, blast)


[STATEMENT]
lemma const_imply3 :
 assumes "\<And>\<tau> \<tau>'. P \<tau> = P \<tau>' \<Longrightarrow> Q \<tau> = Q \<tau>' \<Longrightarrow> R \<tau> = R \<tau>'"
 shows "const P \<Longrightarrow> const Q \<Longrightarrow> const R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const P; const Q\<rbrakk> \<Longrightarrow> const R
[PROOF STEP]
by(simp add: const_def, insert assms, blast)


[STATEMENT]
lemma const_imply4 :
 assumes "\<And>\<tau> \<tau>'. P \<tau> = P \<tau>' \<Longrightarrow> Q \<tau> = Q \<tau>' \<Longrightarrow> R \<tau> = R \<tau>' \<Longrightarrow> S \<tau> = S \<tau>'"
 shows "const P \<Longrightarrow> const Q \<Longrightarrow> const R \<Longrightarrow> const S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const P; const Q; const R\<rbrakk> \<Longrightarrow> const S
[PROOF STEP]
by(simp add: const_def, insert assms, blast)


[STATEMENT]
lemma const_lam : "const (\<lambda>_. e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (\<lambda>_. e)
[PROOF STEP]
by(simp add: const_def)


[STATEMENT]
lemma const_true[simp] : "const true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const true
[PROOF STEP]
by(simp add: const_def true_def)


[STATEMENT]
lemma const_false[simp] : "const false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const false
[PROOF STEP]
by(simp add: const_def false_def)


[STATEMENT]
lemma const_null[simp] : "const null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const null
[PROOF STEP]
by(simp add: const_def null_fun_def)


[STATEMENT]
lemma const_invalid [simp]: "const invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const invalid
[PROOF STEP]
by(simp add: const_def invalid_def)


[STATEMENT]
lemma const_bot[simp] : "const bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const UML_Types.bot_class.bot
[PROOF STEP]
by(simp add: const_def bot_fun_def)


[STATEMENT]
lemma const_defined :
 assumes "const X"
 shows   "const (\<delta> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (\<delta> X)
[PROOF STEP]
by(rule const_imply2[OF _ assms],
   simp add: defined_def false_def true_def bot_fun_def bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma const_valid :
 assumes "const X"
 shows   "const (\<upsilon> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (\<upsilon> X)
[PROOF STEP]
by(rule const_imply2[OF _ assms],
   simp add: valid_def false_def true_def bot_fun_def null_fun_def assms)


[STATEMENT]
lemma const_OclAnd :
  assumes "const X"
  assumes "const X'"
  shows   "const (X and X')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (X and X')
[PROOF STEP]
by(rule const_imply3[OF _ assms], subst (1 2) cp_OclAnd, simp add: assms OclAnd_def)


[STATEMENT]
lemma const_OclNot :
    assumes "const X"
    shows   "const (not X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (not X)
[PROOF STEP]
by(rule const_imply2[OF _ assms],subst cp_OclNot,simp add: assms OclNot_def)


[STATEMENT]
lemma const_OclOr :
  assumes "const X"
  assumes "const X'"
  shows   "const (X or X')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (X or X')
[PROOF STEP]
by(simp add: assms OclOr_def const_OclNot const_OclAnd)


[STATEMENT]
lemma const_OclImplies :
  assumes "const X"
  assumes "const X'"
  shows   "const (X implies X')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (X implies X')
[PROOF STEP]
by(simp add: assms OclImplies_def const_OclNot const_OclOr)


[STATEMENT]
lemma const_StrongEq:
  assumes "const X"
  assumes "const X'"
  shows   "const(X \<triangleq> X')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (X \<triangleq> X')
[PROOF STEP]
apply(simp only: StrongEq_def const_def, intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lfloor>\<lfloor>X \<tau> = X' \<tau>\<rfloor>\<rfloor> = \<lfloor>\<lfloor>X \<tau>' = X' \<tau>'\<rfloor>\<rfloor>
[PROOF STEP]
apply(subst assms(1)[THEN const_charn])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lfloor>\<lfloor>X (?\<tau>'2 \<tau> \<tau>') = X' \<tau>\<rfloor>\<rfloor> = \<lfloor>\<lfloor>X \<tau>' = X' \<tau>'\<rfloor>\<rfloor>
[PROOF STEP]
apply(subst assms(2)[THEN const_charn])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lfloor>\<lfloor>X (?\<tau>''4 \<tau> \<tau> \<tau>' \<tau>') = X' (?\<tau>'3 \<tau> \<tau>')\<rfloor>\<rfloor> = \<lfloor>\<lfloor>X \<tau>' = X' \<tau>'\<rfloor>\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma const_OclIf :
  assumes "const B"
      and "const C1"
      and "const C2"
    shows "const (if B then C1 else C2 endif)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const (if B then C1 else C2 endif)
[PROOF STEP]
apply(rule const_imply4[OF _ assms],
       subst (1 2) cp_OclIf, simp only: OclIf_def cp_defined[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>B \<tau> = B \<tau>'; C1 \<tau> = C1 \<tau>'; C2 \<tau> = C2 \<tau>'\<rbrakk> \<Longrightarrow> (if (\<delta> (\<lambda>_. B \<tau>')) \<tau> = true \<tau> then if B \<tau>' = true \<tau> then C1 \<tau>' else C2 \<tau>' else invalid \<tau>) = (if (\<delta> B) \<tau>' = true \<tau>' then if B \<tau>' = true \<tau>' then C1 \<tau>' else C2 \<tau>' else invalid \<tau>')
[PROOF STEP]
apply(simp add: const_defined[OF assms(1), simplified const_def, THEN spec, THEN spec]
                 const_true[simplified const_def, THEN spec, THEN spec]
                 assms[simplified const_def, THEN spec, THEN spec]
                 const_invalid[simplified const_def, THEN spec, THEN spec])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. (B \<tau>' = true \<tau> \<longrightarrow> ((\<delta> (\<lambda>_. true \<tau>')) \<tau> = true \<tau> \<longrightarrow> (\<delta> B) \<tau>' \<noteq> true \<tau>' \<longrightarrow> C1 \<tau>' = invalid \<tau>') \<and> ((\<delta> (\<lambda>_. true \<tau>')) \<tau> \<noteq> true \<tau> \<longrightarrow> (\<delta> B) \<tau>' = true \<tau>' \<longrightarrow> invalid \<tau> = C1 \<tau>')) \<and> (B \<tau>' \<noteq> true \<tau> \<longrightarrow> (B \<tau>' = true \<tau>' \<longrightarrow> ((\<delta> (\<lambda>_. true \<tau>')) \<tau> = true \<tau> \<longrightarrow> (\<delta> B) \<tau>' \<noteq> true \<tau>' \<longrightarrow> C1 \<tau>' = invalid \<tau>') \<and> ((\<delta> (\<lambda>_. true \<tau>')) \<tau> \<noteq> true \<tau> \<longrightarrow> (\<delta> B) \<tau>' = true \<tau>' \<longrightarrow> invalid \<tau> = C1 \<tau>')) \<and> (B \<tau>' \<noteq> true \<tau>' \<longrightarrow> ((\<delta> (\<lambda>_. B \<tau>')) \<tau> = true \<tau> \<longrightarrow> (\<delta> B) \<tau>' \<noteq> true \<tau>' \<longrightarrow> C2 \<tau>' = invalid \<tau>') \<and> ((\<delta> (\<lambda>_. B \<tau>')) \<tau> \<noteq> true \<tau> \<longrightarrow> (\<delta> B) \<tau>' = true \<tau>' \<longrightarrow> invalid \<tau> = C2 \<tau>')))
[PROOF STEP]
by (metis (no_types) bot_fun_def OclValid_def const_def const_true defined_def
                 foundation16[THEN iffD1]  null_fun_def)


[STATEMENT]
lemma const_OclValid1:
 assumes "const x"
 shows   "(\<tau> \<Turnstile> \<delta> x) = (\<tau>' \<Turnstile> \<delta> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<delta> x) = (\<tau>' \<Turnstile> \<delta> x)
[PROOF STEP]
apply(simp add: OclValid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<delta> x) \<tau> = true \<tau>) = ((\<delta> x) \<tau>' = true \<tau>')
[PROOF STEP]
apply(subst const_defined[OF assms, THEN const_charn])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<delta> x) ?\<tau>' = true \<tau>) = ((\<delta> x) \<tau>' = true \<tau>')
[PROOF STEP]
by(simp add: true_def)


[STATEMENT]
lemma const_OclValid2:
 assumes "const x"
 shows   "(\<tau> \<Turnstile> \<upsilon> x) = (\<tau>' \<Turnstile> \<upsilon> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> \<Turnstile> \<upsilon> x) = (\<tau>' \<Turnstile> \<upsilon> x)
[PROOF STEP]
apply(simp add: OclValid_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<upsilon> x) \<tau> = true \<tau>) = ((\<upsilon> x) \<tau>' = true \<tau>')
[PROOF STEP]
apply(subst const_valid[OF assms, THEN const_charn])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<upsilon> x) ?\<tau>' = true \<tau>) = ((\<upsilon> x) \<tau>' = true \<tau>')
[PROOF STEP]
by(simp add: true_def)


[STATEMENT]
lemma const_HOL_if : "const C \<Longrightarrow> const D \<Longrightarrow> const F \<Longrightarrow> const (\<lambda>\<tau>. if C \<tau> then D \<tau> else F \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const C; const D; const F\<rbrakk> \<Longrightarrow> const (\<lambda>\<tau>. if C \<tau> then D \<tau> else F \<tau>)
[PROOF STEP]
by(auto simp: const_def)


[STATEMENT]
lemma const_HOL_and: "const C \<Longrightarrow> const D \<Longrightarrow> const (\<lambda>\<tau>. C \<tau> \<and> D \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const C; const D\<rbrakk> \<Longrightarrow> const (\<lambda>\<tau>. C \<tau> \<and> D \<tau>)
[PROOF STEP]
by(auto simp: const_def)


[STATEMENT]
lemma const_HOL_eq : "const C \<Longrightarrow> const D \<Longrightarrow> const (\<lambda>\<tau>. C \<tau> = D \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const C; const D\<rbrakk> \<Longrightarrow> const (\<lambda>\<tau>. C \<tau> = D \<tau>)
[PROOF STEP]
apply(auto simp: const_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau> = D \<tau>\<rbrakk> \<Longrightarrow> C \<tau>' = D \<tau>'
 2. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau> = D \<tau>; \<forall>\<tau>'. C \<tau> = C \<tau>'\<rbrakk> \<Longrightarrow> C \<tau>' = D \<tau>'
 2. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau> = D \<tau>; \<forall>\<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau>'. D \<tau> = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau>' = D \<tau>'
 2. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau> = D \<tau>; \<forall>\<tau>'. D \<tau> = D \<tau>'; C \<tau> = C \<tau>'\<rbrakk> \<Longrightarrow> C \<tau>' = D \<tau>'
 2. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau> = D \<tau>; C \<tau> = C \<tau>'; D \<tau> = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau>' = D \<tau>'
 2. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>\<forall>\<tau> \<tau>'. D \<tau> = D \<tau>'; C \<tau>' = D \<tau>'; \<forall>\<tau>'. C \<tau> = C \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau> in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau>' = D \<tau>'; \<forall>\<tau>'. C \<tau> = C \<tau>'; \<forall>\<tau>'. D \<tau> = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau>' = D \<tau>'; \<forall>\<tau>'. D \<tau> = D \<tau>'; C \<tau> = C \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
apply(erule_tac x=\<tau>' in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau> \<tau>'. \<lbrakk>C \<tau>' = D \<tau>'; C \<tau> = C \<tau>'; D \<tau> = D \<tau>'\<rbrakk> \<Longrightarrow> C \<tau> = D \<tau>
[PROOF STEP]
by simp


[STATEMENT]
lemma vec_to_iarray_exists:
shows "(\<exists>b. A $ b \<noteq> 0) = IArray.exists (\<lambda>b. (vec_to_iarray A) !! b \<noteq> 0) (IArray[0..<IArray.length (vec_to_iarray A)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>b. A $ b \<noteq> (0::'b)) = IArray.exists (\<lambda>b. vec_to_iarray A !! b \<noteq> (0::'b)) (IArray [0..<IArray.length (vec_to_iarray A)])
[PROOF STEP]
proof (unfold IArray.exists_def length_vec_to_iarray, auto simp del: IArray.sub_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. A $ b \<noteq> (0::'b) \<Longrightarrow> \<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> (0::'b)
 2. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. A $ b \<noteq> (0::'b) \<Longrightarrow> \<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> (0::'b)
 2. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
assume Ab: "A $ b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
A $ b \<noteq> (0::'b)

goal (2 subgoals):
 1. \<And>b. A $ b \<noteq> (0::'b) \<Longrightarrow> \<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> (0::'b)
 2. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
show "\<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> (0::'b)
[PROOF STEP]
by (rule bexI[of _ "to_nat b"], unfold vec_to_iarray_nth', auto simp add: Ab to_nat_less_card[of b])
[PROOF STATE]
proof (state)
this:
\<exists>b\<in>{0..<CARD('a)}. vec_to_iarray A !! b \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
assume b: "b < CARD('a)" and Ab_vec: "vec_to_iarray A !! b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
b < CARD('a)
vec_to_iarray A !! b \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>b. \<lbrakk>b < CARD('a); vec_to_iarray A !! b \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
show "\<exists>b. A $ b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b. A $ b \<noteq> (0::'b)
[PROOF STEP]
by (rule exI[of _ "from_nat b"], metis Ab_vec vec_to_iarray_nth[OF b])
[PROOF STATE]
proof (state)
this:
\<exists>b. A $ b \<noteq> (0::'b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_is_zero_iarray_eq_iff: "(\<exists>b. A $ b \<noteq> 0) = (\<not> is_zero_iarray (vec_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>b. A $ b \<noteq> (0::'b)) = (\<not> is_zero_iarray (vec_to_iarray A))
[PROOF STEP]
by (metis (full_types) is_zero_iarray_eq_iff vec_eq_iff zero_index)