chapter \<open>Exercise Sheet -- Week 7\<close>

theory Exercise07
  imports 
    Main
begin

section \<open>Exercise 1 -- 4 points\<close>

text \<open>Task 1 (1 point)\<close>

text \<open>Complete the following definition to represent the transitive closure of
  a binary relation $R$, i.e., $R^+$.\<close>

inductive_set transcl :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" for R where
  "everything \<in> transcl R" 

text \<open>Task 2 (1 point): Prove that the transitive closure of R contains R.\<close>

lemma transcl_R: "R \<subseteq> transcl R" 
proof (intro subrelI)
  oops

text \<open>Task 3 (1 point): Prove that the transitive closure of R is transitive.\<close>

text \<open>Note: @{term "A O B"} is relation composition of two binary relations A and B.\<close>

lemma transcl_trans: "transcl R O transcl R \<subseteq> transcl R" 
proof (intro subrelI)
  oops

text \<open>Task 4 (1 point): Prove that the transitive closure of R 
  is the least transitive relation that contains R.\<close>

lemma transcl_least: assumes "R \<subseteq> S" and "S O S \<subseteq> S" 
  shows "transcl R \<subseteq> S" 
proof (intro subrelI)
  oops


section \<open>Exercise 2 -- 3 points\<close>

text \<open>Consider the big-step semantics of simple while programs from Demo07\<close>

type_synonym var = string
type_synonym val = nat
type_synonym state = "var \<Rightarrow> val" 

datatype prog = 
  Skip
  | Update "state \<Rightarrow> state" 
  | Sequence prog prog
  | While "state \<Rightarrow> bool" prog

inductive eval :: "prog \<Rightarrow> state \<Rightarrow> state \<Rightarrow> bool" where
  skip: "eval Skip s s" 
| update: "eval (Update f) s (f s)" 
| sequence: "eval p s t \<Longrightarrow> eval q t u \<Longrightarrow> eval (Sequence p q) s u" 
| while_false: "\<not> c s \<Longrightarrow> eval (While c p) s s" 
| while_true: "c s \<Longrightarrow> eval p s t \<Longrightarrow> eval (While c p) t u \<Longrightarrow> eval (While c p) s u" 

text \<open>Prove that the evaluation relation is deterministic.\<close>

text \<open>Hint: you need one rule induction and several rule inversions.\<close>

lemma eval_det: "eval p s t \<Longrightarrow> eval p s u \<Longrightarrow> t = u" 
  oops


section \<open>Exercise 3 -- 3 points\<close>

text \<open>Prove the well-known fact about the cardinality of the powerset of a finite set.\<close>

text \<open>Comment: with this exercise you will become more familiar with sets in Isabelle.\<close>
text \<open>Hint: use @{command find_theorems} to find existing facts, if sledgehammer is not
  successful.\<close>

lemma "finite X \<Longrightarrow> card { A . A \<subseteq> X} = 2^card X" 
proof (induct X rule: finite_induct)
  case (insert x X)
  have "{A. A \<subseteq> insert x X} = (insert x ` {A . A \<subseteq> X}) \<union> {A . A \<subseteq> X}" (is "?L = ?R1 \<union> ?R2") 
  proof
    show "?L \<subseteq> ?R1 \<union> ?R2" sorry
  qed auto
  
  show ?case sorry
qed auto

  
end