--- a/Attic/Quot/Examples/LamEx.thy Thu Apr 29 17:52:19 2010 +0200
+++ b/Attic/Quot/Examples/LamEx.thy Thu Apr 29 17:52:33 2010 +0200
@@ -55,16 +55,16 @@
lemma rfv_eqvt[eqvt]:
fixes pi::"name prm"
shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
-apply(induct t)
-apply(simp_all)
-apply(simp add: perm_set_eq)
-apply(simp add: union_eqvt)
-apply(simp add: set_diff_eqvt)
-apply(simp add: perm_set_eq)
-done
+ apply(induct t)
+ apply(simp_all)
+ apply(simp add: perm_set_eq)
+ apply(simp add: union_eqvt)
+ apply(simp add: set_diff_eqvt)
+ apply(simp add: perm_set_eq)
+ done
inductive
- alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
+ alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
where
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
@@ -76,101 +76,101 @@
lemma alpha_eqvt:
fixes pi::"name prm"
shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
-apply(induct rule: alpha.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(simp)
-apply(rule a3)
-apply(erule conjE)
-apply(erule exE)
-apply(erule conjE)
-apply(rule_tac x="pi \<bullet> pia" in exI)
-apply(rule conjI)
-apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1])
-apply(perm_simp add: eqvts)
-apply(rule conjI)
-apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1])
-apply(perm_simp add: eqvts)
-apply(rule conjI)
-apply(subst perm_compose[symmetric])
-apply(simp)
-apply(subst perm_compose[symmetric])
-apply(simp)
-done
+ apply(induct rule: alpha.induct)
+ apply(simp add: a1)
+ apply(simp add: a2)
+ apply(simp)
+ apply(rule a3)
+ apply(erule conjE)
+ apply(erule exE)
+ apply(erule conjE)
+ apply(rule_tac x="pi \<bullet> pia" in exI)
+ apply(rule conjI)
+ apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1])
+ apply(perm_simp add: eqvts)
+ apply(rule conjI)
+ apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1])
+ apply(perm_simp add: eqvts)
+ apply(rule conjI)
+ apply(subst perm_compose[symmetric])
+ apply(simp)
+ apply(subst perm_compose[symmetric])
+ apply(simp)
+ done
lemma alpha_refl:
shows "t \<approx> t"
-apply(induct t rule: rlam.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(rule a3)
-apply(rule_tac x="[]" in exI)
-apply(simp_all add: fresh_star_def fresh_list_nil)
-done
+ apply(induct t rule: rlam.induct)
+ apply(simp add: a1)
+ apply(simp add: a2)
+ apply(rule a3)
+ apply(rule_tac x="[]" in exI)
+ apply(simp_all add: fresh_star_def fresh_list_nil)
+ done
lemma alpha_sym:
shows "t \<approx> s \<Longrightarrow> s \<approx> t"
-apply(induct rule: alpha.induct)
-apply(simp add: a1)
-apply(simp add: a2)
-apply(rule a3)
-apply(erule exE)
-apply(rule_tac x="rev pi" in exI)
-apply(simp)
-apply(simp add: fresh_star_def fresh_list_rev)
-apply(rule conjI)
-apply(erule conjE)+
-apply(rotate_tac 3)
-apply(drule_tac pi="rev pi" in alpha_eqvt)
-apply(perm_simp)
-apply(rule pt_bij2[OF pt_name_inst at_name_inst])
-apply(simp)
-done
+ apply(induct rule: alpha.induct)
+ apply(simp add: a1)
+ apply(simp add: a2)
+ apply(rule a3)
+ apply(erule exE)
+ apply(rule_tac x="rev pi" in exI)
+ apply(simp)
+ apply(simp add: fresh_star_def fresh_list_rev)
+ apply(rule conjI)
+ apply(erule conjE)+
+ apply(rotate_tac 3)
+ apply(drule_tac pi="rev pi" in alpha_eqvt)
+ apply(perm_simp)
+ apply(rule pt_bij2[OF pt_name_inst at_name_inst])
+ apply(simp)
+ done
lemma alpha_trans:
shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
-apply(induct arbitrary: t3 rule: alpha.induct)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(simp add: a1)
-apply(rotate_tac 4)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(simp add: a2)
-apply(rotate_tac 1)
-apply(erule alpha.cases)
-apply(simp_all)
-apply(erule conjE)+
-apply(erule exE)+
-apply(erule conjE)+
-apply(rule a3)
-apply(rule_tac x="pia @ pi" in exI)
-apply(simp add: fresh_star_def fresh_list_append)
-apply(simp add: pt_name2)
-apply(drule_tac x="rev pia \<bullet> sa" in spec)
-apply(drule mp)
-apply(rotate_tac 8)
-apply(drule_tac pi="rev pia" in alpha_eqvt)
-apply(perm_simp)
-apply(rotate_tac 11)
-apply(drule_tac pi="pia" in alpha_eqvt)
-apply(perm_simp)
-done
+ apply(induct arbitrary: t3 rule: alpha.induct)
+ apply(erule alpha.cases)
+ apply(simp_all)
+ apply(simp add: a1)
+ apply(rotate_tac 4)
+ apply(erule alpha.cases)
+ apply(simp_all)
+ apply(simp add: a2)
+ apply(rotate_tac 1)
+ apply(erule alpha.cases)
+ apply(simp_all)
+ apply(erule conjE)+
+ apply(erule exE)+
+ apply(erule conjE)+
+ apply(rule a3)
+ apply(rule_tac x="pia @ pi" in exI)
+ apply(simp add: fresh_star_def fresh_list_append)
+ apply(simp add: pt_name2)
+ apply(drule_tac x="rev pia \<bullet> sa" in spec)
+ apply(drule mp)
+ apply(rotate_tac 8)
+ apply(drule_tac pi="rev pia" in alpha_eqvt)
+ apply(perm_simp)
+ apply(rotate_tac 11)
+ apply(drule_tac pi="pia" in alpha_eqvt)
+ apply(perm_simp)
+ done
lemma alpha_equivp:
shows "equivp alpha"
-apply(rule equivpI)
-unfolding reflp_def symp_def transp_def
-apply(auto intro: alpha_refl alpha_sym alpha_trans)
-done
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(auto intro: alpha_refl alpha_sym alpha_trans)
+ done
lemma alpha_rfv:
shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
-apply(induct rule: alpha.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-done
+ apply(induct rule: alpha.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ done
quotient_type lam = rlam / alpha
by (rule alpha_equivp)
@@ -210,16 +210,10 @@
end
lemma perm_rsp[quot_respect]:
- "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
- apply(auto)
- (* this is propably true if some type conditions are imposed ;o) *)
- sorry
-
-lemma fresh_rsp:
- "(op = ===> alpha ===> op =) fresh fresh"
- apply(auto)
- (* this is probably only true if some type conditions are imposed *)
- sorry
+ "(op = ===> alpha ===> alpha) op \<bullet> (op \<bullet> :: (name \<times> name) list \<Rightarrow> rlam \<Rightarrow> rlam)"
+ apply auto
+ apply(erule alpha_eqvt)
+ done
lemma rVar_rsp[quot_respect]:
"(op = ===> alpha) rVar rVar"
@@ -239,8 +233,8 @@
lemma rfv_rsp[quot_respect]:
"(alpha ===> op =) rfv rfv"
-apply(simp add: alpha_rfv)
-done
+ apply(simp add: alpha_rfv)
+ done
section {* lifted theorems *}
@@ -251,56 +245,47 @@
\<Longrightarrow> P lam"
by (lifting rlam.induct)
-ML {* show_all_types := true *}
-
lemma perm_lam [simp]:
- fixes pi::"'a prm"
+ fixes pi::"name prm"
shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
-apply(lifting perm_rlam.simps)
-ML_prf {*
- List.last (map (symmetric o #def) (Quotient_Info.qconsts_dest @{context}));
- List.last (map (Thm.varifyT o symmetric o #def) (Quotient_Info.qconsts_dest @{context}))
-*}
-done
+ by (lifting perm_rlam.simps[where 'a="name"])
instance lam::pt_name
-apply(default)
-apply(induct_tac [!] x rule: lam_induct)
-apply(simp_all add: pt_name2 pt_name3)
-done
+ apply(default)
+ apply(induct_tac [!] x rule: lam_induct)
+ apply(simp_all add: pt_name2 pt_name3)
+ done
lemma fv_lam [simp]:
shows "fv (Var a) = {a}"
and "fv (App t1 t2) = fv t1 \<union> fv t2"
and "fv (Lam a t) = fv t - {a}"
-apply(lifting rfv_var rfv_app rfv_lam)
-done
+ by(lifting rfv_var rfv_app rfv_lam)
-
-lemma a1:
+lemma a1:
"a = b \<Longrightarrow> Var a = Var b"
by (lifting a1)
-lemma a2:
+lemma a2:
"\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
by (lifting a2)
-lemma a3:
+lemma a3:
"\<lbrakk>\<exists>pi::name prm. (fv t - {a} = fv s - {b} \<and> (fv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk>
\<Longrightarrow> Lam a t = Lam b s"
by (lifting a3)
-lemma alpha_cases:
+lemma alpha_cases:
"\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
- \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
+ \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> (fv t - {a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (lifting alpha.cases)
-lemma alpha_induct:
+lemma alpha_induct:
"\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
\<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
\<And>t a s b.
@@ -312,18 +297,18 @@
lemma lam_inject [simp]:
shows "(Var a = Var b) = (a = b)"
and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
-apply(lifting rlam.inject(1) rlam.inject(2))
-apply(auto)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(simp add: alpha.a1)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(drule alpha.cases)
-apply(simp_all)
-apply(rule alpha.a2)
-apply(simp_all)
-done
+ apply(lifting rlam.inject(1) rlam.inject(2))
+ apply(auto)
+ apply(drule alpha.cases)
+ apply(simp_all)
+ apply(simp add: alpha.a1)
+ apply(drule alpha.cases)
+ apply(simp_all)
+ apply(drule alpha.cases)
+ apply(simp_all)
+ apply(rule alpha.a2)
+ apply(simp_all)
+ done
lemma rlam_distinct:
shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
@@ -332,20 +317,20 @@
and "\<not>(rLam nam' rlam' \<approx> rVar nam)"
and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
-apply auto
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-done
+ apply auto
+ apply(erule alpha.cases)
+ apply simp_all
+ apply(erule alpha.cases)
+ apply simp_all
+ apply(erule alpha.cases)
+ apply simp_all
+ apply(erule alpha.cases)
+ apply simp_all
+ apply(erule alpha.cases)
+ apply simp_all
+ apply(erule alpha.cases)
+ apply simp_all
+ done
lemma lam_distinct[simp]:
shows "Var nam \<noteq> App lam1' lam2'"
@@ -354,8 +339,7 @@
and "Lam nam' lam' \<noteq> Var nam"
and "App lam1 lam2 \<noteq> Lam nam' lam'"
and "Lam nam' lam' \<noteq> App lam1 lam2"
-apply(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
-done
+ by(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
lemma var_supp1:
shows "(supp (Var a)) = ((supp a)::name set)"
@@ -367,31 +351,30 @@
lemma app_supp:
shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
-apply(simp only: perm_lam supp_def lam_inject)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
-done
+ apply(simp only: perm_lam supp_def lam_inject)
+ apply(simp add: Collect_imp_eq Collect_neg_eq)
+ done
lemma lam_supp:
shows "supp (Lam x t) = ((supp ([x].t))::name set)"
-apply(simp add: supp_def)
-apply(simp add: abs_perm)
-sorry
-
+ apply(simp add: supp_def)
+ apply(simp add: abs_perm)
+ sorry
instance lam::fs_name
-apply(default)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: var_supp)
-apply(simp add: app_supp)
-apply(simp add: lam_supp abs_supp)
-done
+ apply(default)
+ apply(induct_tac x rule: lam_induct)
+ apply(simp add: var_supp)
+ apply(simp add: app_supp)
+ apply(simp add: lam_supp abs_supp)
+ done
lemma fresh_lam:
"(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)"
-apply(simp add: fresh_def)
-apply(simp add: lam_supp abs_supp)
-apply(auto)
-done
+ apply(simp add: fresh_def)
+ apply(simp add: lam_supp abs_supp)
+ apply(auto)
+ done
lemma lam_induct_strong:
fixes a::"'a::fs_name"
--- a/Attic/Quot/Examples/LarryDatatype.thy Thu Apr 29 17:52:19 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-theory LarryDatatype
-imports Main "../Quotient" "../Quotient_Syntax"
-begin
-
-subsection{*Defining the Free Algebra*}
-
-datatype
- freemsg = NONCE nat
- | MPAIR freemsg freemsg
- | CRYPT nat freemsg
- | DECRYPT nat freemsg
-
-inductive
- msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
-where
- CD: "CRYPT K (DECRYPT K X) \<sim> X"
-| DC: "DECRYPT K (CRYPT K X) \<sim> X"
-| NONCE: "NONCE N \<sim> NONCE N"
-| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
-| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
-| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
-| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
-| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-
-lemmas msgrel.intros[intro]
-
-text{*Proving that it is an equivalence relation*}
-
-lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
-
-theorem equiv_msgrel: "equivp msgrel"
-proof (rule equivpI)
- show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
- show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
- show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
-qed
-
-subsection{*Some Functions on the Free Algebra*}
-
-subsubsection{*The Set of Nonces*}
-
-fun
- freenonces :: "freemsg \<Rightarrow> nat set"
-where
- "freenonces (NONCE N) = {N}"
-| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-| "freenonces (CRYPT K X) = freenonces X"
-| "freenonces (DECRYPT K X) = freenonces X"
-
-theorem msgrel_imp_eq_freenonces:
- assumes a: "U \<sim> V"
- shows "freenonces U = freenonces V"
- using a by (induct) (auto)
-
-subsubsection{*The Left Projection*}
-
-text{*A function to return the left part of the top pair in a message. It will
-be lifted to the initial algrebra, to serve as an example of that process.*}
-fun
- freeleft :: "freemsg \<Rightarrow> freemsg"
-where
- "freeleft (NONCE N) = NONCE N"
-| "freeleft (MPAIR X Y) = X"
-| "freeleft (CRYPT K X) = freeleft X"
-| "freeleft (DECRYPT K X) = freeleft X"
-
-text{*This theorem lets us prove that the left function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeleft_aux:
- shows "freeleft U \<sim> freeleft U"
- by (induct rule: freeleft.induct) (auto)
-
-theorem msgrel_imp_eqv_freeleft:
- assumes a: "U \<sim> V"
- shows "freeleft U \<sim> freeleft V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
-
-subsubsection{*The Right Projection*}
-
-text{*A function to return the right part of the top pair in a message.*}
-fun
- freeright :: "freemsg \<Rightarrow> freemsg"
-where
- "freeright (NONCE N) = NONCE N"
-| "freeright (MPAIR X Y) = Y"
-| "freeright (CRYPT K X) = freeright X"
-| "freeright (DECRYPT K X) = freeright X"
-
-text{*This theorem lets us prove that the right function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeright_aux:
- shows "freeright U \<sim> freeright U"
- by (induct rule: freeright.induct) (auto)
-
-theorem msgrel_imp_eqv_freeright:
- assumes a: "U \<sim> V"
- shows "freeright U \<sim> freeright V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
-
-subsubsection{*The Discriminator for Constructors*}
-
-text{*A function to distinguish nonces, mpairs and encryptions*}
-fun
- freediscrim :: "freemsg \<Rightarrow> int"
-where
- "freediscrim (NONCE N) = 0"
- | "freediscrim (MPAIR X Y) = 1"
- | "freediscrim (CRYPT K X) = freediscrim X + 2"
- | "freediscrim (DECRYPT K X) = freediscrim X - 2"
-
-text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
-theorem msgrel_imp_eq_freediscrim:
- assumes a: "U \<sim> V"
- shows "freediscrim U = freediscrim V"
- using a by (induct) (auto)
-
-subsection{*The Initial Algebra: A Quotiented Message Type*}
-
-quotient_type msg = freemsg / msgrel
- by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_definition
- "Nonce :: nat \<Rightarrow> msg"
-is
- "NONCE"
-
-quotient_definition
- "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-is
- "MPAIR"
-
-quotient_definition
- "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "CRYPT"
-
-quotient_definition
- "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
-
-text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]:
- shows "Crypt K (Decrypt K X) = X"
- by (lifting CD)
-
-theorem DC_eq [simp]:
- shows "Decrypt K (Crypt K X) = X"
- by (lifting DC)
-
-subsection{*The Abstract Function to Return the Set of Nonces*}
-
-quotient_definition
- "nonces:: msg \<Rightarrow> nat set"
-is
- "freenonces"
-
-text{*Now prove the four equations for @{term nonces}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freenonces freenonces"
- by (simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim>) NONCE NONCE"
- by (simp add: NONCE)
-
-lemma nonces_Nonce [simp]:
- shows "nonces (Nonce N) = {N}"
- by (lifting freenonces.simps(1))
-
-lemma [quot_respect]:
- shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
- by (simp add: MPAIR)
-
-lemma nonces_MPair [simp]:
- shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
- by (lifting freenonces.simps(2))
-
-lemma nonces_Crypt [simp]:
- shows "nonces (Crypt K X) = nonces X"
- by (lifting freenonces.simps(3))
-
-lemma nonces_Decrypt [simp]:
- shows "nonces (Decrypt K X) = nonces X"
- by (lifting freenonces.simps(4))
-
-subsection{*The Abstract Function to Return the Left Part*}
-
-quotient_definition
- "left:: msg \<Rightarrow> msg"
-is
- "freeleft"
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
- by (simp add: msgrel_imp_eqv_freeleft)
-
-lemma left_Nonce [simp]:
- shows "left (Nonce N) = Nonce N"
- by (lifting freeleft.simps(1))
-
-lemma left_MPair [simp]:
- shows "left (MPair X Y) = X"
- by (lifting freeleft.simps(2))
-
-lemma left_Crypt [simp]:
- shows "left (Crypt K X) = left X"
- by (lifting freeleft.simps(3))
-
-lemma left_Decrypt [simp]:
- shows "left (Decrypt K X) = left X"
- by (lifting freeleft.simps(4))
-
-subsection{*The Abstract Function to Return the Right Part*}
-
-quotient_definition
- "right:: msg \<Rightarrow> msg"
-is
- "freeright"
-
-text{*Now prove the four equations for @{term right}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeright freeright"
- by (simp add: msgrel_imp_eqv_freeright)
-
-lemma right_Nonce [simp]:
- shows "right (Nonce N) = Nonce N"
- by (lifting freeright.simps(1))
-
-lemma right_MPair [simp]:
- shows "right (MPair X Y) = Y"
- by (lifting freeright.simps(2))
-
-lemma right_Crypt [simp]:
- shows "right (Crypt K X) = right X"
- by (lifting freeright.simps(3))
-
-lemma right_Decrypt [simp]:
- shows "right (Decrypt K X) = right X"
- by (lifting freeright.simps(4))
-
-subsection{*Injectivity Properties of Some Constructors*}
-
-lemma NONCE_imp_eq:
- shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
- by (drule msgrel_imp_eq_freenonces, simp)
-
-text{*Can also be proved using the function @{term nonces}*}
-lemma Nonce_Nonce_eq [iff]:
- shows "(Nonce m = Nonce n) = (m = n)"
-proof
- assume "Nonce m = Nonce n"
- then show "m = n" by (lifting NONCE_imp_eq)
-next
- assume "m = n"
- then show "Nonce m = Nonce n" by simp
-qed
-
-lemma MPAIR_imp_eqv_left:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
- by (drule msgrel_imp_eqv_freeleft) (simp)
-
-lemma MPair_imp_eq_left:
- assumes eq: "MPair X Y = MPair X' Y'"
- shows "X = X'"
- using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
- by (drule msgrel_imp_eqv_freeright) (simp)
-
-lemma MPair_imp_eq_right:
- shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
- by (lifting MPAIR_imp_eqv_right)
-
-theorem MPair_MPair_eq [iff]:
- shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
- by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
-
-lemma NONCE_neqv_MPAIR:
- shows "\<not>(NONCE m \<sim> MPAIR X Y)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Nonce_neq_MPair [iff]:
- shows "Nonce N \<noteq> MPair X Y"
- by (lifting NONCE_neqv_MPAIR)
-
-text{*Example suggested by a referee*}
-
-lemma CRYPT_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt_Nonce_neq_Nonce:
- shows "Crypt K (Nonce M) \<noteq> Nonce N"
- by (lifting CRYPT_NONCE_neq_NONCE)
-
-text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt2_Nonce_neq_Nonce:
- shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
- by (lifting CRYPT2_NONCE_neq_NONCE)
-
-theorem Crypt_Crypt_eq [iff]:
- shows "(Crypt K X = Crypt K X') = (X=X')"
-proof
- assume "Crypt K X = Crypt K X'"
- hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Crypt K X = Crypt K X'" by simp
-qed
-
-theorem Decrypt_Decrypt_eq [iff]:
- shows "(Decrypt K X = Decrypt K X') = (X=X')"
-proof
- assume "Decrypt K X = Decrypt K X'"
- hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Decrypt K X = Decrypt K X'" by simp
-qed
-
-lemma msg_induct_aux:
- shows "\<lbrakk>\<And>N. P (Nonce N);
- \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
- \<And>K X. P X \<Longrightarrow> P (Crypt K X);
- \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
- by (lifting freemsg.induct)
-
-lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
- assumes N: "\<And>N. P (Nonce N)"
- and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
- and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
- and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
- shows "P msg"
- using N M C D by (rule msg_induct_aux)
-
-subsection{*The Abstract Discriminator*}
-
-text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
-need this function in order to prove discrimination theorems.*}
-
-quotient_definition
- "discrim:: msg \<Rightarrow> int"
-is
- "freediscrim"
-
-text{*Now prove the four equations for @{term discrim}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freediscrim freediscrim"
- by (auto simp add: msgrel_imp_eq_freediscrim)
-
-lemma discrim_Nonce [simp]:
- shows "discrim (Nonce N) = 0"
- by (lifting freediscrim.simps(1))
-
-lemma discrim_MPair [simp]:
- shows "discrim (MPair X Y) = 1"
- by (lifting freediscrim.simps(2))
-
-lemma discrim_Crypt [simp]:
- shows "discrim (Crypt K X) = discrim X + 2"
- by (lifting freediscrim.simps(3))
-
-lemma discrim_Decrypt [simp]:
- shows "discrim (Decrypt K X) = discrim X - 2"
- by (lifting freediscrim.simps(4))
-
-end
-
--- a/Attic/Quot/Examples/LarryInt.thy Thu Apr 29 17:52:19 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
-
-theory LarryInt
-imports Nat "../Quotient" "../Quotient_Product"
-begin
-
-fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
-begin
-
-quotient_definition
- Zero_int_def: "0::int" is "(0::nat, 0::nat)"
-
-quotient_definition
- One_int_def: "1::int" is "(1::nat, 0::nat)"
-
-definition
- "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-quotient_definition
- "(op +) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "add_raw"
-
-definition
- "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
-
-quotient_definition
- "uminus :: int \<Rightarrow> int"
-is
- "uminus_raw"
-
-fun
- mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
- "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
- "(op *) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "mult_raw"
-
-definition
- "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-is
- "le_raw"
-
-definition
- less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
-
-definition
- diff_int_def: "z - (w::int) \<equiv> z + (-w)"
-
-instance ..
-
-end
-
-subsection{*Construction of the Integers*}
-
-lemma zminus_zminus_raw:
- "uminus_raw (uminus_raw z) = z"
- by (cases z) (simp add: uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel) uminus_raw uminus_raw"
- by (simp add: uminus_raw_def)
-
-lemma zminus_zminus:
- fixes z::"int"
- shows "- (- z) = z"
- by(lifting zminus_zminus_raw)
-
-lemma zminus_0_raw:
- shows "uminus_raw (0, 0) = (0, 0::nat)"
- by (simp add: uminus_raw_def)
-
-lemma zminus_0:
- shows "- 0 = (0::int)"
- by (lifting zminus_0_raw)
-
-subsection{*Integer Addition*}
-
-lemma zminus_zadd_distrib_raw:
- shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
-by (cases z, cases w)
- (auto simp add: add_raw_def uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
-by (simp add: add_raw_def)
-
-lemma zminus_zadd_distrib:
- fixes z w::"int"
- shows "- (z + w) = (- z) + (- w)"
- by(lifting zminus_zadd_distrib_raw)
-
-lemma zadd_commute_raw:
- shows "add_raw z w = add_raw w z"
-by (cases z, cases w)
- (simp add: add_raw_def)
-
-lemma zadd_commute:
- fixes z w::"int"
- shows "(z::int) + w = w + z"
- by (lifting zadd_commute_raw)
-
-lemma zadd_assoc_raw:
- shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
- by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-
-lemma zadd_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
- by (lifting zadd_assoc_raw)
-
-lemma zadd_0_raw:
- shows "add_raw (0, 0) z = z"
- by (simp add: add_raw_def)
-
-
-text {*also for the instance declaration int :: plus_ac0*}
-lemma zadd_0:
- fixes z::"int"
- shows "0 + z = z"
- by (lifting zadd_0_raw)
-
-lemma zadd_zminus_inverse_raw:
- shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
- by (cases z) (simp add: add_raw_def uminus_raw_def)
-
-lemma zadd_zminus_inverse2:
- fixes z::"int"
- shows "(- z) + z = 0"
- by (lifting zadd_zminus_inverse_raw)
-
-subsection{*Integer Multiplication*}
-
-lemma zmult_zminus_raw:
- shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
-apply(cases z, cases w)
-apply(simp add: uminus_raw_def)
-done
-
-lemma mult_raw_fst:
- assumes a: "intrel x z"
- shows "intrel (mult_raw x y) (mult_raw z y)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult_raw_snd:
- assumes a: "intrel x z"
- shows "intrel (mult_raw y x) (mult_raw y z)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
-
-lemma zmult_zminus:
- fixes z w::"int"
- shows "(- z) * w = - (z * w)"
- by (lifting zmult_zminus_raw)
-
-lemma zmult_commute_raw:
- shows "mult_raw z w = mult_raw w z"
-apply(cases z, cases w)
-apply(simp add: add_ac mult_ac)
-done
-
-lemma zmult_commute:
- fixes z w::"int"
- shows "z * w = w * z"
- by (lifting zmult_commute_raw)
-
-lemma zmult_assoc_raw:
- shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
-apply(cases z1, cases z2, cases z3)
-apply(simp add: add_mult_distrib2 mult_ac)
-done
-
-lemma zmult_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
- by (lifting zmult_assoc_raw)
-
-lemma zadd_mult_distrib_raw:
- shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
-apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
-done
-
-lemma zadd_zmult_distrib:
- fixes z1 z2 w::"int"
- shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
- by(lifting zadd_mult_distrib_raw)
-
-lemma zadd_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 + z2) = (w * z1) + (w * z2)"
- by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-
-lemma zdiff_zmult_distrib:
- fixes w z1 z2::"int"
- shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
- by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 - z2) = (w * z1) - (w * z2)"
- by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
-
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemma zmult_1_raw:
- shows "mult_raw (1, 0) z = z"
- by (cases z) (auto)
-
-lemma zmult_1:
- fixes z::"int"
- shows "1 * z = z"
- by (lifting zmult_1_raw)
-
-lemma zmult_1_right:
- fixes z::"int"
- shows "z * 1 = z"
- by (rule trans [OF zmult_commute zmult_1])
-
-lemma zero_not_one:
- shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
- by auto
-
-text{*The Integers Form A Ring*}
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
- show "i + j = j + i" by (simp add: zadd_commute)
- show "0 + i = i" by (rule zadd_0)
- show "- i + i = 0" by (rule zadd_zminus_inverse2)
- show "i - j = i + (-j)" by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
- show "i * j = j * i" by (rule zmult_commute)
- show "1 * i = i" by (rule zmult_1)
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by (lifting zero_not_one)
-qed
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma zle_refl_raw:
- shows "le_raw w w"
- by (cases w) (simp add: le_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> op =) le_raw le_raw"
- by (auto) (simp_all add: le_raw_def)
-
-lemma zle_refl:
- fixes w::"int"
- shows "w \<le> w"
- by (lifting zle_refl_raw)
-
-
-lemma zle_trans_raw:
- shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
-apply(cases i, cases j, cases k)
-apply(auto simp add: le_raw_def)
-done
-
-lemma zle_trans:
- fixes i j k::"int"
- shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
- by (lifting zle_trans_raw)
-
-lemma zle_anti_sym_raw:
- shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
-apply(cases z, cases w)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_anti_sym:
- fixes z w::"int"
- shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
- by (lifting zle_anti_sym_raw)
-
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le:
- fixes w z::"int"
- shows "(w < z) = (w \<le> z & w \<noteq> z)"
- by (simp add: less_int_def)
-
-instance int :: order
-apply (default)
-apply(auto simp add: zless_le zle_anti_sym)[1]
-apply(rule zle_refl)
-apply(erule zle_trans, assumption)
-apply(erule zle_anti_sym, assumption)
-done
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-
-lemma zle_linear_raw:
- shows "le_raw z w \<or> le_raw w z"
-apply(cases w, cases z)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_linear:
- fixes z w::"int"
- shows "z \<le> w \<or> w \<le> z"
- by (lifting zle_linear_raw)
-
-instance int :: linorder
-apply(default)
-apply(rule zle_linear)
-done
-
-lemma zadd_left_mono_raw:
- shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
-apply(cases k)
-apply(auto simp add: add_raw_def le_raw_def)
-done
-
-lemma zadd_left_mono:
- fixes i j::"int"
- shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting zadd_left_mono_raw)
-
-
-subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
-
-definition
- "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
- "nat2::int \<Rightarrow> nat"
-is
- "nat_raw"
-
-abbreviation
- "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
-
-lemma nat_le_eq_zle_raw:
- shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
- apply (cases w)
- apply (cases z)
- apply (simp add: nat_raw_def le_raw_def)
- by auto
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) nat_raw nat_raw"
- by (auto iff: nat_raw_def)
-
-lemma nat_le_eq_zle:
- fixes w z::"int"
- shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
- unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
-
-end
--- a/Attic/Quot/Examples/Quotient_Int.thy Thu Apr 29 17:52:19 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,379 +0,0 @@
-(* Title: HOL/Quotient_Examples/Quotient_Int.thy
- Author: Cezary Kaliszyk
- Author: Christian Urban
-
-Integers based on Quotients.
-*)
-theory Quotient_Int
-imports Quotient_Product Nat
-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 int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
-begin
-
-quotient_definition
- "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
-
-quotient_definition
- "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
-
-fun
- plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
- "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
-
-quotient_definition
- "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
-
-fun
- uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
- "uminus_int_raw (x, y) = (y, x)"
-
-quotient_definition
- "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
-
-definition
- minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
-
-fun
- times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
- "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
- "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
-
-fun
- le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
-
-quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
-
-definition
- less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
-
-definition
- zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
-
-definition
- zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
-
-instance ..
-
-end
-
-lemma [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
- and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
- and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
- by auto
-
-lemma times_int_raw_fst:
- assumes a: "x \<approx> z"
- shows "times_int_raw x y \<approx> times_int_raw z y"
- using a
- apply(cases x, cases y, cases z)
- apply(auto simp add: times_int_raw.simps intrel.simps)
- apply(rename_tac u v w x y z)
- apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
- apply(simp add: add_mult_distrib [symmetric])
- done
-
-lemma times_int_raw_snd:
- assumes a: "x \<approx> z"
- shows "times_int_raw y x \<approx> times_int_raw y z"
- using a
- apply(cases x, cases y, cases z)
- apply(auto simp add: times_int_raw.simps intrel.simps)
- apply(rename_tac u v w x y z)
- apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
- apply(simp add: add_mult_distrib [symmetric])
- done
-
-lemma [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
- apply(simp only: fun_rel_def)
- apply(rule allI | rule impI)+
- apply(rule equivp_transp[OF int_equivp])
- apply(rule times_int_raw_fst)
- apply(assumption)
- apply(rule times_int_raw_snd)
- apply(assumption)
- done
-
-lemma plus_assoc_raw:
- shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
- by (cases i, cases j, cases k) (simp)
-
-lemma plus_sym_raw:
- shows "plus_int_raw i j \<approx> plus_int_raw j i"
- by (cases i, cases j) (simp)
-
-lemma plus_zero_raw:
- shows "plus_int_raw (0, 0) i \<approx> i"
- by (cases i) (simp)
-
-lemma plus_minus_zero_raw:
- shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
- by (cases i) (simp)
-
-lemma times_assoc_raw:
- shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
- by (cases i, cases j, cases k)
- (simp add: algebra_simps)
-
-lemma times_sym_raw:
- shows "times_int_raw i j \<approx> times_int_raw j i"
- by (cases i, cases j) (simp add: algebra_simps)
-
-lemma times_one_raw:
- shows "times_int_raw (1, 0) i \<approx> i"
- by (cases i) (simp)
-
-lemma times_plus_comm_raw:
- shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
-by (cases i, cases j, cases k)
- (simp add: algebra_simps)
-
-lemma one_zero_distinct:
- shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
- by simp
-
-text{* The integers form a @{text comm_ring_1}*}
-
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)"
- by (lifting plus_assoc_raw)
- show "i + j = j + i"
- by (lifting plus_sym_raw)
- show "0 + i = (i::int)"
- by (lifting plus_zero_raw)
- show "- i + i = 0"
- by (lifting plus_minus_zero_raw)
- show "i - j = i + - j"
- by (simp add: minus_int_def)
- show "(i * j) * k = i * (j * k)"
- by (lifting times_assoc_raw)
- show "i * j = j * i"
- by (lifting times_sym_raw)
- show "1 * i = i"
- by (lifting times_one_raw)
- show "(i + j) * k = i * k + j * k"
- by (lifting times_plus_comm_raw)
- show "0 \<noteq> (1::int)"
- by (lifting one_zero_distinct)
-qed
-
-lemma plus_int_raw_rsp_aux:
- assumes a: "a \<approx> b" "c \<approx> d"
- shows "plus_int_raw a c \<approx> plus_int_raw b d"
- using a
- by (cases a, cases b, cases c, cases d)
- (simp)
-
-lemma add_abs_int:
- "(abs_int (x,y)) + (abs_int (u,v)) =
- (abs_int (x + u, y + v))"
- apply(simp add: plus_int_def id_simps)
- apply(fold plus_int_raw.simps)
- apply(rule Quotient_rel_abs[OF Quotient_int])
- apply(rule plus_int_raw_rsp_aux)
- apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
- done
-
-definition int_of_nat_raw:
- "int_of_nat_raw m = (m :: nat, 0 :: nat)"
-
-quotient_definition
- "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
-
-lemma[quot_respect]:
- shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
- by (simp add: equivp_reflp[OF int_equivp])
-
-lemma int_of_nat:
- shows "of_nat m = int_of_nat m"
- by (induct m)
- (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
-
-lemma le_antisym_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
- by (cases i, cases j) (simp)
-
-lemma le_refl_raw:
- shows "le_int_raw i i"
- by (cases i) (simp)
-
-lemma le_trans_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
- by (cases i, cases j, cases k) (simp)
-
-lemma le_cases_raw:
- shows "le_int_raw i j \<or> le_int_raw j i"
- by (cases i, cases j)
- (simp add: linorder_linear)
-
-instance int :: linorder
-proof
- fix i j k :: int
- show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
- by (lifting le_antisym_raw)
- show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
- by (auto simp add: less_int_def dest: antisym)
- show "i \<le> i"
- by (lifting le_refl_raw)
- show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
- by (lifting le_trans_raw)
- show "i \<le> j \<or> j \<le> i"
- by (lifting le_cases_raw)
-qed
-
-instantiation int :: distrib_lattice
-begin
-
-definition
- "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
-
-definition
- "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
-
-instance
- by intro_classes
- (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
-
-end
-
-lemma le_plus_int_raw:
- shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
- by (cases i, cases j, cases k) (simp)
-
-instance int :: ordered_cancel_ab_semigroup_add
-proof
- fix i j k :: int
- show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting le_plus_int_raw)
-qed
-
-abbreviation
- "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
-
-lemma zmult_zless_mono2_lemma:
- fixes i j::int
- and k::nat
- shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
- apply(induct "k")
- apply(simp)
- apply(case_tac "k = 0")
- apply(simp_all add: left_distrib add_strict_mono)
- done
-
-lemma zero_le_imp_eq_int_raw:
- fixes k::"(nat \<times> nat)"
- shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
- apply(cases k)
- apply(simp add:int_of_nat_raw)
- apply(auto)
- apply(rule_tac i="b" and j="a" in less_Suc_induct)
- apply(auto)
- done
-
-lemma zero_le_imp_eq_int:
- fixes k::int
- shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
- unfolding less_int_def int_of_nat
- by (lifting zero_le_imp_eq_int_raw)
-
-lemma zmult_zless_mono2:
- fixes i j k::int
- assumes a: "i < j" "0 < k"
- shows "k * i < k * j"
- using a
- by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
-
-text{*The integers form an ordered integral domain*}
-instance int :: linordered_idom
-proof
- fix i j k :: int
- show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
- by (rule zmult_zless_mono2)
- show "\<bar>i\<bar> = (if i < 0 then -i else i)"
- by (simp only: zabs_def)
- show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
- by (simp only: zsgn_def)
-qed
-
-lemmas int_distrib =
- left_distrib [of "z1::int" "z2" "w", standard]
- right_distrib [of "w::int" "z1" "z2", standard]
- left_diff_distrib [of "z1::int" "z2" "w", standard]
- right_diff_distrib [of "w::int" "z1" "z2", standard]
- minus_add_distrib[of "z1::int" "z2", standard]
-
-lemma int_induct_raw:
- assumes a: "P (0::nat, 0)"
- and b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
- and c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
- shows "P x"
-proof (cases x, clarify)
- fix a b
- show "P (a, b)"
- proof (induct a arbitrary: b rule: Nat.induct)
- case zero
- show "P (0, b)" using assms by (induct b) auto
- next
- case (Suc n)
- then show ?case using assms by auto
- qed
-qed
-
-lemma int_induct:
- fixes x :: int
- assumes a: "P 0"
- and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
- and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
- shows "P x"
- using a b c unfolding minus_int_def
- by (lifting int_induct_raw)
-
-text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
-
-definition
- "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
- "int_to_nat::int \<Rightarrow> nat"
-is
- "int_to_nat_raw"
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
- by (auto iff: int_to_nat_raw_def)
-
-lemma nat_le_eq_zle_raw:
- assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
- shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
- using a
- by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
-
-lemma nat_le_eq_zle:
- fixes w z::"int"
- shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
- unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
-
-end