theory a3 imports Main begin

(* Any of the lemmas below may need to be generalised first to be provable. *)


lemma sorted_quicksort:
  "sorted (qicksort xs)"
  oops

(* define intervals, is_int_list and set_of *) 


(* some test cases for (a) *)
lemma 
  "set_of [(0,1), (2, 4)] = {0,2,3}"
  oops

lemma
  "is_int_list [(0,1), (2, 4)]"
  oops

lemma
  "\<not>is_int_list [(0,3), (1,5)]"
  oops


(* (b) define add and rem *)


(* invent test cases and prove them *)


(* (c) prove: (may need additional assumptions) *)
lemma set_of_add:
  "set_of (add (x,y) xs) = {x..<y} \<union> set_of xs"
  oops
  
lemma is_int_list_add:
  "is_int_list xs \<Longrightarrow> is_int_list (add (a,b) xs)"
  oops
  

(* (d) prove: (may need additional assumptions) *)
lemma set_of_rem:
  "set_of (rem (a,b) xs) = set_of xs - {a..<b}"
  oops

lemma is_int_list_rem:
  "is_int_list xs \<Longrightarrow> is_int_list (rem (a,b) xs)"
  oops
  
end