theory Finalise_DR

lemma zip_map_eqv:
  "(y, x) \<in> set (zip (map g xs) (map f xs)) = (\<exists>t. (y = g t \<and> x = f t \<and> t \<in> set xs))" apply (clarsimp simp:zip_map1 zip_map2) apply (rule iffI) apply (fastforce simp: in_set_zip) apply (clarsimp simp:set_zip_same) using imageI[where f ="(\<lambda>(a, b). (a, f b)) \<circ> (\<lambda>(x, y). (g x, y))",simplified] apply clarify apply (drule_tac x = t in meta_spec) apply (drule_tac x = t in meta_spec) apply (drule_tac x = "Id \<inter> (set xs) \<times> (set xs) " in meta_spec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((y, x) \<in> set (zip (map g xs) (map f xs))) = (\<exists>t. y = g t \<and> x = f t \<and> t \<in> set xs) proof (prove)
goal (1 subgoal):
 1. ((y, x) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` set (zip xs xs)) = (\<exists>t. y = g t \<and> x = f t \<and> t \<in> set xs) proof (prove)
goal (2 subgoals):
 1. (y, x) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` set (zip xs xs) \<Longrightarrow> \<exists>t. y = g t \<and> x = f t \<and> t \<in> set xs
 2. \<exists>t. y = g t \<and> x = f t \<and> t \<in> set xs \<Longrightarrow> (y, x) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` set (zip xs xs) proof (prove)
goal (1 subgoal):
 1. \<exists>t. y = g t \<and> x = f t \<and> t \<in> set xs \<Longrightarrow> (y, x) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` set (zip xs xs) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
using this:
?x \<in> ?A \<Longrightarrow> (case case ?x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) ` ?A

goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t; \<And>a b A. (a, b) \<in> A \<Longrightarrow> (g a, f b) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) ` A\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t; \<And>b A. (t, b) \<in> A \<Longrightarrow> (g t, f b) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) ` A\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t; \<And>A. (t, t) \<in> A \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) ` A\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>y = g t; t \<in> set xs; x = f t; (t, t) \<in> Restr Id (set xs) \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (a, b) \<Rightarrow> (a, f b)) ` Restr Id (set xs)\<rbrakk> \<Longrightarrow> (g t, f t) \<in> (\<lambda>x. case case x of (x, xa) \<Rightarrow> (g x, xa) of (x, y) \<Rightarrow> (x, f y)) ` Restr Id (set xs) proof (prove)
goal:
No subgoals!