theory Demo = Main:

(*** Beispiele zur Simplifikation ***)

lemma "[] @ xs = xs"
apply simp
done
(* Keine Annahmen: *)
lemma "ys @ [] = []"
apply(simp)
oops (* abandon proof *);

(* Einfache Annahmen: *)
lemma "xs = [] ==> xs @ ys = ys @ xs @ ys"
apply(simp)
oops;

(* Vereinfachung in Annahmen: *)
lemma "[| xs @ zs = ys @ xs; [] @ xs = [] @ [] |] ==> ys = zs"
apply(simp)
done;

(* Annahmen koennen zur Nichtterminierung fuehren.
   U.u. (no_asm) noetig *)
lemma "ALL x. f x = g(f(g(x))) ==> f [] = f [] @ []";
(*
apply(simp)
   sondern so: *)
apply(simp (no_asm))
done;

(* Wenn man zusaetzliche Regeln braucht: *)
lemma "map (\<lambda>x. x+1) (rev xs) = rev(map (\<lambda>x. x+1) xs)"
thm rev_map
apply(simp add: rev_map)
done;

(* Wenn man Regeln abschalten muss: *)

lemma stupid_lemma [simp]: "x+y = x+y+(0::nat)"
apply(simp)
done;

lemma "x+y+z = y+z+(x::nat)"
(* So nicht:
apply(simp)
   sondern so: *)
apply(simp del: stupid_lemma)
done;

(* Wenn man Lemmas global an/abschalten will: *)
declare stupid_lemma[simp]
declare stupid_lemma[simp del]

lemma "x+y+z = y+z+(x::nat)"
apply(simp)
done;



(** Definitionen **)

constdefs
 exor :: "bool => bool => bool"
"exor x y == x & y | ~x & ~y"
 nand :: "bool => bool => bool"
"nand x y == ~(x & y)";

(* Entfalten von Definitionen: *)
lemma "exor x x = nand x (~x)"
apply(unfold exor_def nand_def)
apply(simp)
done;

(* Simplifizieren mit Definitionen: *)
lemma "exor x x = nand x (~x)"
apply(simp add: exor_def nand_def)
done;

(* Let ist auch nur ein definiertes Konzept: *)
lemma "let x = 1::nat; y = x+1; z = y+y in z=u"
apply(unfold Let_def)
apply simp
oops;


(** Der Praeprozessor: **)

lemma "xs = [] & ys = xs ==> ys = zs"
apply(simp)
oops

lemma "[| f xs = []; ALL ys. f ys = [] --> g ys = ys |] ==> g xs = zs"
apply(simp)
oops;

(** Lokale Annahmen: **)
lemma "x+0 = (0::nat) --> x+y = x"
apply(simp)
oops;

(** Fallunterscheidungen **)

(* Bei if automatisch: *)
lemma "(A & B) = (if A then B else False)"
apply(simp)
done

lemma "if A then B else C"
apply(simp)
oops;

(* Bei case explizit: *)
lemma "x = (case x of 0 => n | Suc y => y+y)"
(* apply(simp) schlaegt fehl, da sich nichts veraendert *)
apply(split nat.split)
apply simp
oops;
(* Simp + split: *)
lemma "x = (case x of 0 => n | Suc y => y+y)"
apply(simp split: nat.split)
oops;

(** Ein bischen lineare Arithmetik: **)
lemma "[| (x::nat) <= y+z; z+x < y |] ==> x < y"
apply(simp)
done;


(** Tracing: **)

lemma "rev[x] = []"
apply(simp)
oops;

(** Da Methode auto Methode simp benutzt, kann man auto (fast) genauso
    modifizieren wie simp:
**)
thm add_mult_distrib2
lemma "(EX u::nat. x=y+u) --> a*(b+c)+y <= x + a*b+a*c"
apply(auto simp add: add_mult_distrib2)
done


(* subgoal_tac *)
lemma "\<lbrakk> \<forall> x y z. f (f x y) z = f x (f y z); \<forall> x. f x (g x) = n \<rbrakk>
  \<Longrightarrow> f a (f b (g (f a b))) = n"
apply (subgoal_tac "n = f (f a  b) (g (f a b))")
apply simp+
done

end