Basic.ML

Pretty.setmargin 105;
goals_limit:=1;


goal thy "n = Suc m --> 0 < n";
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "Suc_imp_0_less";


goal thy
"!a. length a = length c --> length b = length d --> zip (a@b) (c@d) = zip a c @ zip b d";
by (induct_tac "c" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (deepen_tac (claset() addDs [Suc_imp_0_less] addss (simpset() addsimps [zero_less_Suc])) 1 1);
qed_spec_mp "zip_append";


goal thy
"!i. length (xs[i:=x]) = length xs";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
qed "length_lupdate";


goal thy
"!xs. length xs = length ys --> zip (rev xs) (rev ys) = rev (zip xs ys)";
by (induct_tac "ys" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (deepen_tac (claset() addDs [Suc_imp_0_less] addss (simpset() 
	addsimps [neq_Nil_conv,zip_append])) 1 1);
qed_spec_mp "zip_rev";


goal thy
"(x : set (replicate n v)) --> (x=v)";
by (case_tac "n=0" 1);
by (Asm_simp_tac  1);
by (Asm_simp_tac  1);
qed_spec_mp "in_set_replicate";


goal thy
"!i v. x:set (xs[i:=v]) --> x=v |  x:set xs";
by (induct_tac "xs" 1);
 by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
by (Fast_tac  1);
qed_spec_mp "in_set_list_update_disj";


goal thy
"!i x y xs. length xs = length ys --> (zip (xs[i:=x]) (ys[i:=y])) = ((zip xs ys)[i:=(x,y)])";
by (induct_tac "ys" 1);
 by (Simp_tac 1);
by (deepen_tac (claset() addDs [Suc_imp_0_less] addss (simpset() addsplits [nat.split] addsimps [neq_Nil_conv])) 0 1);
qed_spec_mp "zip_list_update";

 
goal thy
"((x#xs) ! i) = (case i of 0 => x | (Suc k) => (xs!k))";
by (simp_tac (simpset() addsplits [nat.split] addsimps []) 1);
qed "nth_Cons";


goal thy
"!i. i < length xs --> (xs ! i) : set xs";
by (induct_tac "xs" 1);
 by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsplits [nat.split] addsimps [nth_Cons]) 1);
qed_spec_mp "nth_in_set_list";


goal thy
"(!i. i < length xs --> P (xs ! i)) --> (!x:set xs. P x)";
by (induct_tac "xs" 1);
 by (asm_full_simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsplits [nat.split] addsimps [nth_Cons]) 1);
by (deepen_tac (claset() addss (simpset())) 0 1);
qed_spec_mp "all_nth_imp_set_list";


goal thy
"(!x:set xs. P x) = (!i. i<length xs --> P (xs!i))";
br iffI 1;
 by (asm_full_simp_tac (simpset() addsimps [nth_in_set_list]) 1);
be all_nth_imp_set_list 1;
qed_spec_mp "set_list_all_nth_conv";