theory Lists imports Main begin

consts
map :: "('a => 'u) => 'a list => 'u list"
in_list :: "'a => 'a list => bool"
unit_list:: "'a => 'a list => bool"
car :: "'a list => 'a"
cdr :: "'a list => 'a list"
zip :: "'a list => 'r list => ('a \<times> 'r) list"

primrec
"map r [] = []"
"map r (x#z) = (r x)#(map r z)"

primrec
"in_list x [] = False"
"in_list x (y#z) = ((x = y) \<or> (in_list x z))"

primrec
"unit_list x [] = True"
"unit_list x (y#z) = ((x = y) \<and> (unit_list x z))"

primrec
"car (e#b) = e"

primrec
"cdr [] = []"
"cdr (e#b) = b"

primrec
"zip [] b' = []"
"zip (e#b) b' = (if b' = [] then [] else (e,car b')#(zip b (cdr b')))"


text {* map *}

lemma map_not_empty_lemma: "b ~= [] ==> map f b ~= []";
apply (case_tac b);
apply (auto);
done;

lemma map_form_lemma: "map f (e#b) = (f e)#(map f b)";
apply (auto);
done;

lemma map_length_lemma: "length b = length (map x b)";
apply (induct_tac b);
apply (force);
apply (auto);
done;


text {* if x is in (map f b), there is a e with f e = x *}

lemma in_list_main_reform: "(in_list (x::'a) (map f b)) --> (? (e::'z). f e = x)";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_map_form_reform: "(in_list (x::'a) (map f b)) --> (? (e::'z). in_list e b & f e = x)";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_map_form_lemma: "\<forall> (x::'a). (in_list r (map f b)) --> (?(e::'z). in_list e b & f e = r)";
apply (insert in_list_map_form_reform [of _ f b]);
apply (auto);
done;

lemma in_list_form_lemma: "(in_list e b & f e = r) --> (in_list r (map f b))";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_main_lemma: "(?(e::'z). in_list e b & f e = r) ==> (in_list r (map f b))";
apply (frule someI_ex);
apply (insert in_list_form_lemma [of _ b f]);
apply (auto);
done;

lemma in_list_or_lemma: "in_list x (e#b) ==> x = e | in_list x b";
apply (auto);
done;

lemma in_list_reform: "in_list (e::'z) b --> in_list (f e) (map f b)";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_lemma: "~(in_list e b) ==> \<forall> (e'::'a). in_list e' b --> e' ~= e";
apply (auto);
done;

lemma in_list_rex_lemma: "in_list e b ==> \<exists> (e'::'a). in_list e' b & e' = e";
apply (auto);
done;

lemma in_list_rex_e_lemma: "\<forall> (e::'a). ~(in_list e b) \<or>  e ~= e' ==> ~(in_list e' b)";
apply (auto);
done;

lemma in_list_map_rex_lemma: "[|in_list e b; f e = r|] ==> in_list r (map f b)";
apply (insert in_list_reform [of e b]);
apply (auto);
done;

lemma in_list_map_fail_lemma: "[|in_list e b; ~(in_list Fail (map f b))|] ==> f e ~= Fail";
apply (frule in_list_lemma [of Fail "map f b"]);
apply (insert in_list_map_rex_lemma [of e b f Fail]);
apply (auto);
done;

lemma in_list_map_cjn_lemma: "(in_list (r::'z) (map f b)) --> (? (e::'a). in_list e b \<and> f e = r)";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_map_lemma: "in_list e' (map f b) --> (?(e::'a). in_list e b & e' = f e)";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_map_reform: "\<forall> (e'::'z). in_list e' (map f b) --> (?(e::'a). in_list e b & e' = f e)";
apply (insert in_list_map_lemma [of _ f b]);
apply (auto);
done;

lemma cjn_map_lemma: "\<forall> (e::'a). in_list e b --> f e ~= Fail ==> ~(in_list Fail (map f b))";
apply (insert in_list_map_cjn_lemma [of Fail f b]);
apply (auto);
done;

lemma in_list_main_or_lemma: "in_list e b --> in_list e (b@b')";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_not_empty_lemma: "in_list e (b@[e])";
apply (induct_tac b);
apply (auto);
done;

lemma in_list_not_empty_or_lemma: "in_list e' (b@[e]) & e ~= e' --> in_list e' b";
apply (induct_tac b);
apply (auto);
done;


text {* if for all e, f applied to b not fails, Fail is not in (map f b) *}

lemma in_list_map_expr_lemma: "(\<forall> (e::'a). f e ~= Fail) ==> ~(in_list Fail (map f b))";
apply (insert in_list_main_reform [of Fail f b]);
apply (auto);
done;

lemma gr_cjn_map_lemma: "(\<forall> (e::'a). in_list e b --> f e ~= Fail) ==> ~(in_list Fail (map f b))";
apply (insert in_list_map_cjn_lemma [of Fail f b]);
apply (auto);
done;


text {* map, in_list, zip *}

lemma map_empty_case: "map f [] = map f' []";
apply (auto);
done;

lemma map_not_empty_case: "[|\<forall> (x::'a). in_list x (e#b) --> f x = f' x; map f b = map f' b|] ==> map f (e#b) = map f' (e#b)";
apply (auto);
done;

lemma map_lemma: "(\<forall> (x::'a). in_list x b --> f x = f' x) --> map f b = map f' b";
apply (induct_tac b);
apply (auto);
done;

lemma zip_in_list_empty_or_case: "in_list (x,x') (zip b []) ==> in_list x b";
apply (case_tac b);
apply (auto);
done;

lemma in_list_zip_map_lemma: "[|in_list x (e#b); in_list x b --> in_list (x, f x) ( zip b (map f b))|] ==> in_list (x, f x) (zip (e#b) (map f (e#b)))";
apply (frule in_list_or_lemma [of x e b]);
apply (auto);
done;

lemma main_zip_map_lemma: "in_list x b --> in_list (x, f x) (zip b (map f b))";
apply (induct_tac b);
apply (insert in_list_zip_map_lemma);
apply (auto);
done;

lemma zip_map_in_list_lemma: "in_list e' (map f b) --> (?(x::'a). in_list (x, e') (zip b (map f b)))";
apply (induct_tac b);
apply (auto);
done;

lemma zip_map_in_list_reform: "\<forall> (e'::'z). in_list e' (map f b) --> (?(x::'a). in_list (x, e') (zip b (map f b)))";
apply (insert zip_map_in_list_lemma [of _ f b]);
apply (auto);
done;

lemma zip_map_in_listr_case: "[|in_list (x,x') (zip (e#b) (map f (e#b))); in_list (x,x') (zip b (map f b)) --> x' = f x|] ==> x' = f x"
apply (auto);
done;

lemma zip_map_or_lemma: "in_list (x,x') (zip b (map f b)) --> f x = x'";
apply (induct_tac b);
apply (insert main_zip_map_lemma);
apply (auto);
done;

lemma zip_map_or_reform: "in_list (x,x') (zip b (map f b)) ==> x' = f x";
apply (insert zip_map_or_lemma [of x x' b f]);
apply (auto);
done;

lemma zip_map_or_main_reform: "in_list (x,x') (zip b (map f b)) ==> in_list (x,f x) (zip b (map f b))";
apply (insert zip_map_or_lemma [of x x' b f]);
apply (auto);
done;

lemma in_list_zip_main_or_lemma: "\<forall> (x::'a). in_list x b --> (?(e'::'z). in_list (x, e') (zip b (map f b)) & f x = e')";
apply (insert main_zip_map_lemma [of _ b f]);
apply (auto);
done;

lemma map_form_main_lemma: "in_list e' (map f b) --> (?(x::'a). in_list (x, e') (zip b (map f b)) & f x = e')";
apply (insert zip_map_in_list_reform [of f b]);
apply (insert zip_map_or_reform [of _ e' b f]);
apply (auto);
done;

lemma map_reform: "\<forall> (e'::'z). in_list e' (map f b) --> (?(x::'a). in_list (x, e') (zip b (map f b)) & f x = e')";
apply (insert map_form_main_lemma [of _ f b]);
apply (auto);
done;

lemma in_list_zip_main_or_reform: "\<forall> (x::'a). in_list x b --> (?(e'::'z). in_list (x, e') (zip b (map f b)) & f x = e')";
apply (insert main_zip_map_lemma [of _ b f]);
apply (auto);
done;


text {* unit_list *}

lemma in_unit_list_map_lemma: "[|e = e'; unit_list x (map f e)|] ==> unit_list x (map f e')";
apply (auto);
done;

lemma unit_list_lemma: "[|b ~= []; unit_list x b|] ==> in_list x b";
apply (case_tac b);
apply (auto);
done;

lemma unit_list_main_lemma: "(\<forall> (x::'a). in_list x b --> f x = x') --> unit_list x' (map f b)";
apply (induct_tac b);
apply (auto);
done;

lemma unit_list_main_or_lemma: "~(unit_list x b) ==> ~(unit_list x (x'#b))";
apply (auto);
done;

lemma unit_list_aim_lemma: "(in_list x b & f x ~= e) --> ~(unit_list e (map f b))";
apply (induct_tac b);
apply (auto);
done;


text {* list/set mediation *}

lemma in_list_congr_lemma: "in_list e b --> e \<in> set b";
apply (induct_tac b);
apply (auto);
done;


end