Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Examples/IntEx.thy
changeset 1260 9df6144e281b
parent 1259 db158e995bfc
child 1261 853abc14c5c6 
--- a/Quot/Examples/IntEx.thy	Thu Feb 25 07:48:57 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,277 +0,0 @@
-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
nominal2