theory Demo6 imports Main begin

text {* Introducing new types *}

-- {* a new "undefined" type: *}
typedecl names  
consts blah :: names


-- {* simple abbreviation: *}
types 'a rel = "'a \<Rightarrow> 'a \<Rightarrow> bool"
definition
  eq :: "'a rel"
where
  "eq x y \<equiv> (x = y)"


-- {* type definiton: pairs *}

typedef (prod) 
  ('a, 'b) prod = "{f. \<exists>a b. f = (\<lambda>(x::'a) (y::'b). x=a \<and> y=b)}"
  by blast
  
print_theorems 

definition
  pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) prod"
where
  "pair a b \<equiv> Abs_prod (\<lambda>x y. x = a \<and> y = b)"

definition
  fs :: "('a,'b) prod \<Rightarrow> 'a"
where
  "fs x \<equiv> SOME a. \<exists>b. x = pair a b"

definition
  sn :: "('a,'b) prod \<Rightarrow> 'b"
where
  "sn x \<equiv> SOME b. \<exists>a. x = pair a b"

lemma in_prod: "(\<lambda>x y. x = a \<and> y = b) \<in> prod"
  apply (unfold prod_def)
  apply blast
  done

lemma pair_inject:
  "pair a b = pair a' b' \<Longrightarrow> a=a' \<and> b=b'"
  apply (unfold pair_def)
  thm Abs_prod_inject
  apply (insert in_prod [of a b])
  apply (insert in_prod [of a' b'])
  apply (blast dest: Abs_prod_inject fun_cong)
  done

lemma pair_eq:
  "(pair a b = pair a' b') = (a=a' \<and> b=b')"
  by (blast dest: pair_inject)

lemma fs:
  "fs (pair a b) = a"
  apply (unfold fs_def)
  apply (blast dest: pair_inject)
  done

thm some_equality

lemma sn:
  "sn (pair a b) = b"
  apply (unfold sn_def)
  apply (blast dest: pair_inject)
  done


-- -----------------------------------------------------------

text {* Simplification *}


text {* 
Lists: 
  @{term "[]"}       empty list
  @{term "x#xs"}     cons (list with head x and tail xs)
  @{term "xs @ ys"}  append xs and ys
*}

lemma "ys @ [] = []"
apply(simp)
oops 

constdefs
  a :: "nat list"
  "a \<equiv> []"

  b :: "nat list"
  "b \<equiv> []"

text {* simp add, rewriting with definitions *}
lemma "xs @ a = xs"
  apply (simp add: a_def)
  done

text {* simp only *}
lemma "xs @ a = xs"
  apply (simp only: a_def)
  apply simp
  done


lemma ab [simp]: "a = b" by (simp add: a_def b_def)
lemma ba [simp]: "b = a" by simp

text {* simp del, termination *}
lemma "a = []"
  (*
  apply (simp add: a_def)  
  does not terminate *)
  apply (simp add: a_def del: ab) 
  done


text{* Simple assumption: *}
lemma "xs = [] \<Longrightarrow> xs @ ys = ys @ xs @ ys"
  apply simp
  oops

text{* Simplification in assumption: *}
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
  apply simp
  done


end
