--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/IntEx.thy	Thu Feb 25 07:57:17 2010 +0100
@@ -0,0 +1,277 @@
+theory IntEx
+imports "../Quotient_Product" "../Quotient_List"
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type 
+  my_int = "nat \<times> nat" / intrel
+  apply(unfold equivp_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+quotient_definition
+  "ZERO :: my_int"
+is
+  "(0::nat, 0::nat)"
+
+quotient_definition
+  "ONE :: my_int"
+is
+  "(1::nat, 0::nat)"
+
+fun
+  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_plus (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+  "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+is
+  "my_plus"
+
+fun
+  my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_neg (x, y) = (y, x)"
+
+quotient_definition
+  "NEG :: my_int \<Rightarrow> my_int"
+is
+  "my_neg"
+
+definition
+  MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+where
+  "MINUS z w = PLUS z (NEG w)"
+
+fun
+  my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+  "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+is
+  "my_mult"
+
+
+(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
+fun
+  my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "my_le (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+   "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
+is
+  "my_le"
+
+term LE
+thm LE_def
+
+
+definition
+  LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
+where
+  "LESS z w = (LE z w \<and> z \<noteq> w)"
+
+term LESS
+thm LESS_def
+
+definition
+  ABS :: "my_int \<Rightarrow> my_int"
+where
+  "ABS i = (if (LESS i ZERO) then (NEG i) else i)"
+
+definition
+  SIGN :: "my_int \<Rightarrow> my_int"
+where
+ "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
+
+print_quotconsts
+
+lemma plus_sym_pre:
+  shows "my_plus a b \<approx> my_plus b a"
+  apply(cases a)
+  apply(cases b)
+  apply(auto)
+  done
+
+lemma plus_rsp[quot_respect]:
+  shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
+by (simp)
+
+lemma neg_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx>) my_neg my_neg"
+by simp
+
+lemma test1: "my_plus a b = my_plus a b"
+apply(rule refl)
+done
+
+lemma "PLUS a b = PLUS a b"
+apply(lifting_setup test1)
+apply(regularize)
+apply(injection)
+apply(cleaning)
+done
+
+thm lambda_prs
+
+lemma test2: "my_plus a = my_plus a"
+apply(rule refl)
+done
+
+lemma "PLUS a = PLUS a"
+apply(lifting_setup test2)
+apply(rule impI)
+apply(rule ballI)
+apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
+apply(simp only: in_respects)
+apply(injection)
+apply(cleaning)
+done
+
+lemma test3: "my_plus = my_plus"
+apply(rule refl)
+done
+
+lemma "PLUS = PLUS"
+apply(lifting_setup test3)
+apply(rule impI)
+apply(rule plus_rsp)
+apply(injection)
+apply(cleaning)
+done
+
+
+lemma "PLUS a b = PLUS b a"
+apply(lifting plus_sym_pre)
+done
+
+lemma plus_assoc_pre:
+  shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
+  apply (cases i)
+  apply (cases j)
+  apply (cases k)
+  apply (simp)
+  done
+
+lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
+apply(lifting plus_assoc_pre)
+done
+
+lemma int_induct_raw:
+  assumes a: "P (0::nat, 0)"
+  and     b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))"
+  and     c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))"
+  shows      "P x"
+  apply(case_tac x) apply(simp)
+  apply(rule_tac x="b" in spec)
+  apply(rule_tac Nat.induct)
+  apply(rule allI)
+  apply(rule_tac Nat.induct)
+  using a b c apply(auto)
+  done
+
+lemma int_induct:
+  assumes a: "P ZERO"
+  and     b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)"
+  and     c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))"
+  shows      "P x"
+  using a b c
+  by (lifting int_induct_raw)
+
+lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
+sorry
+
+lemma ex1tst': "\<exists>!(x::my_int). x = x"
+apply(lifting ex1tst)
+done
+
+
+lemma ho_tst: "foldl my_plus x [] = x"
+apply simp
+done
+
+
+term foldl
+lemma "foldl PLUS x [] = x"
+apply(lifting ho_tst)
+done
+
+lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
+sorry
+
+lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
+apply(lifting ho_tst2)
+done
+
+lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
+by simp
+
+lemma "foldl f (x::my_int) ([]::my_int list) = x"
+apply(lifting ho_tst3)
+done
+
+lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
+by simp
+
+(* Don't know how to keep the goal non-contracted... *)
+lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
+apply(lifting lam_tst)
+done
+
+lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
+by simp
+
+lemma
+  shows "equivp (op \<approx>)"
+  and "equivp ((op \<approx>) ===> (op \<approx>))"
+(* Nitpick finds a counterexample! *)
+oops
+
+lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
+by auto
+
+lemma id_rsp:
+  shows "(R ===> R) id id"
+by simp
+
+lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
+apply (rule babs_rsp[OF Quotient_my_int])
+apply (simp add: id_rsp)
+done
+
+lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
+apply(lifting lam_tst3a)
+apply(rule impI)
+apply(rule lam_tst3a_reg)
+done
+
+lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
+by auto
+
+lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
+apply(lifting lam_tst3b)
+apply(rule impI)
+apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+apply(simp add: id_rsp)
+done
+
+lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"
+apply (induct l)
+apply simp
+apply (case_tac a)
+apply simp
+done
+
+lemma "map (\<lambda>x. PLUS x ZERO) l = l"
+apply(lifting lam_tst4)
+done
+
+end