# HG changeset patch # User wenzelm # Date 1272556211 -7200 # Node ID 2584289edbb078f29be113dd7ee46048c27258ed # Parent 3909002beca5afb8b2fb6dffe1052f43739c6fc4# Parent 03d2a2d0ee4a25f463518ce0c74357f846cc5672 merged diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/FunDef.thy Thu Apr 29 17:50:11 2010 +0200 @@ -314,8 +314,8 @@ ML_val -- "setup inactive" {* - Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp - [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) + Context.theory_map (Function_Common.set_termination_prover + (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) *} end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/IsaMakefile Thu Apr 29 17:50:11 2010 +0200 @@ -1295,8 +1295,8 @@ HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ - Quotient_Examples/FSet.thy \ - Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy + Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \ + Quotient_Examples/Quotient_Message.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Lazy_Sequence.thy Thu Apr 29 17:50:11 2010 +0200 @@ -123,6 +123,13 @@ subsection {* Code setup *} +code_reflect + datatypes lazy_sequence = Lazy_Sequence + functions map yield + module_name Lazy_Sequence + +(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *) + ML {* signature LAZY_SEQUENCE = sig @@ -130,14 +137,15 @@ val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence) val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence + val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence end; structure Lazy_Sequence : LAZY_SEQUENCE = struct -@{code_datatype lazy_sequence = Lazy_Sequence} +open Lazy_Sequence; -val yield = @{code yield} +fun map f = mapa f; fun anamorph f k x = (if k = 0 then ([], x) else case f x @@ -148,17 +156,9 @@ fun yieldn S = anamorph yield S; -val map = @{code map} - end; *} -code_reserved Eval Lazy_Sequence - -code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence") - -code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence") - section {* With Hit Bound Value *} text {* assuming in negative context *} diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Predicate.thy Thu Apr 29 17:50:11 2010 +0200 @@ -880,6 +880,11 @@ code_abort not_unique +code_reflect + datatypes pred = Seq and seq = Empty | Insert | Join + functions map + module_name Predicate + ML {* signature PREDICATE = sig @@ -893,15 +898,17 @@ structure Predicate : PREDICATE = struct -@{code_datatype pred = Seq}; -@{code_datatype seq = Empty | Insert | Join}; +datatype pred = datatype Predicate.pred +datatype seq = datatype Predicate.seq + +fun map f = Predicate.map f; -fun yield (@{code Seq} f) = next (f ()) -and next @{code Empty} = NONE - | next (@{code Insert} (x, P)) = SOME (x, P) - | next (@{code Join} (P, xq)) = (case yield P +fun yield (Seq f) = next (f ()) +and next Empty = NONE + | next (Insert (x, P)) = SOME (x, P) + | next (Join (P, xq)) = (case yield P of NONE => next xq - | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq)))); + | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq)))); fun anamorph f k x = (if k = 0 then ([], x) else case f x @@ -912,19 +919,9 @@ fun yieldn P = anamorph yield P; -fun map f = @{code map} f; - end; *} -code_reserved Eval Predicate - -code_type pred and seq - (Eval "_/ Predicate.pred" and "_/ Predicate.seq") - -code_const Seq and Empty and Insert and Join - (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") - no_notation inf (infixl "\" 70) and sup (infixl "\" 65) and diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Apr 29 17:50:11 2010 +0200 @@ -686,6 +686,13 @@ (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *) +subsection {* Free function variable *} + +inductive FF :: "nat => nat => bool" +where + "f x = y ==> FF x y" + +code_pred FF . subsection {* IMP *} diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Thu Apr 29 17:50:11 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Quotient_Examples/Quotient.thy +(* Title: HOL/Quotient_Examples/FSet.thy Author: Cezary Kaliszyk, TU Munich Author: Christian Urban, TU Munich diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/LarryDatatype.thy --- a/src/HOL/Quotient_Examples/LarryDatatype.thy Thu Apr 29 17:47:53 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,394 +0,0 @@ -theory LarryDatatype -imports Main Quotient_Syntax -begin - -subsection{*Defining the Free Algebra*} - -datatype - freemsg = NONCE nat - | MPAIR freemsg freemsg - | CRYPT nat freemsg - | DECRYPT nat freemsg - -inductive - msgrel::"freemsg \ freemsg \ bool" (infixl "\" 50) -where - CD: "CRYPT K (DECRYPT K X) \ X" -| DC: "DECRYPT K (CRYPT K X) \ X" -| NONCE: "NONCE N \ NONCE N" -| MPAIR: "\X \ X'; Y \ Y'\ \ MPAIR X Y \ MPAIR X' Y'" -| CRYPT: "X \ X' \ CRYPT K X \ CRYPT K X'" -| DECRYPT: "X \ X' \ DECRYPT K X \ DECRYPT K X'" -| SYM: "X \ Y \ Y \ X" -| TRANS: "\X \ Y; Y \ Z\ \ X \ Z" - -lemmas msgrel.intros[intro] - -text{*Proving that it is an equivalence relation*} - -lemma msgrel_refl: "X \ 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 \ nat set" -where - "freenonces (NONCE N) = {N}" -| "freenonces (MPAIR X Y) = freenonces X \ freenonces Y" -| "freenonces (CRYPT K X) = freenonces X" -| "freenonces (DECRYPT K X) = freenonces X" - -theorem msgrel_imp_eq_freenonces: - assumes a: "U \ 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 \ 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 \ freeleft U" - 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) - -subsubsection{*The Right Projection*} - -text{*A function to return the right part of the top pair in a message.*} -fun - freeright :: "freemsg \ 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 \ freeright U" - 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) - -subsubsection{*The Discriminator for Constructors*} - -text{*A function to distinguish nonces, mpairs and encryptions*} -fun - freediscrim :: "freemsg \ 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 \ MPair X Y"}*} -theorem msgrel_imp_eq_freediscrim: - assumes a: "U \ 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 \ msg" -is - "NONCE" - -quotient_definition - "MPair :: msg \ msg \ msg" -is - "MPAIR" - -quotient_definition - "Crypt :: nat \ msg \ msg" -is - "CRYPT" - -quotient_definition - "Decrypt :: nat \ msg \ msg" -is - "DECRYPT" - -lemma [quot_respect]: - shows "(op = ===> op \ ===> op \) CRYPT CRYPT" -by (auto intro: CRYPT) - -lemma [quot_respect]: - shows "(op = ===> op \ ===> op \) 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 \ nat set" -is - "freenonces" - -text{*Now prove the four equations for @{term nonces}*} - -lemma [quot_respect]: - shows "(op \ ===> op =) freenonces freenonces" - by (simp add: msgrel_imp_eq_freenonces) - -lemma [quot_respect]: - shows "(op = ===> op \) 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 \ ===> op \ ===> op \) MPAIR MPAIR" - by (simp add: MPAIR) - -lemma nonces_MPair [simp]: - shows "nonces (MPair X Y) = nonces X \ 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 \ msg" -is - "freeleft" - -lemma [quot_respect]: - shows "(op \ ===> op \) 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 \ msg" -is - "freeright" - -text{*Now prove the four equations for @{term right}*} - -lemma [quot_respect]: - shows "(op \ ===> op \) 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 \ NONCE n \ 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 \ MPAIR X' Y' \ X \ 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 \ MPAIR X' Y' \ Y \ Y'" - 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) - -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 "\(NONCE m \ MPAIR X Y)" - by (auto dest: msgrel_imp_eq_freediscrim) - -theorem Nonce_neq_MPair [iff]: - shows "Nonce N \ MPair X Y" - 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) - -theorem Crypt_Nonce_neq_Nonce: - shows "Crypt K (Nonce M) \ Nonce N" - 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) - -theorem Crypt2_Nonce_neq_Nonce: - shows "Crypt K (Crypt K' (Nonce M)) \ 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 "\\N. P (Nonce N); - \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) - -lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: - assumes N: "\N. P (Nonce N)" - and M: "\X Y. \P X; P Y\ \ P (MPair X Y)" - 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) - -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 \ int" -is - "freediscrim" - -text{*Now prove the four equations for @{term discrim}*} - -lemma [quot_respect]: - shows "(op \ ===> 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 - diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/LarryInt.thy --- a/src/HOL/Quotient_Examples/LarryInt.thy Thu Apr 29 17:47:53 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 Main Quotient_Product -begin - -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient_type int = "nat \ 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 \ \(x, y) (u, v). (x + (u::nat), y + (v::nat))" - -quotient_definition - "(op +) :: int \ int \ int" -is - "add_raw" - -definition - "uminus_raw \ \(x::nat, y::nat). (y, x)" - -quotient_definition - "uminus :: int \ int" -is - "uminus_raw" - -fun - mult_raw::"nat \ nat \ nat \ nat \ nat \ nat" -where - "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" - -quotient_definition - "(op *) :: int \ int \ int" -is - "mult_raw" - -definition - "le_raw \ \(x, y) (u, v). (x+v \ u+(y::nat))" - -quotient_definition - le_int_def: "(op \) :: int \ int \ bool" -is - "le_raw" - -definition - less_int_def: "z < (w::int) \ (z \ w & z \ w)" - -definition - diff_int_def: "z - (w::int) \ 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 "\(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 \ (1::int)" by (lifting zero_not_one) -qed - - -subsection{*The @{text "\"} 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 \ 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 simp add: le_raw_def) -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" -apply(cases z, cases w) -apply(auto iff: le_raw_def) -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: - fixes w z::"int" - shows "(w < z) = (w \ z & w \ 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 \ 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 \ w \ w \ 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 \ 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 \ j \ k + i \ k + j" - by (lifting zadd_left_mono_raw) - - -subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} - -definition - "nat_raw \ \(x, y).x - (y::nat)" - -quotient_definition - "nat2::int \ nat" -is - "nat_raw" - -abbreviation - "less_raw x y \ (le_raw x y \ \(intrel x y))" - -lemma nat_le_eq_zle_raw: - shows "less_raw (0, 0) w \ le_raw (0, 0) z \ (nat_raw w \ 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 \ 0 \ z \ (nat2 w \ nat2 z) = (w\z)" - unfolding less_int_def - by (lifting nat_le_eq_zle_raw) - -end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/Quotient_Int.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Apr 29 17:50:11 2010 +0200 @@ -0,0 +1,380 @@ +(* Title: HOL/Quotient_Examples/Quotient_Int.thy + Author: Cezary Kaliszyk + Author: Christian Urban + +Integers based on Quotients, based on an older version by Larry Paulson. +*) +theory Quotient_Int +imports Quotient_Product Nat +begin + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type int = "nat \ 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 \ int" is "(0\nat, 0\nat)" + +quotient_definition + "1 \ int" is "(1\nat, 0\nat)" + +fun + plus_int_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "plus_int_raw (x, y) (u, v) = (x + u, y + v)" + +quotient_definition + "(op +) \ (int \ int \ int)" is "plus_int_raw" + +fun + uminus_int_raw :: "(nat \ nat) \ (nat \ nat)" +where + "uminus_int_raw (x, y) = (y, x)" + +quotient_definition + "(uminus \ (int \ int))" is "uminus_int_raw" + +definition + minus_int_def [code del]: "z - w = z + (-w\int)" + +fun + times_int_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" + +quotient_definition + "(op *) :: (int \ int \ int)" is "times_int_raw" + +fun + le_int_raw :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "le_int_raw (x, y) (u, v) = (x+v \ u+y)" + +quotient_definition + le_int_def: "(op \) :: int \ int \ bool" is "le_int_raw" + +definition + less_int_def [code del]: "(z\int) < w = (z \ w \ z \ w)" + +definition + zabs_def: "\i\int\ = (if i < 0 then - i else i)" + +definition + zsgn_def: "sgn (i\int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)" + +instance .. + +end + +lemma [quot_respect]: + shows "(op \ ===> op \ ===> op \) plus_int_raw plus_int_raw" + and "(op \ ===> op \) uminus_int_raw uminus_int_raw" + and "(op \ ===> op \ ===> op =) le_int_raw le_int_raw" + by auto + +lemma times_int_raw_fst: + assumes a: "x \ z" + shows "times_int_raw x y \ 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 \ z" + shows "times_int_raw y x \ 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 \ ===> op \ ===> op \) 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 \ 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 \ plus_int_raw j i" + by (cases i, cases j) (simp) + +lemma plus_zero_raw: + shows "plus_int_raw (0, 0) i \ i" + by (cases i) (simp) + +lemma plus_minus_zero_raw: + shows "plus_int_raw (uminus_int_raw i) i \ (0, 0)" + by (cases i) (simp) + +lemma times_assoc_raw: + shows "times_int_raw (times_int_raw i j) k \ 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 \ 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 \ i" + by (cases i) (simp) + +lemma times_plus_comm_raw: + shows "times_int_raw (plus_int_raw i j) k \ 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 "\ (0, 0) \ ((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 \ (1::int)" + by (lifting one_zero_distinct) +qed + +lemma plus_int_raw_rsp_aux: + assumes a: "a \ b" "c \ d" + shows "plus_int_raw a c \ 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 \ int" is "int_of_nat_raw" + +lemma[quot_respect]: + shows "(op = ===> op \) 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 \ le_int_raw j i \ i \ 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 \ le_int_raw j k \ le_int_raw i k" + by (cases i, cases j, cases k) (simp) + +lemma le_cases_raw: + shows "le_int_raw i j \ 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 \ j \ j \ i \ i = j" + by (lifting le_antisym_raw) + show "(i < j) = (i \ j \ \ j \ i)" + by (auto simp add: less_int_def dest: antisym) + show "i \ i" + by (lifting le_refl_raw) + show "i \ j \ j \ k \ i \ k" + by (lifting le_trans_raw) + show "i \ j \ j \ i" + by (lifting le_cases_raw) +qed + +instantiation int :: distrib_lattice +begin + +definition + "(inf \ int \ int \ int) = min" + +definition + "(sup \ int \ int \ int) = max" + +instance + by default + (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 \ 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 \ j \ k + i \ k + j" + by (lifting le_plus_int_raw) +qed + +abbreviation + "less_int_raw i j \ le_int_raw i j \ \(i \ j)" + +lemma zmult_zless_mono2_lemma: + fixes i j::int + and k::nat + shows "i < j \ 0 < k \ 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 \ nat)" + shows "less_int_raw (0, 0) k \ (\n > 0. k \ 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 \ \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 \ 0 < k \ k * i < k * j" + by (rule zmult_zless_mono2) + show "\i\ = (if i < 0 then -i else i)" + by (simp only: zabs_def) + show "sgn (i\int) = (if i=0 then 0 else if 0i. P i \ P (plus_int_raw i (1, 0))" + and c: "\i. P i \ 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: "\i. P i \ P (i + 1)" + and c: "\i. P i \ 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 \ \(x, y).x - (y::nat)" + +quotient_definition + "int_to_nat::int \ 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 \ le_int_raw (0, 0) z" + shows "(int_to_nat_raw w \ 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 \ 0 \ z \ (int_to_nat w \ int_to_nat z) = (w \ z)" + unfolding less_int_def + by (lifting nat_le_eq_zle_raw) + +end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/Quotient_Message.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Apr 29 17:50:11 2010 +0200 @@ -0,0 +1,399 @@ +(* Title: HOL/Quotient_Examples/Quotient_Message.thy + Author: Christian Urban + +Message datatype, based on an older version by Larry Paulson. +*) +theory Quotient_Message +imports Main Quotient_Syntax +begin + +subsection{*Defining the Free Algebra*} + +datatype + freemsg = NONCE nat + | MPAIR freemsg freemsg + | CRYPT nat freemsg + | DECRYPT nat freemsg + +inductive + msgrel::"freemsg \ freemsg \ bool" (infixl "\" 50) +where + CD: "CRYPT K (DECRYPT K X) \ X" +| DC: "DECRYPT K (CRYPT K X) \ X" +| NONCE: "NONCE N \ NONCE N" +| MPAIR: "\X \ X'; Y \ Y'\ \ MPAIR X Y \ MPAIR X' Y'" +| CRYPT: "X \ X' \ CRYPT K X \ CRYPT K X'" +| DECRYPT: "X \ X' \ DECRYPT K X \ DECRYPT K X'" +| SYM: "X \ Y \ Y \ X" +| TRANS: "\X \ Y; Y \ Z\ \ X \ Z" + +lemmas msgrel.intros[intro] + +text{*Proving that it is an equivalence relation*} + +lemma msgrel_refl: "X \ 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 \ nat set" +where + "freenonces (NONCE N) = {N}" +| "freenonces (MPAIR X Y) = freenonces X \ freenonces Y" +| "freenonces (CRYPT K X) = freenonces X" +| "freenonces (DECRYPT K X) = freenonces X" + +theorem msgrel_imp_eq_freenonces: + assumes a: "U \ 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 \ 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 \ freeleft U" + 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) + +subsubsection{*The Right Projection*} + +text{*A function to return the right part of the top pair in a message.*} +fun + freeright :: "freemsg \ 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 \ freeright U" + 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) + +subsubsection{*The Discriminator for Constructors*} + +text{*A function to distinguish nonces, mpairs and encryptions*} +fun + freediscrim :: "freemsg \ 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 \ MPair X Y"}*} +theorem msgrel_imp_eq_freediscrim: + assumes a: "U \ 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 \ msg" +is + "NONCE" + +quotient_definition + "MPair :: msg \ msg \ msg" +is + "MPAIR" + +quotient_definition + "Crypt :: nat \ msg \ msg" +is + "CRYPT" + +quotient_definition + "Decrypt :: nat \ msg \ msg" +is + "DECRYPT" + +lemma [quot_respect]: + shows "(op = ===> op \ ===> op \) CRYPT CRYPT" +by (auto intro: CRYPT) + +lemma [quot_respect]: + shows "(op = ===> op \ ===> op \) 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 \ nat set" +is + "freenonces" + +text{*Now prove the four equations for @{term nonces}*} + +lemma [quot_respect]: + shows "(op \ ===> op =) freenonces freenonces" + by (simp add: msgrel_imp_eq_freenonces) + +lemma [quot_respect]: + shows "(op = ===> op \) 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 \ ===> op \ ===> op \) MPAIR MPAIR" + by (simp add: MPAIR) + +lemma nonces_MPair [simp]: + shows "nonces (MPair X Y) = nonces X \ 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 \ msg" +is + "freeleft" + +lemma [quot_respect]: + shows "(op \ ===> op \) 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 \ msg" +is + "freeright" + +text{*Now prove the four equations for @{term right}*} + +lemma [quot_respect]: + shows "(op \ ===> op \) 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 \ NONCE n \ 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 \ MPAIR X' Y' \ X \ 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 \ MPAIR X' Y' \ Y \ Y'" + 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) + +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 "\(NONCE m \ MPAIR X Y)" + by (auto dest: msgrel_imp_eq_freediscrim) + +theorem Nonce_neq_MPair [iff]: + shows "Nonce N \ MPair X Y" + 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) + +theorem Crypt_Nonce_neq_Nonce: + shows "Crypt K (Nonce M) \ Nonce N" + 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) + +theorem Crypt2_Nonce_neq_Nonce: + shows "Crypt K (Crypt K' (Nonce M)) \ 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 "\\N. P (Nonce N); + \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) + +lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: + assumes N: "\N. P (Nonce N)" + and M: "\X Y. \P X; P Y\ \ P (MPair X Y)" + 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) + +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 \ int" +is + "freediscrim" + +text{*Now prove the four equations for @{term discrim}*} + +lemma [quot_respect]: + shows "(op \ ===> 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 + diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 29 17:50:11 2010 +0200 @@ -4,5 +4,5 @@ Testing the quotient package. *) -use_thys ["FSet", "LarryInt", "LarryDatatype"]; +use_thys ["FSet", "Quotient_Int", "Quotient_Message"]; diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Function/fun.ML Thu Apr 29 17:50:11 2010 +0200 @@ -7,12 +7,12 @@ signature FUNCTION_FUN = sig - val add_fun : Function_Common.function_config -> - (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> - bool -> local_theory -> Proof.context - val add_fun_cmd : Function_Common.function_config -> - (binding * string option * mixfix) list -> (Attrib.binding * string) list -> - bool -> local_theory -> Proof.context + val add_fun : (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> Function_Common.function_config -> + local_theory -> Proof.context + val add_fun_cmd : (binding * string option * mixfix) list -> + (Attrib.binding * string) list -> Function_Common.function_config -> + local_theory -> Proof.context val setup : theory -> theory end @@ -56,15 +56,6 @@ () end -val by_pat_completeness_auto = - Proof.global_future_terminal_proof - (Method.Basic Pat_Completeness.pat_completeness, - SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) - -fun termination_by method int = - Function.termination_proof NONE - #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int - fun mk_catchall fixes arity_of = let fun mk_eqn ((fname, fT), _) = @@ -148,24 +139,32 @@ val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, partials=false, tailrec=false } -fun gen_fun add config fixes statements int lthy = - lthy - |> add fixes statements config - |> by_pat_completeness_auto int - |> Local_Theory.restore - |> termination_by (Function_Common.get_termination_prover lthy) int +fun gen_add_fun add fixes statements config lthy = + let + fun pat_completeness_auto ctxt = + Pat_Completeness.pat_completeness_tac ctxt 1 + THEN auto_tac (clasimpset_of ctxt) + fun prove_termination lthy = + Function.prove_termination NONE + (Function_Common.get_termination_prover lthy lthy) lthy + in + lthy + |> add fixes statements config pat_completeness_auto |> snd + |> Local_Theory.restore + |> prove_termination + end -val add_fun = gen_fun Function.add_function -val add_fun_cmd = gen_fun Function.add_function_cmd +val add_fun = gen_add_fun Function.add_function +val add_fun_cmd = gen_add_fun Function.add_function_cmd local structure P = OuterParse and K = OuterKeyword in val _ = - OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl + OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl (function_parser fun_config - >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements)); + >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)); end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Function/function.ML Thu Apr 29 17:50:11 2010 +0200 @@ -11,14 +11,25 @@ val add_function: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Function_Common.function_config -> - local_theory -> Proof.state + (Proof.context -> tactic) -> local_theory -> info * local_theory val add_function_cmd: (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Function_Common.function_config -> + (Proof.context -> tactic) -> local_theory -> info * local_theory + + val function: (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> Function_Common.function_config -> local_theory -> Proof.state - val termination_proof : term option -> local_theory -> Proof.state - val termination_proof_cmd : string option -> local_theory -> Proof.state + val function_cmd: (binding * string option * mixfix) list -> + (Attrib.binding * string) list -> Function_Common.function_config -> + local_theory -> Proof.state + + val prove_termination: term option -> tactic -> local_theory -> local_theory + val prove_termination_cmd: string option -> tactic -> local_theory -> local_theory + + val termination : term option -> local_theory -> Proof.state + val termination_cmd : string option -> local_theory -> Proof.state val setup : theory -> theory val get_congs : Proof.context -> thm list @@ -65,7 +76,7 @@ (saved_simps, fold2 add_for_f fnames simps_by_f lthy) end -fun gen_add_function is_external prep default_constraint fixspec eqns config lthy = +fun prepare_function is_external prep default_constraint fixspec eqns config lthy = let val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy @@ -76,7 +87,7 @@ val defname = mk_defname fixes val FunctionConfig {partials, ...} = config - val ((goalstate, cont), lthy) = + val ((goal_state, cont), lthy') = Function_Mutual.prepare_function_mutual config defname fixes eqs lthy fun afterqed [[proof]] lthy = @@ -115,20 +126,45 @@ if not is_external then () else Specification.print_consts lthy (K false) (map fst fixes) in - lthy - |> Local_Theory.declaration false (add_function_data o morph_function_data info) + (info, + lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) end in - lthy - |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] - |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd + ((goal_state, afterqed), lthy') + end + +fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy = + let + val ((goal_state, afterqed), lthy') = + prepare_function is_external prep default_constraint fixspec eqns config lthy + val pattern_thm = + case SINGLE (tac lthy') goal_state of + NONE => error "pattern completeness and compatibility proof failed" + | SOME st => Goal.finish lthy' st + in + lthy' + |> afterqed [[pattern_thm]] end val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) val add_function_cmd = gen_add_function true Specification.read_spec "_::type" - -fun gen_termination_proof prep_term raw_term_opt lthy = + +fun gen_function is_external prep default_constraint fixspec eqns config lthy = + let + val ((goal_state, afterqed), lthy') = + prepare_function is_external prep default_constraint fixspec eqns config lthy + in + lthy' + |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] + |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd + end + +val function = + gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) +val function_cmd = gen_function true Specification.read_spec "_::type" + +fun prepare_termination_proof prep_term raw_term_opt lthy = let val term_opt = Option.map (prep_term lthy) raw_term_opt val info = the (case term_opt of @@ -169,6 +205,26 @@ end) end in + (goal, afterqed, termination) + end + +fun gen_prove_termination prep_term raw_term_opt tac lthy = + let + val (goal, afterqed, termination) = + prepare_termination_proof prep_term raw_term_opt lthy + + val totality = Goal.prove lthy [] [] goal (K tac) + in + afterqed [[totality]] lthy +end + +val prove_termination = gen_prove_termination Syntax.check_term +val prove_termination_cmd = gen_prove_termination Syntax.read_term + +fun gen_termination prep_term raw_term_opt lthy = + let + val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy + in lthy |> ProofContext.note_thmss "" [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd @@ -180,8 +236,8 @@ |> Proof.theorem NONE afterqed [[(goal, [])]] end -val termination_proof = gen_termination_proof Syntax.check_term -val termination_proof_cmd = gen_termination_proof Syntax.read_term +val termination = gen_termination Syntax.check_term +val termination_cmd = gen_termination Syntax.read_term (* Datatype hook to declare datatype congs as "function_congs" *) @@ -221,11 +277,11 @@ val _ = OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal (function_parser default_config - >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config)) + >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) val _ = OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal - (Scan.option P.term >> termination_proof_cmd) + (Scan.option P.term >> termination_cmd) end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Thu Apr 29 17:50:11 2010 +0200 @@ -172,7 +172,7 @@ structure TerminationProver = Generic_Data ( - type T = Proof.context -> Proof.method + type T = Proof.context -> tactic val empty = (fn _ => error "Termination prover not configured") val extend = I fun merge (a, b) = b (* FIXME ? *) diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Apr 29 17:50:11 2010 +0200 @@ -225,6 +225,6 @@ Method.setup @{binding lexicographic_order} (Method.sections clasimp_modifiers >> (K lexicographic_order)) "termination prover for lexicographic orderings" - #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order) + #> Context.theory_map (Function_Common.set_termination_prover (lexicographic_order_tac false)) end; diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Apr 29 17:50:11 2010 +0200 @@ -10,7 +10,7 @@ val sizechange_tac : Proof.context -> tactic -> tactic - val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method + val decomp_scnp_tac : ScnpSolve.label list -> Proof.context -> tactic val setup : theory -> theory @@ -396,13 +396,12 @@ fun sizechange_tac ctxt autom_tac = gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac)) -fun decomp_scnp orders ctxt = +fun decomp_scnp_tac orders ctxt = let val extra_simps = Function_Common.Termination_Simps.get ctxt val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps) in - SIMPLE_METHOD - (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)) + gen_sizechange_tac orders autom_tac ctxt (print_error ctxt) end @@ -416,7 +415,8 @@ || Scan.succeed [MAX, MS, MIN] val setup = Method.setup @{binding size_change} - (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp) + (Scan.lift orders --| Method.sections clasimp_modifiers >> + (fn orders => SIMPLE_METHOD o decomp_scnp_tac orders)) "termination prover with graph decomposition and the NP subset of size change termination" end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 29 17:50:11 2010 +0200 @@ -529,16 +529,19 @@ fun instantiate i n {context = ctxt, params = p, prems = prems, asms = a, concl = cl, schematics = s} = let + fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) + fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) + |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of) val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) val case_th = MetaSimplifier.simplify true - (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) - (nth cases (i - 1)) + (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) - val (_, tenv) = fold (Pattern.match thy) pats (Vartab.empty, Vartab.empty) - fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) - val inst = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) - val thesis = Thm.instantiate ([], inst) case_th OF (replicate nargs @{thm refl}) OF prems' + val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th + OF (replicate nargs @{thm refl}) + val thesis = + Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th' + OF prems' in (rtac thesis 1) end diff -r 03d2a2d0ee4a -r 2584289edbb0 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Thu Apr 29 17:50:11 2010 +0200 @@ -171,10 +171,20 @@ |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr)) end; +fun add_eval_constr (const, const') thy = + let + val k = Code.args_number thy const; + fun pr pr' fxy ts = Code_Printer.brackify fxy + (const' :: the_list (Code_ML.print_tuple pr' Code_Printer.BR (map fst ts))); + in + thy + |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr))) + end; + fun add_eval_const (const, const') = Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const'))); -fun process (code_body, (tyco_map, const_map)) module_name NONE thy = +fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy = let val pr = Code_Printer.str o Long_Name.append module_name; in @@ -182,6 +192,7 @@ |> Code_Target.add_reserved target module_name |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body)) |> fold (add_eval_tyco o apsnd pr) tyco_map + |> fold (add_eval_constr o apsnd pr) constr_map |> fold (add_eval_const o apsnd pr) const_map end | process (code_body, _) _ (SOME file_name) thy = @@ -197,11 +208,15 @@ let val datatypes = map (fn (raw_tyco, raw_cos) => (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes; + val _ = map (uncurry (check_datatype thy)) datatypes; + val tycos = map fst datatypes; + val constrs = maps snd datatypes; val functions = map (prep_const thy) raw_functions; - val _ = map (uncurry (check_datatype thy)) datatypes; + val result = evaluation_code thy module_name tycos (constrs @ functions) + |> (apsnd o apsnd) (chop (length constrs)); in thy - |> process (evaluation_code thy module_name (map fst datatypes) (maps snd datatypes @ functions)) module_name some_file + |> process result module_name some_file end; val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const; diff -r 03d2a2d0ee4a -r 2584289edbb0 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Apr 29 17:47:53 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Apr 29 17:50:11 2010 +0200 @@ -9,6 +9,8 @@ val target_SML: string val evaluation_code_of: theory -> string -> string -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list + val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T) + -> Code_Printer.fixity -> 'a list -> Pretty.T option val setup: theory -> theory end;