[STATEMENT]
lemma modelAppendTautologicalFormula:
fixes
  F :: Formula and F' :: Formula
assumes
  "model valuation F" "\<forall> c. c el F' \<longrightarrow> clauseTautology c"
  "vars valuation \<supseteq> vars F \<union> vars F'"
shows
  "model valuation (F @ F')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. model valuation (F @ F')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
model valuation F
\<forall>c. c el F' \<longrightarrow> clauseTautology c
vars F \<union> vars F' \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ F')
[PROOF STEP]
proof (induct F')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>model valuation F; \<forall>c. c el [] \<longrightarrow> clauseTautology c; vars F \<union> vars [] \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ [])
 2. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
model valuation F
\<forall>c. c el [] \<longrightarrow> clauseTautology c
vars F \<union> vars [] \<subseteq> vars valuation

goal (2 subgoals):
 1. \<lbrakk>model valuation F; \<forall>c. c el [] \<longrightarrow> clauseTautology c; vars F \<union> vars [] \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ [])
 2. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
model valuation F
\<forall>c. c el [] \<longrightarrow> clauseTautology c
vars F \<union> vars [] \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation (F @ [])

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
case (Cons c F'')
[PROOF STATE]
proof (state)
this:
\<lbrakk>model valuation F; \<forall>c. c el F'' \<longrightarrow> clauseTautology c; vars F \<union> vars F'' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'')
model valuation F
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
hence "model valuation (F @ F'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>model valuation F; \<forall>c. c el F'' \<longrightarrow> clauseTautology c; vars F \<union> vars F'' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'')
model valuation F
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation (F @ F'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation (F @ F'')

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
hence "model valuation ((F @ F'') @ [c])"
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using Cons(3)
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using Cons(4)
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using modelAppendTautology[of "valuation" "F @ F''" "c"]
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation
\<lbrakk>model valuation (F @ F''); clauseTautology c; vars (F @ F'') \<union> vars c \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
using varsAppendFormulae[of "F" "F''"]
[PROOF STATE]
proof (prove)
using this:
model valuation (F @ F'')
\<forall>ca. ca el c # F'' \<longrightarrow> clauseTautology ca
vars F \<union> vars (c # F'') \<subseteq> vars valuation
\<lbrakk>model valuation (F @ F''); clauseTautology c; vars (F @ F'') \<union> vars c \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation ((F @ F'') @ [c])
vars (F @ F'') = vars F \<union> vars F''

goal (1 subgoal):
 1. model valuation ((F @ F'') @ [c])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. \<And>a F'. \<lbrakk>\<lbrakk>model valuation F; \<forall>c. c el F' \<longrightarrow> clauseTautology c; vars F \<union> vars F' \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ F'); model valuation F; \<forall>c. c el a # F' \<longrightarrow> clauseTautology c; vars F \<union> vars (a # F') \<subseteq> vars valuation\<rbrakk> \<Longrightarrow> model valuation (F @ a # F')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
model valuation ((F @ F'') @ [c])

goal (1 subgoal):
 1. model valuation (F @ c # F'')
[PROOF STEP]
by (simp add: formulaTrueAppend)
[PROOF STATE]
proof (state)
this:
model valuation (F @ c # F'')

goal:
No subgoals!
[PROOF STEP]
qed