--- 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
--- 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
--- 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 *}
--- 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 "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
--- 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 *}
--- 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
--- 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 \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
-where
- CD: "CRYPT K (DECRYPT K X) \<sim> X"
-| DC: "DECRYPT K (CRYPT K X) \<sim> X"
-| NONCE: "NONCE N \<sim> NONCE N"
-| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
-| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
-| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
-| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
-| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-
-lemmas msgrel.intros[intro]
-
-text{*Proving that it is an equivalence relation*}
-
-lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
-
-theorem equiv_msgrel: "equivp msgrel"
-proof (rule equivpI)
- show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
- show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
- show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
-qed
-
-subsection{*Some Functions on the Free Algebra*}
-
-subsubsection{*The Set of Nonces*}
-
-fun
- freenonces :: "freemsg \<Rightarrow> nat set"
-where
- "freenonces (NONCE N) = {N}"
-| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-| "freenonces (CRYPT K X) = freenonces X"
-| "freenonces (DECRYPT K X) = freenonces X"
-
-theorem msgrel_imp_eq_freenonces:
- assumes a: "U \<sim> V"
- shows "freenonces U = freenonces V"
- using a by (induct) (auto)
-
-subsubsection{*The Left Projection*}
-
-text{*A function to return the left part of the top pair in a message. It will
-be lifted to the initial algrebra, to serve as an example of that process.*}
-fun
- freeleft :: "freemsg \<Rightarrow> freemsg"
-where
- "freeleft (NONCE N) = NONCE N"
-| "freeleft (MPAIR X Y) = X"
-| "freeleft (CRYPT K X) = freeleft X"
-| "freeleft (DECRYPT K X) = freeleft X"
-
-text{*This theorem lets us prove that the left function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeleft_aux:
- shows "freeleft U \<sim> freeleft U"
- by (induct rule: freeleft.induct) (auto)
-
-theorem msgrel_imp_eqv_freeleft:
- assumes a: "U \<sim> V"
- shows "freeleft U \<sim> freeleft V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
-
-subsubsection{*The Right Projection*}
-
-text{*A function to return the right part of the top pair in a message.*}
-fun
- freeright :: "freemsg \<Rightarrow> freemsg"
-where
- "freeright (NONCE N) = NONCE N"
-| "freeright (MPAIR X Y) = Y"
-| "freeright (CRYPT K X) = freeright X"
-| "freeright (DECRYPT K X) = freeright X"
-
-text{*This theorem lets us prove that the right function respects the
-equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
-lemma msgrel_imp_eqv_freeright_aux:
- shows "freeright U \<sim> freeright U"
- by (induct rule: freeright.induct) (auto)
-
-theorem msgrel_imp_eqv_freeright:
- assumes a: "U \<sim> V"
- shows "freeright U \<sim> freeright V"
- using a
- by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
-
-subsubsection{*The Discriminator for Constructors*}
-
-text{*A function to distinguish nonces, mpairs and encryptions*}
-fun
- freediscrim :: "freemsg \<Rightarrow> int"
-where
- "freediscrim (NONCE N) = 0"
- | "freediscrim (MPAIR X Y) = 1"
- | "freediscrim (CRYPT K X) = freediscrim X + 2"
- | "freediscrim (DECRYPT K X) = freediscrim X - 2"
-
-text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
-theorem msgrel_imp_eq_freediscrim:
- assumes a: "U \<sim> V"
- shows "freediscrim U = freediscrim V"
- using a by (induct) (auto)
-
-subsection{*The Initial Algebra: A Quotiented Message Type*}
-
-quotient_type msg = freemsg / msgrel
- by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_definition
- "Nonce :: nat \<Rightarrow> msg"
-is
- "NONCE"
-
-quotient_definition
- "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-is
- "MPAIR"
-
-quotient_definition
- "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "CRYPT"
-
-quotient_definition
- "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
-
-text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]:
- shows "Crypt K (Decrypt K X) = X"
- by (lifting CD)
-
-theorem DC_eq [simp]:
- shows "Decrypt K (Crypt K X) = X"
- by (lifting DC)
-
-subsection{*The Abstract Function to Return the Set of Nonces*}
-
-quotient_definition
- "nonces:: msg \<Rightarrow> nat set"
-is
- "freenonces"
-
-text{*Now prove the four equations for @{term nonces}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freenonces freenonces"
- by (simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim>) NONCE NONCE"
- by (simp add: NONCE)
-
-lemma nonces_Nonce [simp]:
- shows "nonces (Nonce N) = {N}"
- by (lifting freenonces.simps(1))
-
-lemma [quot_respect]:
- shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
- by (simp add: MPAIR)
-
-lemma nonces_MPair [simp]:
- shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
- by (lifting freenonces.simps(2))
-
-lemma nonces_Crypt [simp]:
- shows "nonces (Crypt K X) = nonces X"
- by (lifting freenonces.simps(3))
-
-lemma nonces_Decrypt [simp]:
- shows "nonces (Decrypt K X) = nonces X"
- by (lifting freenonces.simps(4))
-
-subsection{*The Abstract Function to Return the Left Part*}
-
-quotient_definition
- "left:: msg \<Rightarrow> msg"
-is
- "freeleft"
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
- by (simp add: msgrel_imp_eqv_freeleft)
-
-lemma left_Nonce [simp]:
- shows "left (Nonce N) = Nonce N"
- by (lifting freeleft.simps(1))
-
-lemma left_MPair [simp]:
- shows "left (MPair X Y) = X"
- by (lifting freeleft.simps(2))
-
-lemma left_Crypt [simp]:
- shows "left (Crypt K X) = left X"
- by (lifting freeleft.simps(3))
-
-lemma left_Decrypt [simp]:
- shows "left (Decrypt K X) = left X"
- by (lifting freeleft.simps(4))
-
-subsection{*The Abstract Function to Return the Right Part*}
-
-quotient_definition
- "right:: msg \<Rightarrow> msg"
-is
- "freeright"
-
-text{*Now prove the four equations for @{term right}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeright freeright"
- by (simp add: msgrel_imp_eqv_freeright)
-
-lemma right_Nonce [simp]:
- shows "right (Nonce N) = Nonce N"
- by (lifting freeright.simps(1))
-
-lemma right_MPair [simp]:
- shows "right (MPair X Y) = Y"
- by (lifting freeright.simps(2))
-
-lemma right_Crypt [simp]:
- shows "right (Crypt K X) = right X"
- by (lifting freeright.simps(3))
-
-lemma right_Decrypt [simp]:
- shows "right (Decrypt K X) = right X"
- by (lifting freeright.simps(4))
-
-subsection{*Injectivity Properties of Some Constructors*}
-
-lemma NONCE_imp_eq:
- shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
- by (drule msgrel_imp_eq_freenonces, simp)
-
-text{*Can also be proved using the function @{term nonces}*}
-lemma Nonce_Nonce_eq [iff]:
- shows "(Nonce m = Nonce n) = (m = n)"
-proof
- assume "Nonce m = Nonce n"
- then show "m = n" by (lifting NONCE_imp_eq)
-next
- assume "m = n"
- then show "Nonce m = Nonce n" by simp
-qed
-
-lemma MPAIR_imp_eqv_left:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
- by (drule msgrel_imp_eqv_freeleft) (simp)
-
-lemma MPair_imp_eq_left:
- assumes eq: "MPair X Y = MPair X' Y'"
- shows "X = X'"
- using eq by (lifting MPAIR_imp_eqv_left)
-
-lemma MPAIR_imp_eqv_right:
- shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
- by (drule msgrel_imp_eqv_freeright) (simp)
-
-lemma MPair_imp_eq_right:
- shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
- by (lifting MPAIR_imp_eqv_right)
-
-theorem MPair_MPair_eq [iff]:
- shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
- by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
-
-lemma NONCE_neqv_MPAIR:
- shows "\<not>(NONCE m \<sim> MPAIR X Y)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Nonce_neq_MPair [iff]:
- shows "Nonce N \<noteq> MPair X Y"
- by (lifting NONCE_neqv_MPAIR)
-
-text{*Example suggested by a referee*}
-
-lemma CRYPT_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt_Nonce_neq_Nonce:
- shows "Crypt K (Nonce M) \<noteq> Nonce N"
- by (lifting CRYPT_NONCE_neq_NONCE)
-
-text{*...and many similar results*}
-lemma CRYPT2_NONCE_neq_NONCE:
- shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
- by (auto dest: msgrel_imp_eq_freediscrim)
-
-theorem Crypt2_Nonce_neq_Nonce:
- shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
- by (lifting CRYPT2_NONCE_neq_NONCE)
-
-theorem Crypt_Crypt_eq [iff]:
- shows "(Crypt K X = Crypt K X') = (X=X')"
-proof
- assume "Crypt K X = Crypt K X'"
- hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Crypt K X = Crypt K X'" by simp
-qed
-
-theorem Decrypt_Decrypt_eq [iff]:
- shows "(Decrypt K X = Decrypt K X') = (X=X')"
-proof
- assume "Decrypt K X = Decrypt K X'"
- hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Decrypt K X = Decrypt K X'" by simp
-qed
-
-lemma msg_induct_aux:
- shows "\<lbrakk>\<And>N. P (Nonce N);
- \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
- \<And>K X. P X \<Longrightarrow> P (Crypt K X);
- \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
- by (lifting freemsg.induct)
-
-lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
- assumes N: "\<And>N. P (Nonce N)"
- and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
- and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
- and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
- shows "P msg"
- using N M C D by (rule msg_induct_aux)
-
-subsection{*The Abstract Discriminator*}
-
-text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
-need this function in order to prove discrimination theorems.*}
-
-quotient_definition
- "discrim:: msg \<Rightarrow> int"
-is
- "freediscrim"
-
-text{*Now prove the four equations for @{term discrim}*}
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freediscrim freediscrim"
- by (auto simp add: msgrel_imp_eq_freediscrim)
-
-lemma discrim_Nonce [simp]:
- shows "discrim (Nonce N) = 0"
- by (lifting freediscrim.simps(1))
-
-lemma discrim_MPair [simp]:
- shows "discrim (MPair X Y) = 1"
- by (lifting freediscrim.simps(2))
-
-lemma discrim_Crypt [simp]:
- shows "discrim (Crypt K X) = discrim X + 2"
- by (lifting freediscrim.simps(3))
-
-lemma discrim_Decrypt [simp]:
- shows "discrim (Decrypt K X) = discrim X - 2"
- by (lifting freediscrim.simps(4))
-
-end
-
--- a/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 \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
-begin
-
-quotient_definition
- Zero_int_def: "0::int" is "(0::nat, 0::nat)"
-
-quotient_definition
- One_int_def: "1::int" is "(1::nat, 0::nat)"
-
-definition
- "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-quotient_definition
- "(op +) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "add_raw"
-
-definition
- "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
-
-quotient_definition
- "uminus :: int \<Rightarrow> int"
-is
- "uminus_raw"
-
-fun
- mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
- "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
- "(op *) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "mult_raw"
-
-definition
- "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-is
- "le_raw"
-
-definition
- less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
-
-definition
- diff_int_def: "z - (w::int) \<equiv> z + (-w)"
-
-instance ..
-
-end
-
-subsection{*Construction of the Integers*}
-
-lemma zminus_zminus_raw:
- "uminus_raw (uminus_raw z) = z"
- by (cases z) (simp add: uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel) uminus_raw uminus_raw"
- by (simp add: uminus_raw_def)
-
-lemma zminus_zminus:
- fixes z::"int"
- shows "- (- z) = z"
- by(lifting zminus_zminus_raw)
-
-lemma zminus_0_raw:
- shows "uminus_raw (0, 0) = (0, 0::nat)"
- by (simp add: uminus_raw_def)
-
-lemma zminus_0:
- shows "- 0 = (0::int)"
- by (lifting zminus_0_raw)
-
-subsection{*Integer Addition*}
-
-lemma zminus_zadd_distrib_raw:
- shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
-by (cases z, cases w)
- (auto simp add: add_raw_def uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
-by (simp add: add_raw_def)
-
-lemma zminus_zadd_distrib:
- fixes z w::"int"
- shows "- (z + w) = (- z) + (- w)"
- by(lifting zminus_zadd_distrib_raw)
-
-lemma zadd_commute_raw:
- shows "add_raw z w = add_raw w z"
-by (cases z, cases w)
- (simp add: add_raw_def)
-
-lemma zadd_commute:
- fixes z w::"int"
- shows "(z::int) + w = w + z"
- by (lifting zadd_commute_raw)
-
-lemma zadd_assoc_raw:
- shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
- by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-
-lemma zadd_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
- by (lifting zadd_assoc_raw)
-
-lemma zadd_0_raw:
- shows "add_raw (0, 0) z = z"
- by (simp add: add_raw_def)
-
-
-text {*also for the instance declaration int :: plus_ac0*}
-lemma zadd_0:
- fixes z::"int"
- shows "0 + z = z"
- by (lifting zadd_0_raw)
-
-lemma zadd_zminus_inverse_raw:
- shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
- by (cases z) (simp add: add_raw_def uminus_raw_def)
-
-lemma zadd_zminus_inverse2:
- fixes z::"int"
- shows "(- z) + z = 0"
- by (lifting zadd_zminus_inverse_raw)
-
-subsection{*Integer Multiplication*}
-
-lemma zmult_zminus_raw:
- shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
-apply(cases z, cases w)
-apply(simp add: uminus_raw_def)
-done
-
-lemma mult_raw_fst:
- assumes a: "intrel x z"
- shows "intrel (mult_raw x y) (mult_raw z y)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult_raw_snd:
- assumes a: "intrel x z"
- shows "intrel (mult_raw y x) (mult_raw y z)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
-
-lemma zmult_zminus:
- fixes z w::"int"
- shows "(- z) * w = - (z * w)"
- by (lifting zmult_zminus_raw)
-
-lemma zmult_commute_raw:
- shows "mult_raw z w = mult_raw w z"
-apply(cases z, cases w)
-apply(simp add: add_ac mult_ac)
-done
-
-lemma zmult_commute:
- fixes z w::"int"
- shows "z * w = w * z"
- by (lifting zmult_commute_raw)
-
-lemma zmult_assoc_raw:
- shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
-apply(cases z1, cases z2, cases z3)
-apply(simp add: add_mult_distrib2 mult_ac)
-done
-
-lemma zmult_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
- by (lifting zmult_assoc_raw)
-
-lemma zadd_mult_distrib_raw:
- shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
-apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
-done
-
-lemma zadd_zmult_distrib:
- fixes z1 z2 w::"int"
- shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
- by(lifting zadd_mult_distrib_raw)
-
-lemma zadd_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 + z2) = (w * z1) + (w * z2)"
- by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-
-lemma zdiff_zmult_distrib:
- fixes w z1 z2::"int"
- shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
- by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 - z2) = (w * z1) - (w * z2)"
- by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
-
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemma zmult_1_raw:
- shows "mult_raw (1, 0) z = z"
- by (cases z) (auto)
-
-lemma zmult_1:
- fixes z::"int"
- shows "1 * z = z"
- by (lifting zmult_1_raw)
-
-lemma zmult_1_right:
- fixes z::"int"
- shows "z * 1 = z"
- by (rule trans [OF zmult_commute zmult_1])
-
-lemma zero_not_one:
- shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
- by auto
-
-text{*The Integers Form A Ring*}
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
- show "i + j = j + i" by (simp add: zadd_commute)
- show "0 + i = i" by (rule zadd_0)
- show "- i + i = 0" by (rule zadd_zminus_inverse2)
- show "i - j = i + (-j)" by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
- show "i * j = j * i" by (rule zmult_commute)
- show "1 * i = i" by (rule zmult_1)
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by (lifting zero_not_one)
-qed
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma zle_refl_raw:
- shows "le_raw w w"
- by (cases w) (simp add: le_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> op =) le_raw le_raw"
- by (auto) (simp_all add: le_raw_def)
-
-lemma zle_refl:
- fixes w::"int"
- shows "w \<le> w"
- by (lifting zle_refl_raw)
-
-
-lemma zle_trans_raw:
- shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
-apply(cases i, cases j, cases k)
-apply(auto simp add: le_raw_def)
-done
-
-lemma zle_trans:
- fixes i j k::"int"
- shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
- by (lifting zle_trans_raw)
-
-lemma zle_anti_sym_raw:
- shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
-apply(cases z, cases w)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_anti_sym:
- fixes z w::"int"
- shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
- by (lifting zle_anti_sym_raw)
-
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le:
- fixes w z::"int"
- shows "(w < z) = (w \<le> z & w \<noteq> z)"
- by (simp add: less_int_def)
-
-instance int :: order
-apply (default)
-apply(auto simp add: zless_le zle_anti_sym)[1]
-apply(rule zle_refl)
-apply(erule zle_trans, assumption)
-apply(erule zle_anti_sym, assumption)
-done
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-
-lemma zle_linear_raw:
- shows "le_raw z w \<or> le_raw w z"
-apply(cases w, cases z)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_linear:
- fixes z w::"int"
- shows "z \<le> w \<or> w \<le> z"
- by (lifting zle_linear_raw)
-
-instance int :: linorder
-apply(default)
-apply(rule zle_linear)
-done
-
-lemma zadd_left_mono_raw:
- shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
-apply(cases k)
-apply(auto simp add: add_raw_def le_raw_def)
-done
-
-lemma zadd_left_mono:
- fixes i j::"int"
- shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting zadd_left_mono_raw)
-
-
-subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
-
-definition
- "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
- "nat2::int \<Rightarrow> nat"
-is
- "nat_raw"
-
-abbreviation
- "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
-
-lemma nat_le_eq_zle_raw:
- shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
- apply (cases w)
- apply (cases z)
- apply (simp add: nat_raw_def le_raw_def)
- by auto
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) nat_raw nat_raw"
- by (auto iff: nat_raw_def)
-
-lemma nat_le_eq_zle:
- fixes w z::"int"
- shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
- unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
-
-end
--- /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 \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+ by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+begin
+
+quotient_definition
+ "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+
+quotient_definition
+ "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+
+fun
+ plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+ "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+
+fun
+ uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "uminus_int_raw (x, y) = (y, x)"
+
+quotient_definition
+ "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+
+definition
+ minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
+
+fun
+ times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+ "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+
+fun
+ le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+
+definition
+ less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+
+instance ..
+
+end
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
+ and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
+ and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
+ by auto
+
+lemma times_int_raw_fst:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw x y \<approx> times_int_raw z y"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma times_int_raw_snd:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw y x \<approx> times_int_raw y z"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
+ apply(simp only: fun_rel_def)
+ apply(rule allI | rule impI)+
+ apply(rule equivp_transp[OF int_equivp])
+ apply(rule times_int_raw_fst)
+ apply(assumption)
+ apply(rule times_int_raw_snd)
+ apply(assumption)
+ done
+
+lemma plus_assoc_raw:
+ shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
+ by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+ shows "plus_int_raw i j \<approx> plus_int_raw j i"
+ by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+ shows "plus_int_raw (0, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+ shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
+ by (cases i) (simp)
+
+lemma times_assoc_raw:
+ shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
+ by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma times_sym_raw:
+ shows "times_int_raw i j \<approx> times_int_raw j i"
+ by (cases i, cases j) (simp add: algebra_simps)
+
+lemma times_one_raw:
+ shows "times_int_raw (1, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma times_plus_comm_raw:
+ shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
+by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma one_zero_distinct:
+ shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
+ by simp
+
+text{* The integers form a @{text comm_ring_1}*}
+
+instance int :: comm_ring_1
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)"
+ by (lifting plus_assoc_raw)
+ show "i + j = j + i"
+ by (lifting plus_sym_raw)
+ show "0 + i = (i::int)"
+ by (lifting plus_zero_raw)
+ show "- i + i = 0"
+ by (lifting plus_minus_zero_raw)
+ show "i - j = i + - j"
+ by (simp add: minus_int_def)
+ show "(i * j) * k = i * (j * k)"
+ by (lifting times_assoc_raw)
+ show "i * j = j * i"
+ by (lifting times_sym_raw)
+ show "1 * i = i"
+ by (lifting times_one_raw)
+ show "(i + j) * k = i * k + j * k"
+ by (lifting times_plus_comm_raw)
+ show "0 \<noteq> (1::int)"
+ by (lifting one_zero_distinct)
+qed
+
+lemma plus_int_raw_rsp_aux:
+ assumes a: "a \<approx> b" "c \<approx> d"
+ shows "plus_int_raw a c \<approx> plus_int_raw b d"
+ using a
+ by (cases a, cases b, cases c, cases d)
+ (simp)
+
+lemma add_abs_int:
+ "(abs_int (x,y)) + (abs_int (u,v)) =
+ (abs_int (x + u, y + v))"
+ apply(simp add: plus_int_def id_simps)
+ apply(fold plus_int_raw.simps)
+ apply(rule Quotient_rel_abs[OF Quotient_int])
+ apply(rule plus_int_raw_rsp_aux)
+ apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+ done
+
+definition int_of_nat_raw:
+ "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_definition
+ "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
+
+lemma[quot_respect]:
+ shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+ by (simp add: equivp_reflp[OF int_equivp])
+
+lemma int_of_nat:
+ shows "of_nat m = int_of_nat m"
+ by (induct m)
+ (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
+
+lemma le_antisym_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
+ by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+ shows "le_int_raw i i"
+ by (cases i) (simp)
+
+lemma le_trans_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
+ by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+ shows "le_int_raw i j \<or> le_int_raw j i"
+ by (cases i, cases j)
+ (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+ fix i j k :: int
+ show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+ by (lifting le_antisym_raw)
+ show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+ by (auto simp add: less_int_def dest: antisym)
+ show "i \<le> i"
+ by (lifting le_refl_raw)
+ show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+ by (lifting le_trans_raw)
+ show "i \<le> j \<or> j \<le> i"
+ by (lifting le_cases_raw)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+ by 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 \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
+ by (cases i, cases j, cases k) (simp)
+
+instance int :: ordered_cancel_ab_semigroup_add
+proof
+ fix i j k :: int
+ show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (lifting le_plus_int_raw)
+qed
+
+abbreviation
+ "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
+
+lemma zmult_zless_mono2_lemma:
+ fixes i j::int
+ and k::nat
+ shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+ apply(induct "k")
+ apply(simp)
+ apply(case_tac "k = 0")
+ apply(simp_all add: left_distrib add_strict_mono)
+ done
+
+lemma zero_le_imp_eq_int_raw:
+ fixes k::"(nat \<times> nat)"
+ shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+ apply(cases k)
+ apply(simp add:int_of_nat_raw)
+ apply(auto)
+ apply(rule_tac i="b" and j="a" in less_Suc_induct)
+ apply(auto)
+ done
+
+lemma zero_le_imp_eq_int:
+ fixes k::int
+ shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+ unfolding less_int_def int_of_nat
+ by (lifting zero_le_imp_eq_int_raw)
+
+lemma zmult_zless_mono2:
+ fixes i j k::int
+ assumes a: "i < j" "0 < k"
+ shows "k * i < k * j"
+ using a
+ by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+
+text{*The integers form an ordered integral domain*}
+
+instance int :: linordered_idom
+proof
+ fix i j k :: int
+ show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+ by (rule zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+ by (simp only: zabs_def)
+ show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
+qed
+
+lemmas int_distrib =
+ left_distrib [of "z1::int" "z2" "w", standard]
+ right_distrib [of "w::int" "z1" "z2", standard]
+ left_diff_distrib [of "z1::int" "z2" "w", standard]
+ right_diff_distrib [of "w::int" "z1" "z2", standard]
+ minus_add_distrib[of "z1::int" "z2", standard]
+
+lemma int_induct_raw:
+ assumes a: "P (0::nat, 0)"
+ and b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
+ and c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
+ shows "P x"
+proof (cases x, clarify)
+ fix a b
+ show "P (a, b)"
+ proof (induct a arbitrary: b rule: Nat.induct)
+ case zero
+ show "P (0, b)" using assms by (induct b) auto
+ next
+ case (Suc n)
+ then show ?case using assms by auto
+ qed
+qed
+
+lemma int_induct:
+ fixes x :: int
+ assumes a: "P 0"
+ and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+ and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+ shows "P x"
+ using a b c unfolding minus_int_def
+ by (lifting int_induct_raw)
+
+text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+
+definition
+ "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+ "int_to_nat::int \<Rightarrow> nat"
+is
+ "int_to_nat_raw"
+
+lemma [quot_respect]:
+ shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
+ by (auto iff: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle_raw:
+ assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
+ shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
+ using a
+ by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle:
+ fixes w z::"int"
+ shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
+ unfolding less_int_def
+ by (lifting nat_le_eq_zle_raw)
+
+end
--- /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 \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where
+ CD: "CRYPT K (DECRYPT K X) \<sim> X"
+| DC: "DECRYPT K (CRYPT K X) \<sim> X"
+| NONCE: "NONCE N \<sim> NONCE N"
+| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+lemmas msgrel.intros[intro]
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> X"
+by (induct X, (blast intro: msgrel.intros)+)
+
+theorem equiv_msgrel: "equivp msgrel"
+proof (rule equivpI)
+ show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
+ show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
+ show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+qed
+
+subsection{*Some Functions on the Free Algebra*}
+
+subsubsection{*The Set of Nonces*}
+
+fun
+ freenonces :: "freemsg \<Rightarrow> nat set"
+where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
+
+theorem msgrel_imp_eq_freenonces:
+ assumes a: "U \<sim> V"
+ shows "freenonces U = freenonces V"
+ using a by (induct) (auto)
+
+subsubsection{*The Left Projection*}
+
+text{*A function to return the left part of the top pair in a message. It will
+be lifted to the initial algrebra, to serve as an example of that process.*}
+fun
+ freeleft :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft X"
+
+text{*This theorem lets us prove that the left function respects the
+equivalence relation. It also helps us prove that MPair
+ (the abstract constructor) is injective*}
+lemma msgrel_imp_eqv_freeleft_aux:
+ shows "freeleft U \<sim> freeleft U"
+ by (induct rule: freeleft.induct) (auto)
+
+theorem msgrel_imp_eqv_freeleft:
+ assumes a: "U \<sim> V"
+ shows "freeleft U \<sim> freeleft V"
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
+
+subsubsection{*The Right Projection*}
+
+text{*A function to return the right part of the top pair in a message.*}
+fun
+ freeright :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright X"
+
+text{*This theorem lets us prove that the right function respects the
+equivalence relation. It also helps us prove that MPair
+ (the abstract constructor) is injective*}
+lemma msgrel_imp_eqv_freeright_aux:
+ shows "freeright U \<sim> freeright U"
+ by (induct rule: freeright.induct) (auto)
+
+theorem msgrel_imp_eqv_freeright:
+ assumes a: "U \<sim> V"
+ shows "freeright U \<sim> freeright V"
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
+
+subsubsection{*The Discriminator for Constructors*}
+
+text{*A function to distinguish nonces, mpairs and encryptions*}
+fun
+ freediscrim :: "freemsg \<Rightarrow> int"
+where
+ "freediscrim (NONCE N) = 0"
+ | "freediscrim (MPAIR X Y) = 1"
+ | "freediscrim (CRYPT K X) = freediscrim X + 2"
+ | "freediscrim (DECRYPT K X) = freediscrim X - 2"
+
+text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_freediscrim:
+ assumes a: "U \<sim> V"
+ shows "freediscrim U = freediscrim V"
+ using a by (induct) (auto)
+
+subsection{*The Initial Algebra: A Quotiented Message Type*}
+
+quotient_type msg = freemsg / msgrel
+ by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_definition
+ "Nonce :: nat \<Rightarrow> msg"
+is
+ "NONCE"
+
+quotient_definition
+ "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "MPAIR"
+
+quotient_definition
+ "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "CRYPT"
+
+quotient_definition
+ "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "DECRYPT"
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
+by (auto intro: DECRYPT)
+
+text{*Establishing these two equations is the point of the whole exercise*}
+theorem CD_eq [simp]:
+ shows "Crypt K (Decrypt K X) = X"
+ by (lifting CD)
+
+theorem DC_eq [simp]:
+ shows "Decrypt K (Crypt K X) = X"
+ by (lifting DC)
+
+subsection{*The Abstract Function to Return the Set of Nonces*}
+
+quotient_definition
+ "nonces:: msg \<Rightarrow> nat set"
+is
+ "freenonces"
+
+text{*Now prove the four equations for @{term nonces}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freenonces freenonces"
+ by (simp add: msgrel_imp_eq_freenonces)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim>) NONCE NONCE"
+ by (simp add: NONCE)
+
+lemma nonces_Nonce [simp]:
+ shows "nonces (Nonce N) = {N}"
+ by (lifting freenonces.simps(1))
+
+lemma [quot_respect]:
+ shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
+ by (simp add: MPAIR)
+
+lemma nonces_MPair [simp]:
+ shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
+ by (lifting freenonces.simps(2))
+
+lemma nonces_Crypt [simp]:
+ shows "nonces (Crypt K X) = nonces X"
+ by (lifting freenonces.simps(3))
+
+lemma nonces_Decrypt [simp]:
+ shows "nonces (Decrypt K X) = nonces X"
+ by (lifting freenonces.simps(4))
+
+subsection{*The Abstract Function to Return the Left Part*}
+
+quotient_definition
+ "left:: msg \<Rightarrow> msg"
+is
+ "freeleft"
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
+ by (simp add: msgrel_imp_eqv_freeleft)
+
+lemma left_Nonce [simp]:
+ shows "left (Nonce N) = Nonce N"
+ by (lifting freeleft.simps(1))
+
+lemma left_MPair [simp]:
+ shows "left (MPair X Y) = X"
+ by (lifting freeleft.simps(2))
+
+lemma left_Crypt [simp]:
+ shows "left (Crypt K X) = left X"
+ by (lifting freeleft.simps(3))
+
+lemma left_Decrypt [simp]:
+ shows "left (Decrypt K X) = left X"
+ by (lifting freeleft.simps(4))
+
+subsection{*The Abstract Function to Return the Right Part*}
+
+quotient_definition
+ "right:: msg \<Rightarrow> msg"
+is
+ "freeright"
+
+text{*Now prove the four equations for @{term right}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) freeright freeright"
+ by (simp add: msgrel_imp_eqv_freeright)
+
+lemma right_Nonce [simp]:
+ shows "right (Nonce N) = Nonce N"
+ by (lifting freeright.simps(1))
+
+lemma right_MPair [simp]:
+ shows "right (MPair X Y) = Y"
+ by (lifting freeright.simps(2))
+
+lemma right_Crypt [simp]:
+ shows "right (Crypt K X) = right X"
+ by (lifting freeright.simps(3))
+
+lemma right_Decrypt [simp]:
+ shows "right (Decrypt K X) = right X"
+ by (lifting freeright.simps(4))
+
+subsection{*Injectivity Properties of Some Constructors*}
+
+lemma NONCE_imp_eq:
+ shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
+ by (drule msgrel_imp_eq_freenonces, simp)
+
+text{*Can also be proved using the function @{term nonces}*}
+lemma Nonce_Nonce_eq [iff]:
+ shows "(Nonce m = Nonce n) = (m = n)"
+proof
+ assume "Nonce m = Nonce n"
+ then show "m = n" by (lifting NONCE_imp_eq)
+next
+ assume "m = n"
+ then show "Nonce m = Nonce n" by simp
+qed
+
+lemma MPAIR_imp_eqv_left:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
+ by (drule msgrel_imp_eqv_freeleft) (simp)
+
+lemma MPair_imp_eq_left:
+ assumes eq: "MPair X Y = MPair X' Y'"
+ shows "X = X'"
+ using eq by (lifting MPAIR_imp_eqv_left)
+
+lemma MPAIR_imp_eqv_right:
+ shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+ by (drule msgrel_imp_eqv_freeright) (simp)
+
+lemma MPair_imp_eq_right:
+ shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
+ by (lifting MPAIR_imp_eqv_right)
+
+theorem MPair_MPair_eq [iff]:
+ shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
+ by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
+
+lemma NONCE_neqv_MPAIR:
+ shows "\<not>(NONCE m \<sim> MPAIR X Y)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Nonce_neq_MPair [iff]:
+ shows "Nonce N \<noteq> MPair X Y"
+ by (lifting NONCE_neqv_MPAIR)
+
+text{*Example suggested by a referee*}
+
+lemma CRYPT_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt_Nonce_neq_Nonce:
+ shows "Crypt K (Nonce M) \<noteq> Nonce N"
+ by (lifting CRYPT_NONCE_neq_NONCE)
+
+text{*...and many similar results*}
+lemma CRYPT2_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt2_Nonce_neq_Nonce:
+ shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
+ by (lifting CRYPT2_NONCE_neq_NONCE)
+
+theorem Crypt_Crypt_eq [iff]:
+ shows "(Crypt K X = Crypt K X') = (X=X')"
+proof
+ assume "Crypt K X = Crypt K X'"
+ hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Crypt K X = Crypt K X'" by simp
+qed
+
+theorem Decrypt_Decrypt_eq [iff]:
+ shows "(Decrypt K X = Decrypt K X') = (X=X')"
+proof
+ assume "Decrypt K X = Decrypt K X'"
+ hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Decrypt K X = Decrypt K X'" by simp
+qed
+
+lemma msg_induct_aux:
+ shows "\<lbrakk>\<And>N. P (Nonce N);
+ \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
+ \<And>K X. P X \<Longrightarrow> P (Crypt K X);
+ \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
+ by (lifting freemsg.induct)
+
+lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
+ assumes N: "\<And>N. P (Nonce N)"
+ and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
+ and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
+ and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
+ shows "P msg"
+ using N M C D by (rule msg_induct_aux)
+
+subsection{*The Abstract Discriminator*}
+
+text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
+need this function in order to prove discrimination theorems.*}
+
+quotient_definition
+ "discrim:: msg \<Rightarrow> int"
+is
+ "freediscrim"
+
+text{*Now prove the four equations for @{term discrim}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freediscrim freediscrim"
+ by (auto simp add: msgrel_imp_eq_freediscrim)
+
+lemma discrim_Nonce [simp]:
+ shows "discrim (Nonce N) = 0"
+ by (lifting freediscrim.simps(1))
+
+lemma discrim_MPair [simp]:
+ shows "discrim (MPair X Y) = 1"
+ by (lifting freediscrim.simps(2))
+
+lemma discrim_Crypt [simp]:
+ shows "discrim (Crypt K X) = discrim X + 2"
+ by (lifting freediscrim.simps(3))
+
+lemma discrim_Decrypt [simp]:
+ shows "discrim (Decrypt K X) = discrim X - 2"
+ by (lifting freediscrim.simps(4))
+
+end
+
--- a/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"];
--- 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
--- 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
--- 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 ? *)
--- 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;
--- 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
--- 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
--- 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;
--- 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;