# HG changeset patch # User Christian Urban # Date 1262386772 -3600 # Node ID ba7e81531c6d2bb17f73a288180f13bcc2b7c9c3 # Parent 6f6ee78c73574bd992b93b5ae5ac46f4f796dfcf tuned diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/Examples/LamEx.thy Fri Jan 01 23:59:32 2010 +0100 @@ -4,33 +4,44 @@ atom_decl name -thm abs_fresh(1) - -nominal_datatype rlam = +datatype rlam = rVar "name" | rApp "rlam" "rlam" | rLam "name" "rlam" -print_theorems - -function +fun rfv :: "rlam \ name set" where rfv_var: "rfv (rVar a) = {a}" | rfv_app: "rfv (rApp t1 t2) = (rfv t1) \ (rfv t2)" | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" -sorry + +overloading + perm_rlam \ "perm :: 'x prm \ rlam \ rlam" (unchecked) +begin -termination rfv sorry +fun + perm_rlam +where + "perm_rlam pi (rVar a) = rVar (pi \ a)" +| "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)" +| "perm_rlam pi (rLam a t) = rLam (pi \ a) (perm_rlam pi t)" + +end inductive alpha :: "rlam \ rlam \ bool" ("_ \ _" [100, 100] 100) where a1: "a = b \ (rVar a) \ (rVar b)" | a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" -| a3: "\t \ ([(a,b)]\s); a \ rfv (rLam b t)\ \ rLam a t \ rLam b s" +| a3: "\t \ ([(a,b)] \ s); a \ rfv (rLam b t)\ \ rLam a t \ rLam b s" -print_theorems +lemma helper: + fixes t::"rlam" + and a::"name" + shows "[(a, a)] \ t = t" +by (induct t) + (auto simp add: calc_atm) lemma alpha_refl: fixes t::"rlam" @@ -39,10 +50,7 @@ apply(simp add: a1) apply(simp add: a2) apply(rule a3) - apply(subst pt_swap_bij'') - apply(rule pt_name_inst) - apply(rule at_name_inst) - apply(simp) + apply(simp add: helper) apply(simp) done @@ -51,10 +59,8 @@ sorry quotient_type lam = rlam / alpha - apply(rule alpha_equivp) - done + by (rule alpha_equivp) -print_quotients quotient_definition "Var :: name \ lam" @@ -71,15 +77,14 @@ as "rLam" -thm Var_def -thm App_def -thm Lam_def - quotient_definition "fv :: lam \ name set" as "rfv" +thm Var_def +thm App_def +thm Lam_def thm fv_def (* definition of overloaded permutation function *) @@ -97,22 +102,36 @@ thm perm_lam_def -(* lemmas that need to lift *) -lemma pi_var_com: +(* lemmas that need to be lifted *) +lemma pi_var_eqvt1: fixes pi::"'x prm" - shows "(pi\rVar a) \ rVar (pi\a)" - sorry + shows "(pi \ rVar a) \ rVar (pi \ a)" + by (simp add: alpha_refl) -lemma pi_app_com: +lemma pi_var_eqvt2: + fixes pi::"'x prm" + shows "(pi \ rVar a) = rVar (pi \ a)" + by (simp) + +lemma pi_app_eqvt1: fixes pi::"'x prm" - shows "(pi\rApp t1 t2) \ rApp (pi\t1) (pi\t2)" - sorry + shows "(pi \ rApp t1 t2) \ rApp (pi \ t1) (pi \ t2)" + by (simp add: alpha_refl) + +lemma pi_app_eqvt2: + fixes pi::"'x prm" + shows "(pi \ rApp t1 t2) = rApp (pi \ t1) (pi \ t2)" + by (simp) -lemma pi_lam_com: +lemma pi_lam_eqvt1: fixes pi::"'x prm" - shows "(pi\rLam a t) \ rLam (pi\a) (pi\t)" - sorry + shows "(pi \ rLam a t) \ rLam (pi \ a) (pi \ t)" + by (simp add: alpha_refl) +lemma pi_lam_eqvt2: + fixes pi::"'x prm" + shows "(pi \ rLam a t) = rLam (pi \ a) (pi \ t)" + by (simp add: alpha) lemma real_alpha: @@ -136,25 +155,20 @@ lemma rVar_rsp[quot_respect]: "(op = ===> alpha) rVar rVar" -by (auto intro:a1) +by (auto intro: a1) lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp" -by (auto intro:a2) +by (auto intro: a2) lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam" apply(auto) apply(rule a3) - apply(rule_tac t="[(x,x)]\y" and s="y" in subst) - apply(rule sym) - apply(rule trans) - apply(rule pt_name3) - apply(rule at_ds1[OF at_name_inst]) - apply(simp add: pt_name1) - apply(assumption) - apply(simp add: abs_fresh) + apply(simp add: helper) + apply(simp) done -lemma rfv_rsp[quot_respect]: "(alpha ===> op =) rfv rfv" +lemma rfv_rsp[quot_respect]: + "(alpha ===> op =) rfv rfv" sorry lemma rvar_inject: "rVar a \ rVar b = (a = b)" @@ -164,76 +178,86 @@ done -lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" -apply (lifting pi_var_com) -done +lemma pi_var1: + fixes pi::"'x prm" + shows "pi \ Var a = Var (pi \ a)" + by (lifting pi_var_eqvt1) -lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" -apply (lifting pi_app_com) -done +lemma pi_var2: + fixes pi::"'x prm" + shows "pi \ Var a = Var (pi \ a)" + by (lifting pi_var_eqvt2) + -lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" -apply (lifting pi_lam_com) -done +lemma pi_app: + fixes pi::"'x prm" + shows "pi \ App t1 t2 = App (pi \ t1) (pi \ t2)" + by (lifting pi_app_eqvt2) -lemma fv_var: "fv (Var (a\name)) = {a}" -apply (lifting rfv_var) -done +lemma pi_lam: + fixes pi::"'x prm" + shows "pi \ Lam a t = Lam (pi \ a) (pi \ t)" + by (lifting pi_lam_eqvt2) -lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" -apply (lifting rfv_app) -done +lemma fv_var: + shows "fv (Var a) = {a}" + by (lifting rfv_var) -lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" -apply (lifting rfv_lam) -done +lemma fv_app: + shows "fv (App t1 t2) = fv t1 \ fv t2" + by (lifting rfv_app) + +lemma fv_lam: + shows "fv (Lam a t) = fv t - {a}" + by (lifting rfv_lam) -lemma a1: "(a\name) = (b\name) \ Var a = Var b" -apply (lifting a1) -done +lemma a1: + "a = b \ Var a = Var b" + by (lifting a1) -lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" -apply (lifting a2) -done +lemma a2: + "\x = xa; xb = xc\ \ App x xb = App xa xc" + by (lifting a2) -lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" -apply (lifting a3) -done +lemma a3: + "\x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ Lam a x = Lam b xa" + by (lifting a3) -lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; - \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; - \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ +lemma alpha_cases: + "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; + \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; + \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" -apply (lifting alpha.cases) -done + by (lifting alpha.cases) -lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); - \(x\lam) (xa\lam) (xb\lam) xc\lam. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); - \(x\lam) (a\name) (b\name) xa\lam. +lemma alpha_induct: + "\qx = qxa; \a b. a = b \ qxb (Var a) (Var b); + \x xa xb xc. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); + \x a b xa. \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ \ qxb qx qxa" -apply (lifting alpha.induct) -done + by (lifting alpha.induct) + +lemma var_inject: + "(Var a = Var b) = (a = b)" + by (lifting rvar_inject) -lemma var_inject: "(Var a = Var b) = (a = b)" -apply (lifting rvar_inject) -done - -lemma lam_induct:" \\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); - \name lam. P lam \ P (Lam name lam)\ \ P lam" -apply (lifting rlam.induct) -done +lemma lam_induct: + "\\name. P (Var name); + \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); + \name lam. P lam \ P (Lam name lam)\ \ P lam" + by (lifting rlam.induct) lemma var_supp: shows "supp (Var a) = ((supp a)::name set)" apply(simp add: supp_def) - apply(simp add: pi_var) + apply(simp add: pi_var2) apply(simp add: var_inject) done lemma var_fresh: fixes a::"name" - shows "(a\(Var b)) = (a\b)" + shows "(a \ (Var b)) = (a \ b)" apply(simp add: fresh_def) apply(simp add: var_supp) done diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/Examples/LarryDatatype.thy --- a/Quot/Examples/LarryDatatype.thy Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/Examples/LarryDatatype.thy Fri Jan 01 23:59:32 2010 +0100 @@ -51,7 +51,7 @@ theorem msgrel_imp_eq_freenonces: assumes a: "U \ V" shows "freenonces U = freenonces V" -using a by (induct) (auto) + using a by (induct) (auto) subsubsection{*The Left Projection*} @@ -70,13 +70,13 @@ (the abstract constructor) is injective*} lemma msgrel_imp_eqv_freeleft_aux: shows "freeleft U \ freeleft U" -by (induct rule: freeleft.induct) (auto) + by (induct rule: freeleft.induct) (auto) theorem msgrel_imp_eqv_freeleft: assumes a: "U \ V" shows "freeleft U \ freeleft V" -using a -by (induct)(auto intro: msgrel_imp_eqv_freeleft_aux) + using a + by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux) subsubsection{*The Right Projection*} @@ -94,13 +94,13 @@ (the abstract constructor) is injective*} lemma msgrel_imp_eqv_freeright_aux: shows "freeright U \ freeright U" -by (induct rule: freeright.induct) (auto) + by (induct rule: freeright.induct) (auto) theorem msgrel_imp_eqv_freeright: assumes a: "U \ V" shows "freeright U \ freeright V" -using a -by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) + using a + by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) subsubsection{*The Discriminator for Constructors*} @@ -117,7 +117,7 @@ theorem msgrel_imp_eq_freediscrim: assumes a: "U \ V" shows "freediscrim U = freediscrim V" -using a by (induct, auto) + using a by (induct) (auto) subsection{*The Initial Algebra: A Quotiented Message Type*} @@ -155,11 +155,13 @@ by (auto intro: DECRYPT) text{*Establishing these two equations is the point of the whole exercise*} -theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X" -by (lifting CD) +theorem CD_eq [simp]: + shows "Crypt K (Decrypt K X) = X" + by (lifting CD) -theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X" -by (lifting DC) +theorem DC_eq [simp]: + shows "Decrypt K (Crypt K X) = X" + by (lifting DC) subsection{*The Abstract Function to Return the Set of Nonces*} @@ -172,30 +174,31 @@ lemma [quot_respect]: shows "(op \ ===> op =) freenonces freenonces" -by (simp add: msgrel_imp_eq_freenonces) + by (simp add: msgrel_imp_eq_freenonces) lemma [quot_respect]: shows "(op = ===> op \) NONCE NONCE" -by (simp add: NONCE) + by (simp add: NONCE) lemma nonces_Nonce [simp]: shows "nonces (Nonce N) = {N}" -by (lifting freenonces.simps(1)) + by (lifting freenonces.simps(1)) lemma [quot_respect]: shows " (op \ ===> op \ ===> op \) MPAIR MPAIR" -by (simp add: MPAIR) + by (simp add: MPAIR) lemma nonces_MPair [simp]: shows "nonces (MPair X Y) = nonces X \ nonces Y" -by (lifting freenonces.simps(2)) + by (lifting freenonces.simps(2)) lemma nonces_Crypt [simp]: shows "nonces (Crypt K X) = nonces X" -by (lifting freenonces.simps(3)) + by (lifting freenonces.simps(3)) -lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X" -by (lifting freenonces.simps(4)) +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*} @@ -206,23 +209,23 @@ lemma [quot_respect]: shows "(op \ ===> op \) freeleft freeleft" -by (simp add: msgrel_imp_eqv_freeleft) + by (simp add: msgrel_imp_eqv_freeleft) lemma left_Nonce [simp]: shows "left (Nonce N) = Nonce N" -by (lifting freeleft.simps(1)) + by (lifting freeleft.simps(1)) lemma left_MPair [simp]: shows "left (MPair X Y) = X" -by (lifting freeleft.simps(2)) + by (lifting freeleft.simps(2)) lemma left_Crypt [simp]: shows "left (Crypt K X) = left X" -by (lifting freeleft.simps(3)) + by (lifting freeleft.simps(3)) lemma left_Decrypt [simp]: shows "left (Decrypt K X) = left X" -by (lifting freeleft.simps(4)) + by (lifting freeleft.simps(4)) subsection{*The Abstract Function to Return the Right Part*} @@ -235,29 +238,29 @@ lemma [quot_respect]: shows "(op \ ===> op \) freeright freeright" -by (simp add: msgrel_imp_eqv_freeright) + by (simp add: msgrel_imp_eqv_freeright) lemma right_Nonce [simp]: shows "right (Nonce N) = Nonce N" -by (lifting freeright.simps(1)) + by (lifting freeright.simps(1)) lemma right_MPair [simp]: shows "right (MPair X Y) = Y" -by (lifting freeright.simps(2)) + by (lifting freeright.simps(2)) lemma right_Crypt [simp]: shows "right (Crypt K X) = right X" -by (lifting freeright.simps(3)) + by (lifting freeright.simps(3)) lemma right_Decrypt [simp]: shows "right (Decrypt K X) = right X" -by (lifting freeright.simps(4)) + by (lifting freeright.simps(4)) subsection{*Injectivity Properties of Some Constructors*} lemma NONCE_imp_eq: shows "NONCE m \ NONCE n \ m = n" -by (drule msgrel_imp_eq_freenonces, simp) + by (drule msgrel_imp_eq_freenonces, simp) text{*Can also be proved using the function @{term nonces}*} lemma Nonce_Nonce_eq [iff]: @@ -272,51 +275,51 @@ lemma MPAIR_imp_eqv_left: shows "MPAIR X Y \ MPAIR X' Y' \ X \ X'" -by (drule msgrel_imp_eqv_freeleft) (simp) + 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) + using eq by (lifting MPAIR_imp_eqv_left) lemma MPAIR_imp_eqv_right: shows "MPAIR X Y \ MPAIR X' Y' \ Y \ Y'" -by (drule msgrel_imp_eqv_freeright) (simp) + by (drule msgrel_imp_eqv_freeright) (simp) lemma MPair_imp_eq_right: shows "MPair X Y = MPair X' Y' \ Y = Y'" -by (lifting MPAIR_imp_eqv_right) + 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) + by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) lemma NONCE_neqv_MPAIR: shows "\(NONCE m \ MPAIR X Y)" -by (auto dest: msgrel_imp_eq_freediscrim) + by (auto dest: msgrel_imp_eq_freediscrim) theorem Nonce_neq_MPair [iff]: shows "Nonce N \ MPair X Y" -by (lifting NONCE_neqv_MPAIR) + by (lifting NONCE_neqv_MPAIR) text{*Example suggested by a referee*} lemma CRYPT_NONCE_neq_NONCE: shows "\(CRYPT K (NONCE M) \ NONCE N)" -by (auto dest: msgrel_imp_eq_freediscrim) + by (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt_Nonce_neq_Nonce: shows "Crypt K (Nonce M) \ Nonce N" -by (lifting CRYPT_NONCE_neq_NONCE) + by (lifting CRYPT_NONCE_neq_NONCE) text{*...and many similar results*} lemma CRYPT2_NONCE_neq_NONCE: shows "\(CRYPT K (CRYPT K' (NONCE M)) \ NONCE N)" -by (auto dest: msgrel_imp_eq_freediscrim) + by (auto dest: msgrel_imp_eq_freediscrim) theorem Crypt2_Nonce_neq_Nonce: shows "Crypt K (Crypt K' (Nonce M)) \ Nonce N" -by (lifting CRYPT2_NONCE_neq_NONCE) + by (lifting CRYPT2_NONCE_neq_NONCE) theorem Crypt_Crypt_eq [iff]: shows "(Crypt K X = Crypt K X') = (X=X')" @@ -345,7 +348,7 @@ \X Y. \P X; P Y\ \ P (MPair X Y); \K X. P X \ P (Crypt K X); \K X. P X \ P (Decrypt K X)\ \ P msg" -by (lifting freemsg.induct) + by (lifting freemsg.induct) lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: assumes N: "\N. P (Nonce N)" @@ -353,7 +356,7 @@ and C: "\K X. P X \ P (Crypt K X)" and D: "\K X. P X \ P (Decrypt K X)" shows "P msg" -using N M C D by (rule msg_induct_aux) + using N M C D by (rule msg_induct_aux) subsection{*The Abstract Discriminator*} @@ -369,23 +372,23 @@ lemma [quot_respect]: shows "(op \ ===> op =) freediscrim freediscrim" -by (auto simp add: msgrel_imp_eq_freediscrim) + by (auto simp add: msgrel_imp_eq_freediscrim) lemma discrim_Nonce [simp]: shows "discrim (Nonce N) = 0" -by (lifting freediscrim.simps(1)) + by (lifting freediscrim.simps(1)) lemma discrim_MPair [simp]: shows "discrim (MPair X Y) = 1" -by (lifting freediscrim.simps(2)) + by (lifting freediscrim.simps(2)) lemma discrim_Crypt [simp]: shows "discrim (Crypt K X) = discrim X + 2" -by (lifting freediscrim.simps(3)) + by (lifting freediscrim.simps(3)) lemma discrim_Decrypt [simp]: shows "discrim (Decrypt K X) = discrim X - 2" -by (lifting freediscrim.simps(4)) + by (lifting freediscrim.simps(4)) end diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/Examples/LarryInt.thy --- a/Quot/Examples/LarryInt.thy Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/Examples/LarryInt.thy Fri Jan 01 23:59:32 2010 +0100 @@ -76,18 +76,18 @@ shows "(intrel ===> intrel) uminus_raw uminus_raw" by (simp add: uminus_raw_def) -lemma zminus_zminus: - shows "- (- z) = (z::int)" -apply(lifting zminus_zminus_raw) -done +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) + by (simp add: uminus_raw_def) -lemma zminus_0: "- 0 = (0::int)" -apply(lifting zminus_0_raw) -done +lemma zminus_0: + shows "- 0 = (0::int)" + by (lifting zminus_0_raw) subsection{*Integer Addition*} @@ -101,9 +101,9 @@ by (simp add: add_raw_def) lemma zminus_zadd_distrib: - shows "- (z + w) = (- z) + (- w::int)" -apply(lifting zminus_zadd_distrib_raw) -done + 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" @@ -111,43 +111,45 @@ (simp add: add_raw_def) lemma zadd_commute: + fixes z w::"int" shows "(z::int) + w = w + z" -apply(lifting zadd_commute_raw) -done + 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) + by (cases z1, cases z2, cases z3) (simp add: add_raw_def) -lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)" -apply(lifting zadd_assoc_raw) -done +lemma zadd_assoc: + fixes z1 z2 z3::"int" + shows "(z1 + z2) + z3 = z1 + (z2 + z3)" + by (lifting zadd_assoc_raw) lemma zadd_0_raw: - fixes z::"nat \ nat" shows "add_raw (0, 0) z = z" -by (simp add: add_raw_def) + by (simp add: add_raw_def) -(*also for the instance declaration int :: plus_ac0*) -lemma zadd_0: "(0::int) + z = z" -apply(lifting zadd_0_raw) -done +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) + by (cases z) (simp add: add_raw_def uminus_raw_def) -lemma zadd_zminus_inverse2: "(- z) + z = (0::int)" -apply(lifting zadd_zminus_inverse_raw) -done +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) +apply(simp add: uminus_raw_def) done lemma mult_raw_fst: @@ -185,9 +187,10 @@ apply(assumption) done -lemma zmult_zminus: "(- z) * w = - (z * (w::int))" -apply(lifting zmult_zminus_raw) -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" @@ -195,8 +198,10 @@ apply(simp add: add_ac mult_ac) done -lemma zmult_commute: "(z::int) * w = w * z" -by (lifting zmult_commute_raw) +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)" @@ -204,8 +209,10 @@ apply(simp add: add_mult_distrib2 mult_ac) done -lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)" -by (lifting zmult_assoc_raw) +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)" @@ -213,18 +220,25 @@ apply(simp add: add_mult_distrib2 mult_ac add_raw_def) done -lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)" -apply(lifting zadd_mult_distrib_raw) -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 zadd_zmult_distrib2: "(w::int) * (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_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)" -by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus) - -lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)" -by (simp add: zmult_commute [of w] zdiff_zmult_distrib) +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 @@ -232,20 +246,21 @@ lemma zmult_1_raw: shows "mult_raw (1, 0) z = z" -apply(cases z) -apply(auto) -done + by (cases z) (auto) -lemma zmult_1: "(1::int) * z = z" -apply(lifting zmult_1_raw) -done +lemma zmult_1: + fixes z::"int" + shows "1 * z = z" + by (lifting zmult_1_raw) -lemma zmult_1_right: "z * (1::int) = z" -by (rule trans [OF zmult_commute zmult_1]) +lemma zmult_1_right: + fixes z::"int" + shows "z * 1 = z" + by (rule trans [OF zmult_commute zmult_1]) lemma zero_not_one: shows "\(intrel (0, 0) (1::nat, 0::nat))" -by auto + by auto text{*The Integers Form A Ring*} instance int :: comm_ring_1 @@ -267,29 +282,29 @@ subsection{*The @{text "\"} Ordering*} lemma zle_refl_raw: - "le_raw w w" -apply(cases w) -apply(simp add: le_raw_def) -done + 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) + by (auto) (simp_all add: le_raw_def) -lemma zle_refl: "w \ (w::int)" -apply(lifting zle_refl_raw) -done +lemma zle_refl: + fixes w::"int" + shows "w \ w" + by (lifting zle_refl_raw) + lemma zle_trans_raw: shows "\le_raw i j; le_raw j k\ \ le_raw i k" apply(cases i, cases j, cases k) -apply(auto) -apply(simp add:le_raw_def) +apply(auto simp add: le_raw_def) done -lemma zle_trans: "\i \ j; j \ k\ \ i \ (k::int)" -apply(lifting zle_trans_raw) -done +lemma zle_trans: + fixes i j k::"int" + shows "\i \ j; j \ k\ \ i \ k" + by (lifting zle_trans_raw) lemma zle_anti_sym_raw: shows "\le_raw z w; le_raw w z\ \ intrel z w" @@ -297,34 +312,43 @@ apply(auto iff: le_raw_def) done -lemma zle_anti_sym: "\z \ w; w \ z\ \ z = (w::int)" -apply(lifting zle_anti_sym_raw) -done +lemma zle_anti_sym: + fixes z w::"int" + shows "\z \ w; w \ z\ \ z = w" + by (lifting zle_anti_sym_raw) + (* Axiom 'order_less_le' of class 'order': *) -lemma zless_le: "((w::int) < z) = (w \ z & w \ z)" -by (simp add: less_int_def) +lemma zless_le: + fixes w z::"int" + shows "(w < z) = (w \ z & w \ z)" + by (simp add: less_int_def) instance int :: order -apply(intro_classes) -apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def) +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: - "le_raw z w \ le_raw w z" + shows "le_raw z w \ le_raw w z" apply(cases w, cases z) apply(auto iff: le_raw_def) done - -lemma zle_linear: "(z::int) \ w \ w \ z" -apply(lifting zle_linear_raw) -done +lemma zle_linear: + fixes z w::"int" + shows "z \ w \ w \ z" + by (lifting zle_linear_raw) instance int :: linorder -proof qed (rule zle_linear) +apply(default) +apply(rule zle_linear) +done lemma zadd_left_mono_raw: shows "le_raw i j \ le_raw (add_raw k i) (add_raw k j)" @@ -332,10 +356,10 @@ apply(auto simp add: add_raw_def le_raw_def) done -lemma zadd_left_mono: "i \ j \ k + i \ k + (j::int)" -apply(lifting zadd_left_mono_raw) -done - +lemma zadd_left_mono: + fixes i j::"int" + shows "i \ j \ k + i \ k + j" + by (lifting zadd_left_mono_raw) subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} @@ -344,7 +368,7 @@ "nat_raw \ \(x, y).x - (y::nat)" quotient_definition - "nat2::int\nat" + "nat2::int \ nat" as "nat_raw" @@ -358,12 +382,12 @@ lemma [quot_respect]: shows "(intrel ===> op =) nat_raw nat_raw" -apply(auto iff: nat_raw_def) -done + by (auto iff: nat_raw_def) -lemma nat_le_eq_zle: "0 < w \ 0 \ z \ (nat2 w \ nat2 z) = (w\z)" -unfolding less_int_def -apply(lifting nat_le_eq_zle_raw) -done +lemma nat_le_eq_zle: + fixes w z::"int" + shows "0 < w \ 0 \ z \ (nat2 w \ nat2 z) = (w\z)" + unfolding less_int_def + by (lifting nat_le_eq_zle_raw) end diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_def.ML --- a/Quot/quotient_def.ML Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/quotient_def.ML Fri Jan 01 23:59:32 2010 +0100 @@ -26,15 +26,15 @@ (* interface and syntax setup *) -(* the ML-interface takes a 4-tuple consisting of *) -(* *) -(* - the mixfix annotation *) -(* - name and attributes *) -(* - the new constant including its type *) -(* - the rhs of the definition *) -(* *) -(* returns the defined constant and its definition *) -(* theorem; stores the data in the qconsts slot *) +(* the ML-interface takes a 4-tuple consisting of *) +(* *) +(* - the mixfix annotation *) +(* - name and attributes *) +(* - the new constant as term *) +(* - the rhs of the definition as term *) +(* *) +(* it returns the defined constant and its definition *) +(* theorem; stores the data in the qconsts slot *) fun quotient_def mx attr lhs rhs lthy = let @@ -55,10 +55,10 @@ ((trm, thm), lthy'') end -fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = +fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = let - val lhs = Syntax.read_term lthy lhsstr - val rhs = Syntax.read_term lthy rhsstr + val lhs = Syntax.read_term lthy lhs_str + val rhs = Syntax.read_term lthy rhs_str in quotient_def mx attr lhs rhs lthy |> snd end diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/quotient_tacs.ML Fri Jan 01 23:59:32 2010 +0100 @@ -39,7 +39,7 @@ fun atomize_thm thm = let - val thm' = Thm.freezeT (forall_intr_vars thm) (* TODO: is this proper Isar-technology? *) + val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) val thm'' = ObjectLogic.atomize (cprop_of thm') in @{thm equal_elim_rule1} OF [thm'', thm'] @@ -60,7 +60,7 @@ val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac (* FIXME / TODO: test whether DETERM makes any runtime-difference *) -(* FIXME / TODO: reason: it might back-track over the two alternatives in FIRST' *) +(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) fun quotient_tac ctxt = SOLVES' (REPEAT_ALL_NEW (FIRST' [rtac @{thm identity_quotient}, @@ -84,15 +84,15 @@ fun get_match_inst thy pat trm = let val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) + val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) in (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) end -(* calculates the instantiations for te lemmas *) -(* ball_reg_eqv_range and bex_reg_eqv_range *) +(* calculates the instantiations for the lemmas *) +(* ball_reg_eqv_range and bex_reg_eqv_range *) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) @@ -106,11 +106,11 @@ SOME thm'' end handle _ => NONE -(* FIXME/TODO: !!!CLEVER CODE!!! *) -(* FIXME/TODO: What is the place where the exception is raised, *) -(* FIXME/TODO: and which exception is it? *) -(* FIXME/TODO: Can one not find out from the types of R1 or R2, *) -(* FIXME/TODO: or from their form, when NONE should be returned? *) +(* FIXME/TODO: !!!CLEVER CODE!!! *) +(* FIXME/TODO: What are the places where the exceptions are raised, *) +(* FIXME/TODO: and which exception is it? *) +(* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *) +(* FIXME/TODO: when NONE should be returned? *) fun ball_bex_range_simproc ss redex = let @@ -231,10 +231,9 @@ val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl - -(* We apply apply_rsp only in case if the type needs lifting. *) -(* This is the case if the type of the data in the Quot_True *) -(* assumption is different from the corresponding type in the goal *) +(* We apply apply_rsp only in case if the type needs lifting. *) +(* This is the case if the type of the data in the Quot_True *) +(* assumption is different from the corresponding type in the goal. *) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => let @@ -269,13 +268,13 @@ in rtac thm THEN' quotient_tac ctxt end -(* TODO: Are they raised by instantiate'? *) -(* TODO: Again, can one specify more concretely when no_tac should be returned? *) +(* TODO: Are they raised by instantiate'? *) +(* TODO: Again, can one specify more concretely *) +(* TODO: in terms of R when no_tac should be returned? *) handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac - fun rep_abs_rsp_tac ctxt = SUBGOAL (fn (goal, i) => case (bare_concl goal) of @@ -564,16 +563,16 @@ (* The General Shape of the Lifting Procedure *) (**********************************************) -(* - A is the original raw theorem *) -(* - B is the regularized theorem *) -(* - C is the rep/abs injected version of B *) -(* - D is the lifted theorem *) -(* *) -(* - 1st prem is the regularization step *) -(* - 2nd prem is the rep/abs injection step *) -(* - 3rd prem is the cleaning part *) -(* *) -(* the Quot_True premise in 2 records the lifted theorem *) +(* - A is the original raw theorem *) +(* - B is the regularized theorem *) +(* - C is the rep/abs injected version of B *) +(* - D is the lifted theorem *) +(* *) +(* - 1st prem is the regularization step *) +(* - 2nd prem is the rep/abs injection step *) +(* - 3rd prem is the cleaning part *) +(* *) +(* the Quot_True premise in 2nd records the lifted theorem *) val lifting_procedure_thm = @{lemma "[|A; diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_term.ML --- a/Quot/quotient_term.ML Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/quotient_term.ML Fri Jan 01 23:59:32 2010 +0100 @@ -72,7 +72,7 @@ TVar _ => mk_Free rty | Type (_, []) => mk_identity rty | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) - | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") + | _ => raise LIFT_MATCH ("mk_mapfun (default)") in fold_rev Term.lambda vs' (mk_mapfun_aux rty) end @@ -120,13 +120,13 @@ (* produces an aggregate absrep function *) (* *) -(* - In case of equal types we just return the identity *) +(* - In case of equal types we just return the identity. *) (* *) (* - In case of function types and TFrees, we recurse, taking in *) (* the first case the polarity change into account. *) (* *) (* - If the type constructors are equal, we recurse for the *) -(* arguments and prefix the appropriate map function *) +(* arguments and build the appropriate map function. *) (* *) (* - If the type constructors are unequal, there must be an *) (* instance of quotient types: *) @@ -135,12 +135,12 @@ (* must be some distinct TVars *) (* - we then match the rty_pat with rty and qty_pat with qty; *) (* if matching fails the types do not match *) -(* - the matching produces two environments, we look up the *) +(* - the matching produces two environments; we look up the *) (* assignments for the qty_pat variables and recurse on the *) -(* assignmetnts *) +(* assignments *) (* - we prefix the aggregate map function for the rty_pat, *) (* which is an abstraction over all type variables *) -(* - finally we compse the result with the appropriate *) +(* - finally we compose the result with the appropriate *) (* absrep function *) (* *) (* The composition is necessary for types like *) diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Fri Jan 01 11:30:00 2010 +0100 +++ b/Quot/quotient_typ.ML Fri Jan 01 23:59:32 2010 +0100 @@ -218,8 +218,8 @@ (* - the type to be quotient *) (* - the relation according to which the type is quotient *) (* *) -(* opens a proof-state in which one has to show that the *) -(* relation is an equivalence relation *) +(* it opens a proof-state in which one has to show that the *) +(* relations are equivalence relations *) fun quotient_type quot_list lthy = let