theory HaskellLemmaBucket

lemma not_orList_is_replicate:
  "\<not> orList ls \<Longrightarrow> ls = replicate (length ls) False" proof (induct ls rule: rev_induct) case Nil thus ?case unfolding orList_def by simp next case (snoc l ls) from snoc.prems have ol: "\<not> orList ls" and nl: "\<not> l" unfolding orList_def by auto have "ls = replicate (length ls) False" by (rule snoc.hyps [OF ol]) thus ?case by (rule ssubst) (simp add: nl replicate_app_Cons_same [where xs = "[]", simplified]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> orList ls \<Longrightarrow> ls = replicate (length ls) False proof (state)
goal (2 subgoals):
 1. \<not> orList [] \<Longrightarrow> [] = replicate (length []) False
 2. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (state)
this:
\<not> orList []

goal (2 subgoals):
 1. \<not> orList [] \<Longrightarrow> [] = replicate (length []) False
 2. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (prove)
using this:
\<not> orList []

goal (1 subgoal):
 1. [] = replicate (length []) False proof (prove)
using this:
\<not> foldl (\<or>) False []

goal (1 subgoal):
 1. [] = replicate (length []) False proof (state)
this:
[] = replicate (length []) False

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (state)
this:
\<not> orList ls \<Longrightarrow> ls = replicate (length ls) False
\<not> orList (ls @ [l])

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (chain)
picking this:
\<not> orList (ls @ [l]) proof (prove)
using this:
\<not> orList (ls @ [l])

goal (1 subgoal):
 1. \<not> orList ls &&& \<not> l proof (prove)
using this:
\<not> foldl (\<or>) False (ls @ [l])

goal (1 subgoal):
 1. \<not> foldl (\<or>) False ls &&& \<not> l proof (state)
this:
\<not> orList ls
\<not> l

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (prove)
goal (1 subgoal):
 1. ls = replicate (length ls) False proof (state)
this:
ls = replicate (length ls) False

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<not> orList xs \<Longrightarrow> xs = replicate (length xs) False; \<not> orList (xs @ [x])\<rbrakk> \<Longrightarrow> xs @ [x] = replicate (length (xs @ [x])) False proof (prove)
using this:
ls = replicate (length ls) False

goal (1 subgoal):
 1. ls @ [l] = replicate (length (ls @ [l])) False proof (state)
this:
ls @ [l] = replicate (length (ls @ [l])) False

goal:
No subgoals!