theory Lib

lemma wf_sum_wf:
  "\<lbrakk> wf r; wf r' \<rbrakk> \<Longrightarrow> wf (wf_sum divisor r r')" apply (simp add: wf_sum_def) apply (rule wf_Un)+ apply (erule wf_Int2) apply (rule wf_subset
             [where r="measure (\<lambda>x. If (divisor x) 1 0)"]) apply simp apply clarsimp apply blast apply (erule wf_Int2) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf (wf_sum divisor r r') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y} \<union> {x. divisor x} \<times> {y. divisor y} \<inter> r) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r')
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. \<not> divisor x} \<times> {y. divisor y})
 3. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r') \<inter> Range ({x. \<not> divisor x} \<times> {y. divisor y}) = {}
 4. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 5. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. \<not> divisor x} \<times> {y. divisor y})
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r') \<inter> Range ({x. \<not> divisor x} \<times> {y. divisor y}) = {}
 3. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 4. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>x. if divisor x then 1 else 0))
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> {x. \<not> divisor x} \<times> {y. divisor y} \<subseteq> measure (\<lambda>x. if divisor x then 1 else 0)
 3. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r') \<inter> Range ({x. \<not> divisor x} \<times> {y. divisor y}) = {}
 4. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 5. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> {x. \<not> divisor x} \<times> {y. divisor y} \<subseteq> measure (\<lambda>x. if divisor x then 1 else 0)
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r') \<inter> Range ({x. \<not> divisor x} \<times> {y. divisor y}) = {}
 3. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 4. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r') \<inter> Range ({x. \<not> divisor x} \<times> {y. divisor y}) = {}
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 3. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> wf ({x. divisor x} \<times> {y. divisor y} \<inter> r)
 2. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf r; wf r'\<rbrakk> \<Longrightarrow> Domain ({x. \<not> divisor x} \<times> {y. \<not> divisor y} \<inter> r' \<union> {x. \<not> divisor x} \<times> {y. divisor y}) \<inter> Range ({x. divisor x} \<times> {y. divisor y} \<inter> r) = {} proof (prove)
goal:
No subgoals!