Up to index of Isabelle/HOL/PMC
theory Prelude = Main:(*
Author: Wolfram Kahl, 2003
(Some rtrancl lemmas have been moved here from theories
originally authored by Rene Vestergaard and James Brotherston.)
*)
header {* Prelude *}
theory Prelude = Main:
lemma imp_curry: "(A & B \<longrightarrow> C) = (A \<longrightarrow> B \<longrightarrow> C)"
by blast
lemma subset_lemma_3:
"\<lbrakk> A Int B = {}; C <= A Un {x}; x ~: B \<rbrakk> \<Longrightarrow> C Int B = {}"
by blast
theorem rtrancl_left_inclusion:
"(s, t) : R^* \<Longrightarrow> (s, t) : (R Un T)^*"
apply (erule rtrancl_induct)
apply (rule rtrancl_refl)
apply (rotate_tac 1)
apply (drule_tac B=T in UnI1)
apply (erule rtrancl_into_rtrancl, assumption)
done
theorem rtrancl_right_inclusion:
"(s, t) : R^* \<Longrightarrow> (s, t) : (T Un R)^*"
apply (erule rtrancl_induct)
apply (rule rtrancl_refl)
apply (rotate_tac 1)
apply (drule_tac A=T in UnI2)
apply (erule rtrancl_into_rtrancl, assumption)
done
lemma rtrancl_Int_Vec:
"(!! x y . (x,y) : A \<Longrightarrow> P x \<Longrightarrow> P y) \<Longrightarrow>
A^* Int {(x,y) . P x} <= (A Int {(x,y) . P x})^*"
apply (rule subsetI)
apply (tactic "split_all_tac 1")
apply simp
apply (erule conjE)
apply (erule rtrancl_induct)
apply simp
apply simp
apply (erule rtrancl_into_rtrancl)
apply simp
apply (erule rtrancl_induct)
apply assumption
apply auto
done
lemma drop_length_0:
"ALL k . k \<le> length xs \<longrightarrow> length (drop k xs) = length xs - k"
by (induct_tac xs, auto)
lemma drop_length:
"k \<le> length xs \<Longrightarrow> k + length (drop k xs) = length xs"
by (induct_tac xs, auto)
lemma minus_leq:
"ALL c . a + b <= (c :: nat) \<longrightarrow> b <= c - a"
by (induct_tac "a", auto, arith)
lemma take_plus:
"take (m+n) xs = take m xs @ take n (drop m xs)"
apply (subgoal_tac "take m (take (m + n) xs) @ drop m (take (m + n) xs) = take m xs @ take n (drop m xs)")
apply (cut_tac n=m and xs="take (m+n) xs" in append_take_drop_id)
apply (rotate_tac -1, drule sym)
apply simp
apply (subst take_take)
apply (subgoal_tac "min m (m + n) = m")
prefer 2
apply arith
apply simp
apply (thin_tac "min m (m + n) = m")
apply (rule sym)
apply (subgoal_tac "m + n = n + m")
prefer 2
apply arith
apply (simp (no_asm_simp))
apply (rule take_drop)
done
lemma set_drop_0: "ALL xs . set (drop k xs) <= set xs"
by (induct_tac k, auto, case_tac xs, auto)
lemma set_drop: "set (drop k xs) <= set xs"
by (cut_tac k=k in set_drop_0, auto)
lemma set_take_0: "ALL xs . set (take k xs) <= set xs"
by (induct_tac k, auto, case_tac xs, auto)
lemma set_take: "set (take k xs) <= set xs"
by (cut_tac k=k in set_take_0, auto)
lemma mem_cat[simp]:
"x mem xs @ ys = (x mem xs | x mem ys)"
by (induct_tac xs, auto)
lemma mem_rev[simp]:
"x mem rev ys = x mem ys"
by (induct_tac ys, auto)
lemma mem_set:
"(x : set xs) = x mem xs"
by (induct_tac xs, auto)
lemma set_rev[simp]:
"set (rev ys) = set ys"
by (induct_tac ys, auto)
lemma all_list_induct_1:
"ALL x. x mem y # ys --> P x ==> (ALL x. x mem ys --> P x) & P y"
by (simp add: set_mem_eq)
lemma zip_take2_len1_0:
"ALL ys . zip xs (take (length xs) ys) = zip xs ys"
apply (induct_tac xs, tactic "ALLGOALS strip_tac", auto)
apply (case_tac ys, auto)
done
lemma zip_take2_len1[simp]:
"zip xs (take (length xs) ys) = zip xs ys"
by (insert zip_take2_len1_0, auto)
lemma zip_take1_len2_0:
"ALL ys . zip (take (length xs) ys) xs = zip ys xs"
apply (induct_tac xs, tactic "ALLGOALS strip_tac", auto)
apply (case_tac ys, auto)
done
lemma zip_take1_len2[simp]:
"zip (take (length xs) ys) xs = zip ys xs"
by (insert zip_take1_len2_0, auto)
lemma map_fst_zip[simp]:
"ALL ys . map fst (zip xs ys) = take (length ys) xs"
apply (induct_tac xs, tactic "ALLGOALS strip_tac", simp_all)
apply (case_tac ys)
apply simp
apply (drule_tac x=lista in spec)
apply auto
done
lemma map_snd_zip[simp]:
"ALL ys . map snd (zip ys xs) = take (length ys) xs"
apply (induct_tac xs, tactic "ALLGOALS strip_tac", simp_all)
apply (case_tac ys)
apply simp
apply (drule_tac x=lista in spec)
apply auto
done
end
lemma imp_curry:
(A & B --> C) = (A --> B --> C)
lemma subset_lemma_3:
[| A Int B = {}; C <= A Un {x}; x ~: B |] ==> C Int B = {}
theorem rtrancl_left_inclusion:
(s, t) : R^* ==> (s, t) : (R Un T)^*
theorem rtrancl_right_inclusion:
(s, t) : R^* ==> (s, t) : (T Un R)^*
lemma rtrancl_Int_Vec:
(!!x y. [| (x, y) : A; P x |] ==> P y)
==> A^* Int {(x, y). P x} <= (A Int {(x, y). P x})^*
lemma drop_length_0:
ALL k. k <= length xs --> length (drop k xs) = length xs - k
lemma drop_length:
k <= length xs ==> k + length (drop k xs) = length xs
lemma minus_leq:
ALL c. a + b <= c --> b <= c - a
lemma take_plus:
take (m + n) xs = take m xs @ take n (drop m xs)
lemma set_drop_0:
ALL xs. set (drop k xs) <= set xs
lemma set_drop:
set (drop k xs) <= set xs
lemma set_take_0:
ALL xs. set (take k xs) <= set xs
lemma set_take:
set (take k xs) <= set xs
lemma mem_cat:
x mem xs @ ys = (x mem xs | x mem ys)
lemma mem_rev:
x mem rev ys = x mem ys
lemma mem_set:
(x : set xs) = x mem xs
lemma set_rev:
set (rev ys) = set ys
lemma all_list_induct_1:
ALL x. x mem y # ys --> P x ==> (ALL x. x mem ys --> P x) & P y
lemma zip_take2_len1_0:
ALL ys. zip xs (take (length xs) ys) = zip xs ys
lemma zip_take2_len1:
zip xs (take (length xs) ys) = zip xs ys
lemma zip_take1_len2_0:
ALL ys. zip (take (length xs) ys) xs = zip ys xs
lemma zip_take1_len2:
zip (take (length xs) ys) xs = zip ys xs
lemma map_fst_zip:
ALL ys. map fst (zip xs ys) = take (length ys) xs
lemma map_snd_zip:
ALL ys. map snd (zip ys xs) = take (length ys) xs