theory PPL_Summer_School_2017
imports Main
begin
(** Pure logic **)
lemma name: "\P. P \ P"
proof-
fix P
assume 1: "P"
show "P" by (rule 1)
qed
lemma name2:
fixes P :: "bool" shows "P \ P"
proof-
assume 1: "P"
show "P" by (rule 1)
qed
lemma name3:
fixes P assumes 1: "P" shows "P"
by (rule 1)
lemma mp_Pure:
"\ P Q. P \ ((P \ Q) \ Q)"
proof-
fix P Q
assume 1: "P"
assume 2: "P \ Q"
show "Q"
by (rule 2, rule 1) (* blah *)
qed
lemma mp_Pure2:
fixes P Q
assumes 1: "P"
assumes 2: "P \ Q"
shows "Q"
by (rule 2, rule 1)
(** HOL logic **)
term "True"
term "False"
term "\ x"
term "x \ y"
term "x \ y"
term "\x :: nat. P x \ \ P x"
lemma True_HOL: "True" by (rule TrueI)
lemma "\ False"
find_theorems "(_ \ False) \ \ _"
by (rule notI)
lemma "\p. p \ p"
find_theorems "(\_. _) \ \_. _"
by (intro allI impI)
lemma "\p q. p \ (p \ q) \ q"
proof (intro allI impI)
fix p q
assume 1: "p"
assume 2: "p \ q"
have 3: "p \ q"
using 2 by (elim impE)
show "q"
by (rule 3, rule 1)
qed
(** Definition **)
term my_True
definition my_True where "my_True = True"
term my_True
lemma "my_True = True"
by (rule my_True_def)
lemma "my_True"
unfolding my_True_def by (rule TrueI)
definition my_id where "my_id x = x"
thm my_id_def
lemma "my_id (my_id x) = x"
unfolding my_id_def by (rule refl)
lemma "my_id (my_id x) = x"
by (simp add: my_id_def)
declare my_id_def[simp]
lemma "my_id (my_id x) = x" by simp
definition my_id2 where "my_id2 = (\x. x)"
declare my_id2_def[simp]
lemma "my_id = my_id2"
apply (rule ext) by simp
lemma "my_id = my_id2"
by auto
term "[]"
term "x#xs"
term "[1::int, 2, 3, 4]!2"
value "[1::int, 2, 3, 4]!6"
(** Insert sort **)
definition my_sorted
where "my_sorted xs = (\ i j. i < j \ j < length xs \ \ xs!i > xs!j)"
lemma my_sortedI [intro]:
fixes xs
assumes 1: "\ i j. i < j \ j < length xs \ \ xs!i > xs!j"
shows "my_sorted xs"
unfolding my_sorted_def
using 1 by auto
lemma my_sortedD [dest]:
fixes xs
assumes 1: "my_sorted xs"
shows "\i j. i < j \ j < length xs \ \ xs ! i > xs ! j"
using 1
unfolding my_sorted_def
by auto
lemma my_sortedE [elim]:
fixes xs
assumes 1: "my_sorted xs"
assumes 2: "(\i j. i < j \ j < length xs \ \ xs ! i > xs ! j) \ P"
shows "P"
using 1 2 unfolding my_sorted_def by auto
fun my_insert
where "my_insert x [] = [x]"
| "my_insert x (y#ys) = (if x \ y then x # y # ys else y # my_insert x ys)"
fun my_sort
where "my_sort [] = []"
| "my_sort (x#xs) = my_insert x (my_sort xs)"
value "my_sort [4::int,3,5,1]"
term "set xs"
lemma my_sorted_Cons':
assumes 1: "my_sorted xs"
assumes 2: "\y. y \ set xs \ \x > y"
shows "my_sorted (x#xs)"
proof (rule my_sortedI)
fix i j :: "nat"
assume 3: "i < j"
assume 4: "j < length (x#xs)"
show "\(x # xs) ! j < (x # xs) ! i"
proof (cases i)
case 0
then show ?thesis using 1 2 3 4 by auto
next
case (Suc nat)
then show ?thesis using 1 2 3 4 by auto
qed
qed
lemma my_sorted_Cons [simp]:
"my_sorted (x#xs) \ my_sorted xs \ (\y \ set xs. \ x > y)"
(is "?l \ ?r") (* to avoid copy&paste *)
proof (intro iffI)
assume 1: "?r"
show "?l"
using 1 by (intro my_sorted_Cons', auto)
next
assume 1: "?l"
show "?r"
proof (intro conjI)
show "my_sorted xs"
apply (intro my_sortedI)
using "1" sorted_nth_monoI by auto
next
show "\y\set xs. \ x > y"
proof (intro ballI)
fix y
assume 2: "y \ set xs"
obtain i where 3: "xs ! i = y" and 4: "i < length xs"
by (meson "2" in_set_conv_nth)
show "~ x > y"
using 1 2 3 4 by auto
qed
qed
qed
lemma set_my_insert[simp]:
"set (my_insert x xs) = set xs \ {x}"
by (induct xs, auto)
lemma my_sorted_my_insert [intro]:
fixes xs :: "('a :: preorder) list"
assumes 1: "my_sorted xs"
shows "my_sorted (my_insert x xs)"
using 1
by (induct xs, auto simp add: less_le_not_le dest: order_trans)
theorem my_sorted_my_sort:
fixes xs :: "'a :: preorder list"
shows "my_sorted (my_sort xs)"
by (induct xs, auto)
corollary
fixes xs :: "int list"
shows "my_sorted (my_sort xs)"
by (rule my_sorted_my_sort)
export_code my_sort in OCaml
definition my_sort_integer ::
"integer list \ integer list"
where "my_sort_integer = my_sort"
export_code my_sort_integer in OCaml
value "my_sort [CHR ''f'', CHR ''a'', CHR ''b'']"
instantiation char :: ord
begin
definition less_eq_char where
"less_eq_char a b = (nat_of_char a \ nat_of_char b)"
definition less_char where
"less_char a b = (nat_of_char a < nat_of_char b)"
instance by (intro_classes)
end
value "my_sort [CHR ''f'', CHR ''a'', CHR ''b'']"
declare less_eq_char_def [simp]
declare less_char_def [simp]
instance char :: linorder
by (intro_classes, auto)
corollary
fixes xs :: "char list"
shows "my_sorted (my_sort xs)"
by (rule my_sorted_my_sort)
end