--- a/NEWS Thu Feb 14 16:36:21 2013 +0100
+++ b/NEWS Thu Feb 14 17:06:15 2013 +0100
@@ -10,6 +10,15 @@
(lin)order_topology. Allows to generalize theorems about limits and
order. Instances are reals and extended reals.
+*** HOL ***
+
+* Consolidation of library theories on product orders:
+
+ Product_Lattice ~> Product_Order -- pointwise order on products
+ Product_ord ~> Product_Lexorder -- lexicographic order on products
+
+INCOMPATIBILITY.
+
New in Isabelle2013 (February 2013)
-----------------------------------
--- a/src/HOL/Big_Operators.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Big_Operators.thy Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
header {* Big operators and finite (non-empty) sets *}
theory Big_Operators
-imports Plain
+imports Finite_Set Metis
begin
subsection {* Generic monoid operation over a set *}
--- a/src/HOL/Code_Evaluation.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Evaluation
-imports Plain Typerep New_DSequence
+imports Typerep New_DSequence
begin
subsection {* Term representation *}
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Thu Feb 14 17:06:15 2013 +0100
@@ -22,23 +22,13 @@
lemma [code, code del]:
"pred_of_set = pred_of_set" ..
-
-lemma [code, code del]:
- "Cardinality.card' = Cardinality.card'" ..
-
-lemma [code, code del]:
- "Cardinality.finite' = Cardinality.finite'" ..
-
-lemma [code, code del]:
- "Cardinality.subset' = Cardinality.subset'" ..
-
-lemma [code, code del]:
- "Cardinality.eq_set = Cardinality.eq_set" ..
-
-
lemma [code, code del]:
"acc = acc" ..
+lemmas [code del] =
+ finite_set_code finite_coset_code
+ equal_set_code
+
(*
If the code generation ends with an exception with the following message:
'"List.set" is not a constructor, on left hand side of equation: ...',
--- a/src/HOL/Equiv_Relations.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Equiv_Relations.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* Equivalence Relations in Higher-Order Set Theory *}
theory Equiv_Relations
-imports Big_Operators Relation Plain
+imports Big_Operators Relation
begin
subsection {* Equivalence relations -- set version *}
--- a/src/HOL/Int.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Int.thy Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *}
theory Int
-imports Equiv_Relations Wellfounded Quotient
+imports Equiv_Relations Wellfounded Quotient FunDef
begin
subsection {* Definition of integers as a quotient type *}
--- a/src/HOL/Library/Cardinality.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Cardinality.thy Thu Feb 14 17:06:15 2013 +0100
@@ -199,7 +199,7 @@
subsection {* A type class for computing the cardinality of types *}
definition is_list_UNIV :: "'a list \<Rightarrow> bool"
-where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
+where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric]
@@ -211,15 +211,6 @@
fixes card_UNIV :: "'a card_UNIV"
assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
-lemma card_UNIV_code [code_unfold]:
- "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"
-by(simp add: card_UNIV)
-
-lemma is_list_UNIV_code [code]:
- "is_list_UNIV (xs :: 'a list) =
- (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
-by(rule is_list_UNIV_def)
-
subsection {* Instantiations for @{text "card_UNIV"} *}
instantiation nat :: card_UNIV begin
@@ -396,80 +387,66 @@
subsection {* Code setup for sets *}
+text {*
+ Implement operations @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, and @{term "op ="}
+ for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}.
+*}
+
lemma card_Compl:
"finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
-context fixes xs :: "'a :: card_UNIV list"
-begin
+lemma card_coset_code [code]:
+ fixes xs :: "'a :: card_UNIV list"
+ shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
+by(simp add: List.card_set card_Compl card_UNIV)
-definition card' :: "'a set \<Rightarrow> nat"
-where [simp, code del, code_abbrev]: "card' = card"
-
-lemma card'_code [code]:
- "card' (set xs) = length (remdups xs)"
- "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
-by(simp_all add: List.card_set card_Compl card_UNIV)
+lemma [code, code del]: "finite = finite" ..
-lemma card'_UNIV [code_unfold]:
- "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)"
-by(simp add: card_UNIV)
-
-definition finite' :: "'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "finite' = finite"
-
-lemma finite'_code [code]:
- "finite' (set xs) \<longleftrightarrow> True"
- "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
+lemma [code]:
+ fixes xs :: "'a :: card_UNIV list"
+ shows finite_set_code:
+ "finite (set xs) = True"
+ and finite_coset_code:
+ "finite (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
by(simp_all add: card_gt_0_iff finite_UNIV)
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
-
-lemma subset'_code [code]:
- "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
- "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
- "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
+lemma coset_subset_code [code]:
+ fixes xs :: "'a list" shows
+ "List.coset xs \<subseteq> set ys \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card (set (xs @ ys)) = n)"
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
(metis finite_compl finite_set rev_finite_subset)
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
-where [simp, code del, code_abbrev]: "eq_set = op ="
-
-lemma eq_set_code [code]:
- fixes ys
+lemma equal_set_code [code]:
+ fixes xs ys :: "'a :: equal list"
defines "rhs \<equiv>
let n = CARD('a)
in if n = 0 then False else
let xs' = remdups xs; ys' = remdups ys
in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
- shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
- and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
- and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
- and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
+ shows "equal_class.equal (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
+ and "equal_class.equal (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
+ and "equal_class.equal (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
+ and "equal_class.equal (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
proof -
show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs thus ?rhs
- by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
+ by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
next
assume ?rhs
moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
ultimately show ?lhs
- by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+ by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
qed
- thus ?thesis2 unfolding eq_set_def by blast
- show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
+ thus ?thesis2 unfolding equal_eq by blast
+ show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+
qed
-end
-
notepad begin (* test code setup *)
have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
by eval
end
-hide_const (open) card' finite' subset' eq_set
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,113 @@
+(* Title: HOL/Library/Code_Abstract_Nat.thy
+ Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+*)
+
+header {* Avoidance of pattern matching on natural numbers *}
+
+theory Code_Abstract_Nat
+imports Main
+begin
+
+text {*
+ When natural numbers are implemented in another than the
+ conventional inductive @{term "0::nat"}/@{term Suc} representation,
+ it is necessary to avoid all pattern matching on natural numbers
+ altogether. This is accomplished by this theory (up to a certain
+ extent).
+*}
+
+subsection {* Case analysis *}
+
+text {*
+ Case analysis on natural numbers is rephrased using a conditional
+ expression:
+*}
+
+lemma [code, code_unfold]:
+ "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+ by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
+
+
+subsection {* Preprocessors *}
+
+text {*
+ The term @{term "Suc n"} is no longer a valid pattern. Therefore,
+ all occurrences of this term in a position where a pattern is
+ expected (i.e.~on the left-hand side of a code equation) must be
+ eliminated. This can be accomplished – as far as possible – by
+ applying the following transformation rule:
+*}
+
+lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
+ f n \<equiv> if n = 0 then g else h (n - 1)"
+ by (rule eq_reflection) (cases n, simp_all)
+
+text {*
+ The rule above is built into a preprocessor that is plugged into
+ the code generator.
+*}
+
+setup {*
+let
+
+fun remove_suc thy thms =
+ let
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
+ val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
+ fun lhs_of th = snd (Thm.dest_comb
+ (fst (Thm.dest_comb (cprop_of th))));
+ fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
+ fun find_vars ct = (case term_of ct of
+ (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
+ | _ $ _ =>
+ let val (ct1, ct2) = Thm.dest_comb ct
+ in
+ map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
+ map (apfst (Thm.apply ct1)) (find_vars ct2)
+ end
+ | _ => []);
+ val eqs = maps
+ (fn th => map (pair th) (find_vars (lhs_of th))) thms;
+ fun mk_thms (th, (ct, cv')) =
+ let
+ val th' =
+ Thm.implies_elim
+ (Conv.fconv_rule (Thm.beta_conversion true)
+ (Drule.instantiate'
+ [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
+ SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
+ @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+ in
+ case map_filter (fn th'' =>
+ SOME (th'', singleton
+ (Variable.trade (K (fn [th'''] => [th''' RS th']))
+ (Variable.global_thm_context th'')) th'')
+ handle THM _ => NONE) thms of
+ [] => NONE
+ | thps =>
+ let val (ths1, ths2) = split_list thps
+ in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
+ end
+ in get_first mk_thms eqs end;
+
+fun eqn_suc_base_preproc thy thms =
+ let
+ val dest = fst o Logic.dest_equals o prop_of;
+ val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
+ in
+ if forall (can dest) thms andalso exists (contains_suc o dest) thms
+ then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
+ else NONE
+ end;
+
+val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
+
+in
+
+ Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
+
+end;
+*}
+
+end
--- a/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy Thu Feb 14 17:06:15 2013 +0100
@@ -1,11 +1,11 @@
(* Title: HOL/Library/Code_Binary_Nat.thy
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
*)
header {* Implementation of natural numbers as binary numerals *}
theory Code_Binary_Nat
-imports Main
+imports Code_Abstract_Nat
begin
text {*
@@ -146,104 +146,6 @@
by (simp_all add: nat_of_num_numeral)
-subsection {* Case analysis *}
-
-text {*
- Case analysis on natural numbers is rephrased using a conditional
- expression:
-*}
-
-lemma [code, code_unfold]:
- "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
- by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
-
-
-subsection {* Preprocessors *}
-
-text {*
- The term @{term "Suc n"} is no longer a valid pattern.
- Therefore, all occurrences of this term in a position
- where a pattern is expected (i.e.~on the left-hand side of a recursion
- equation) must be eliminated.
- This can be accomplished by applying the following transformation rules:
-*}
-
-lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
- f n \<equiv> if n = 0 then g else h (n - 1)"
- by (rule eq_reflection) (cases n, simp_all)
-
-text {*
- The rules above are built into a preprocessor that is plugged into
- the code generator. Since the preprocessor for introduction rules
- does not know anything about modes, some of the modes that worked
- for the canonical representation of natural numbers may no longer work.
-*}
-
-(*<*)
-setup {*
-let
-
-fun remove_suc thy thms =
- let
- val vname = singleton (Name.variant_list (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
- val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
- fun lhs_of th = snd (Thm.dest_comb
- (fst (Thm.dest_comb (cprop_of th))));
- fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
- fun find_vars ct = (case term_of ct of
- (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
- | _ $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct
- in
- map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
- map (apfst (Thm.apply ct1)) (find_vars ct2)
- end
- | _ => []);
- val eqs = maps
- (fn th => map (pair th) (find_vars (lhs_of th))) thms;
- fun mk_thms (th, (ct, cv')) =
- let
- val th' =
- Thm.implies_elim
- (Conv.fconv_rule (Thm.beta_conversion true)
- (Drule.instantiate'
- [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
- SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
- @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
- in
- case map_filter (fn th'' =>
- SOME (th'', singleton
- (Variable.trade (K (fn [th'''] => [th''' RS th']))
- (Variable.global_thm_context th'')) th'')
- handle THM _ => NONE) thms of
- [] => NONE
- | thps =>
- let val (ths1, ths2) = split_list thps
- in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
- end
- in get_first mk_thms eqs end;
-
-fun eqn_suc_base_preproc thy thms =
- let
- val dest = fst o Logic.dest_equals o prop_of;
- val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
- in
- if forall (can dest) thms andalso exists (contains_suc o dest) thms
- then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes
- else NONE
- end;
-
-val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
-
-in
-
- Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
-
-end;
-*}
-(*>*)
-
code_modulename SML
Code_Binary_Nat Arith
--- a/src/HOL/Library/Code_Numeral_Types.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Numeral_Types.thy Thu Feb 14 17:06:15 2013 +0100
@@ -13,9 +13,11 @@
typedef integer = "UNIV \<Colon> int set"
morphisms int_of_integer integer_of_int ..
+setup_lifting (no_code) type_definition_integer
+
lemma integer_eq_iff:
"k = l \<longleftrightarrow> int_of_integer k = int_of_integer l"
- using int_of_integer_inject [of k l] ..
+ by transfer rule
lemma integer_eqI:
"int_of_integer k = int_of_integer l \<Longrightarrow> k = l"
@@ -23,172 +25,199 @@
lemma int_of_integer_integer_of_int [simp]:
"int_of_integer (integer_of_int k) = k"
- using integer_of_int_inverse [of k] by simp
+ by transfer rule
lemma integer_of_int_int_of_integer [simp]:
"integer_of_int (int_of_integer k) = k"
- using int_of_integer_inverse [of k] by simp
+ by transfer rule
instantiation integer :: ring_1
begin
-definition
- "0 = integer_of_int 0"
+lift_definition zero_integer :: integer
+ is "0 :: int"
+ .
-lemma int_of_integer_zero [simp]:
- "int_of_integer 0 = 0"
- by (simp add: zero_integer_def)
-
-definition
- "1 = integer_of_int 1"
+declare zero_integer.rep_eq [simp]
-lemma int_of_integer_one [simp]:
- "int_of_integer 1 = 1"
- by (simp add: one_integer_def)
+lift_definition one_integer :: integer
+ is "1 :: int"
+ .
+
+declare one_integer.rep_eq [simp]
-definition
- "k + l = integer_of_int (int_of_integer k + int_of_integer l)"
+lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "plus :: int \<Rightarrow> int \<Rightarrow> int"
+ .
-lemma int_of_integer_plus [simp]:
- "int_of_integer (k + l) = int_of_integer k + int_of_integer l"
- by (simp add: plus_integer_def)
+declare plus_integer.rep_eq [simp]
-definition
- "- k = integer_of_int (- int_of_integer k)"
+lift_definition uminus_integer :: "integer \<Rightarrow> integer"
+ is "uminus :: int \<Rightarrow> int"
+ .
-lemma int_of_integer_uminus [simp]:
- "int_of_integer (- k) = - int_of_integer k"
- by (simp add: uminus_integer_def)
-
-definition
- "k - l = integer_of_int (int_of_integer k - int_of_integer l)"
+declare uminus_integer.rep_eq [simp]
-lemma int_of_integer_minus [simp]:
- "int_of_integer (k - l) = int_of_integer k - int_of_integer l"
- by (simp add: minus_integer_def)
+lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "minus :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare minus_integer.rep_eq [simp]
-definition
- "k * l = integer_of_int (int_of_integer k * int_of_integer l)"
+lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "times :: int \<Rightarrow> int \<Rightarrow> int"
+ .
-lemma int_of_integer_times [simp]:
- "int_of_integer (k * l) = int_of_integer k * int_of_integer l"
- by (simp add: times_integer_def)
+declare times_integer.rep_eq [simp]
instance proof
-qed (auto simp add: integer_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
end
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+ by (unfold of_nat_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+proof -
+ have "fun_rel HOL.eq cr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+ by (unfold of_int_of_nat [abs_def]) transfer_prover
+ then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
+proof -
+ have "fun_rel HOL.eq cr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))"
+ by transfer_prover
+ then show ?thesis by simp
+qed
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer (neg_numeral :: num \<Rightarrow> int) (neg_numeral :: num \<Rightarrow> integer)"
+ by (unfold neg_numeral_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq (fun_rel HOL.eq cr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold Num.sub_def [abs_def]) transfer_prover
+
lemma int_of_integer_of_nat [simp]:
"int_of_integer (of_nat n) = of_nat n"
- by (induct n) simp_all
+ by transfer rule
-definition integer_of_nat :: "nat \<Rightarrow> integer"
-where
- "integer_of_nat = of_nat"
+lift_definition integer_of_nat :: "nat \<Rightarrow> integer"
+ is "of_nat :: nat \<Rightarrow> int"
+ .
lemma int_of_integer_integer_of_nat [simp]:
"int_of_integer (integer_of_nat n) = of_nat n"
- by (simp add: integer_of_nat_def)
-
-definition nat_of_integer :: "integer \<Rightarrow> nat"
-where
- "nat_of_integer k = Int.nat (int_of_integer k)"
+ by transfer rule
+
+lift_definition nat_of_integer :: "integer \<Rightarrow> nat"
+ is Int.nat
+ .
lemma nat_of_integer_of_nat [simp]:
"nat_of_integer (of_nat n) = n"
- by (simp add: nat_of_integer_def)
+ by transfer simp
lemma int_of_integer_of_int [simp]:
"int_of_integer (of_int k) = k"
- by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one)
+ by transfer simp
lemma nat_of_integer_integer_of_nat [simp]:
"nat_of_integer (integer_of_nat n) = n"
- by (simp add: integer_of_nat_def)
+ by transfer simp
lemma integer_of_int_eq_of_int [simp, code_abbrev]:
"integer_of_int = of_int"
- by rule (simp add: integer_eq_iff)
+ by transfer (simp add: fun_eq_iff)
lemma of_int_integer_of [simp]:
"of_int (int_of_integer k) = (k :: integer)"
- by (simp add: integer_eq_iff)
+ by transfer rule
lemma int_of_integer_numeral [simp]:
"int_of_integer (numeral k) = numeral k"
- using int_of_integer_of_int [of "numeral k"] by simp
+ by transfer rule
lemma int_of_integer_neg_numeral [simp]:
"int_of_integer (neg_numeral k) = neg_numeral k"
- by (simp only: neg_numeral_def int_of_integer_uminus) simp
+ by transfer rule
lemma int_of_integer_sub [simp]:
"int_of_integer (Num.sub k l) = Num.sub k l"
- by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral)
+ by transfer rule
instantiation integer :: "{ring_div, equal, linordered_idom}"
begin
-definition
- "k div l = of_int (int_of_integer k div int_of_integer l)"
+lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int"
+ .
-lemma int_of_integer_div [simp]:
- "int_of_integer (k div l) = int_of_integer k div int_of_integer l"
- by (simp add: div_integer_def)
+declare div_integer.rep_eq [simp]
-definition
- "k mod l = of_int (int_of_integer k mod int_of_integer l)"
+lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+ is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int"
+ .
+
+declare mod_integer.rep_eq [simp]
-lemma int_of_integer_mod [simp]:
- "int_of_integer (k mod l) = int_of_integer k mod int_of_integer l"
- by (simp add: mod_integer_def)
+lift_definition abs_integer :: "integer \<Rightarrow> integer"
+ is "abs :: int \<Rightarrow> int"
+ .
-definition
- "\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>"
+declare abs_integer.rep_eq [simp]
-lemma int_of_integer_abs [simp]:
- "int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>"
- by (simp add: abs_integer_def)
+lift_definition sgn_integer :: "integer \<Rightarrow> integer"
+ is "sgn :: int \<Rightarrow> int"
+ .
-definition
- "sgn k = of_int (sgn (int_of_integer k))"
+declare sgn_integer.rep_eq [simp]
-lemma int_of_integer_sgn [simp]:
- "int_of_integer (sgn k) = sgn (int_of_integer k)"
- by (simp add: sgn_integer_def)
+lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
-definition
- "k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l"
+lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "less :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
-definition
- "k < l \<longleftrightarrow> int_of_integer k < int_of_integer l"
-
-definition
- "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)"
+lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
+ is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool"
+ .
instance proof
-qed (auto simp add: integer_eq_iff algebra_simps
- less_eq_integer_def less_integer_def equal_integer_def equal
- intro: mult_strict_right_mono)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
end
+lemma [transfer_rule]:
+ "fun_rel cr_integer (fun_rel cr_integer cr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel cr_integer (fun_rel cr_integer cr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+ by (unfold max_def [abs_def]) transfer_prover
+
lemma int_of_integer_min [simp]:
"int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
- by (simp add: min_def less_eq_integer_def)
+ by transfer rule
lemma int_of_integer_max [simp]:
"int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)"
- by (simp add: max_def less_eq_integer_def)
+ by transfer rule
lemma nat_of_integer_non_positive [simp]:
"k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
- by (simp add: nat_of_integer_def less_eq_integer_def)
+ by transfer simp
lemma of_nat_of_integer [simp]:
"of_nat (nat_of_integer k) = max 0 k"
- by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def)
+ by transfer auto
subsection {* Code theorems for target language integers *}
@@ -199,29 +228,36 @@
where
[simp, code_abbrev]: "Pos = numeral"
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer numeral Pos"
+ by simp transfer_prover
+
definition Neg :: "num \<Rightarrow> integer"
where
[simp, code_abbrev]: "Neg = neg_numeral"
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_integer neg_numeral Neg"
+ by simp transfer_prover
+
code_datatype "0::integer" Pos Neg
text {* Auxiliary operations *}
-definition dup :: "integer \<Rightarrow> integer"
-where
- [simp]: "dup k = k + k"
+lift_definition dup :: "integer \<Rightarrow> integer"
+ is "\<lambda>k::int. k + k"
+ .
lemma dup_code [code]:
"dup 0 = 0"
"dup (Pos n) = Pos (Num.Bit0 n)"
"dup (Neg n) = Neg (Num.Bit0 n)"
- unfolding Pos_def Neg_def neg_numeral_def
- by (simp_all add: numeral_Bit0)
+ by (transfer, simp only: neg_numeral_def numeral_Bit0 minus_add_distrib)+
-definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
-where
- [simp]: "sub m n = numeral m - numeral n"
+lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer"
+ is "\<lambda>m n. numeral m - numeral n :: int"
+ .
lemma sub_code [code]:
"sub Num.One Num.One = 0"
@@ -233,9 +269,7 @@
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
- unfolding sub_def dup_def numeral.simps Pos_def Neg_def
- neg_numeral_def numeral_BitM
- by (simp_all only: algebra_simps add.comm_neutral)
+ by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
text {* Implementations *}
@@ -251,7 +285,7 @@
"Pos m + Neg n = sub m n"
"Neg m + Pos n = sub n m"
"Neg m + Neg n = Neg (m + n)"
- by simp_all
+ by (transfer, simp)+
lemma uminus_integer_code [code]:
"uminus 0 = (0::integer)"
@@ -266,7 +300,7 @@
"Pos m - Neg n = Pos (m + n)"
"Neg m - Pos n = Neg (m + n)"
"Neg m - Neg n = sub n m"
- by simp_all
+ by (transfer, simp)+
lemma abs_integer_code [code]:
"\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)"
@@ -322,15 +356,18 @@
(let j = sub k l in
if j < 0 then (0, Pos k)
else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
- by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta
- sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+ apply (simp add: prod_eq_iff Let_def prod_case_beta)
+ apply transfer
+ apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
+ done
-lemma divmod_integer_code [code]: "divmod_integer k l =
- (if k = 0 then (0, 0) else if l = 0 then (0, k) else
- (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
- then divmod_abs k l
- else (let (r, s) = divmod_abs k l in
- if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+lemma divmod_integer_code [code]:
+ "divmod_integer k l =
+ (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+ (apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l
+ then divmod_abs k l
+ else (let (r, s) = divmod_abs k l in
+ if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
proof -
have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0"
by (auto simp add: sgn_if)
@@ -358,7 +395,7 @@
"HOL.equal (Neg k) 0 \<longleftrightarrow> False"
"HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
"HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
- by (simp_all add: equal integer_eq_iff)
+ by (simp_all add: equal)
lemma equal_integer_refl [code nbe]:
"HOL.equal (k::integer) k \<longleftrightarrow> True"
@@ -374,7 +411,7 @@
"Neg k \<le> 0 \<longleftrightarrow> True"
"Neg k \<le> Pos l \<longleftrightarrow> True"
"Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
- by (simp_all add: less_eq_integer_def)
+ by simp_all
lemma less_integer_code [code]:
"0 < (0::integer) \<longleftrightarrow> False"
@@ -386,21 +423,21 @@
"Neg k < 0 \<longleftrightarrow> True"
"Neg k < Pos l \<longleftrightarrow> True"
"Neg k < Neg l \<longleftrightarrow> l < k"
- by (simp_all add: less_integer_def)
+ by simp_all
-definition integer_of_num :: "num \<Rightarrow> integer"
-where
- "integer_of_num = numeral"
+lift_definition integer_of_num :: "num \<Rightarrow> integer"
+ is "numeral :: num \<Rightarrow> int"
+ .
lemma integer_of_num [code]:
"integer_of_num num.One = 1"
"integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
"integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
- by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps)
+ by (transfer, simp only: numeral.simps Let_def)+
-definition num_of_integer :: "integer \<Rightarrow> num"
-where
- "num_of_integer = num_of_nat \<circ> nat_of_integer"
+lift_definition num_of_integer :: "integer \<Rightarrow> num"
+ is "num_of_nat \<circ> nat"
+ .
lemma num_of_integer_code [code]:
"num_of_integer k = (if k \<le> 1 then Num.One
@@ -587,9 +624,11 @@
typedef natural = "UNIV \<Colon> nat set"
morphisms nat_of_natural natural_of_nat ..
+setup_lifting (no_code) type_definition_natural
+
lemma natural_eq_iff [termination_simp]:
"m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n"
- using nat_of_natural_inject [of m n] ..
+ by transfer rule
lemma natural_eqI:
"nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n"
@@ -597,168 +636,179 @@
lemma nat_of_natural_of_nat_inverse [simp]:
"nat_of_natural (natural_of_nat n) = n"
- using natural_of_nat_inverse [of n] by simp
+ by transfer rule
lemma natural_of_nat_of_natural_inverse [simp]:
"natural_of_nat (nat_of_natural n) = n"
- using nat_of_natural_inverse [of n] by simp
+ by transfer rule
instantiation natural :: "{comm_monoid_diff, semiring_1}"
begin
-definition
- "0 = natural_of_nat 0"
+lift_definition zero_natural :: natural
+ is "0 :: nat"
+ .
-lemma nat_of_natural_zero [simp]:
- "nat_of_natural 0 = 0"
- by (simp add: zero_natural_def)
+declare zero_natural.rep_eq [simp]
-definition
- "1 = natural_of_nat 1"
+lift_definition one_natural :: natural
+ is "1 :: nat"
+ .
-lemma nat_of_natural_one [simp]:
- "nat_of_natural 1 = 1"
- by (simp add: one_natural_def)
-
-definition
- "m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)"
+declare one_natural.rep_eq [simp]
-lemma nat_of_natural_plus [simp]:
- "nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n"
- by (simp add: plus_natural_def)
+lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
-definition
- "m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)"
+declare plus_natural.rep_eq [simp]
-lemma nat_of_natural_minus [simp]:
- "nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n"
- by (simp add: minus_natural_def)
+lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare minus_natural.rep_eq [simp]
-definition
- "m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)"
+lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "times :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
-lemma nat_of_natural_times [simp]:
- "nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n"
- by (simp add: times_natural_def)
+declare times_natural.rep_eq [simp]
instance proof
-qed (auto simp add: natural_eq_iff algebra_simps)
+qed (transfer, simp add: algebra_simps)+
end
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
+proof -
+ have "fun_rel HOL.eq cr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
+ by (unfold of_nat_def [abs_def]) transfer_prover
+ then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+ "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+proof -
+ have "fun_rel HOL.eq cr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+ by transfer_prover
+ then show ?thesis by simp
+qed
+
lemma nat_of_natural_of_nat [simp]:
"nat_of_natural (of_nat n) = n"
- by (induct n) simp_all
+ by transfer rule
lemma natural_of_nat_of_nat [simp, code_abbrev]:
"natural_of_nat = of_nat"
- by rule (simp add: natural_eq_iff)
+ by transfer rule
lemma of_nat_of_natural [simp]:
"of_nat (nat_of_natural n) = n"
- using natural_of_nat_of_natural_inverse [of n] by simp
+ by transfer rule
lemma nat_of_natural_numeral [simp]:
"nat_of_natural (numeral k) = numeral k"
- using nat_of_natural_of_nat [of "numeral k"] by simp
+ by transfer rule
instantiation natural :: "{semiring_div, equal, linordered_semiring}"
begin
-definition
- "m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)"
+lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
+
+declare div_natural.rep_eq [simp]
-lemma nat_of_natural_div [simp]:
- "nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n"
- by (simp add: div_natural_def)
+lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
+ is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
+ .
-definition
- "m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)"
+declare mod_natural.rep_eq [simp]
-lemma nat_of_natural_mod [simp]:
- "nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n"
- by (simp add: mod_natural_def)
+lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
+
+declare less_eq_natural.rep_eq [termination_simp]
-definition
- [termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n"
+lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "less :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
-definition
- [termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n"
+declare less_natural.rep_eq [termination_simp]
-definition
- "HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)"
+lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
+ is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool"
+ .
instance proof
-qed (auto simp add: natural_eq_iff algebra_simps
- less_eq_natural_def less_natural_def equal_natural_def equal)
+qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
end
+lemma [transfer_rule]:
+ "fun_rel cr_natural (fun_rel cr_natural cr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ by (unfold min_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "fun_rel cr_natural (fun_rel cr_natural cr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+ by (unfold max_def [abs_def]) transfer_prover
+
lemma nat_of_natural_min [simp]:
"nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
- by (simp add: min_def less_eq_natural_def)
+ by transfer rule
lemma nat_of_natural_max [simp]:
"nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
- by (simp add: max_def less_eq_natural_def)
+ by transfer rule
-definition natural_of_integer :: "integer \<Rightarrow> natural"
-where
- "natural_of_integer = of_nat \<circ> nat_of_integer"
+lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
+ is "nat :: int \<Rightarrow> nat"
+ .
-definition integer_of_natural :: "natural \<Rightarrow> integer"
-where
- "integer_of_natural = of_nat \<circ> nat_of_natural"
+lift_definition integer_of_natural :: "natural \<Rightarrow> integer"
+ is "of_nat :: nat \<Rightarrow> int"
+ .
lemma natural_of_integer_of_natural [simp]:
"natural_of_integer (integer_of_natural n) = n"
- by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff)
+ by transfer simp
lemma integer_of_natural_of_integer [simp]:
"integer_of_natural (natural_of_integer k) = max 0 k"
- by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff)
+ by transfer auto
lemma int_of_integer_of_natural [simp]:
"int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)"
- by (simp add: integer_of_natural_def)
+ by transfer rule
lemma integer_of_natural_of_nat [simp]:
"integer_of_natural (of_nat n) = of_nat n"
- by (simp add: integer_eq_iff)
+ by transfer rule
lemma [measure_function]:
- "is_measure nat_of_natural" by (rule is_measure_trivial)
+ "is_measure nat_of_natural"
+ by (rule is_measure_trivial)
subsection {* Inductive represenation of target language naturals *}
-definition Suc :: "natural \<Rightarrow> natural"
-where
- "Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural"
+lift_definition Suc :: "natural \<Rightarrow> natural"
+ is Nat.Suc
+ .
-lemma nat_of_natural_Suc [simp]:
- "nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)"
- by (simp add: Suc_def)
+declare Suc.rep_eq [simp]
rep_datatype "0::natural" Suc
-proof -
- fix P :: "natural \<Rightarrow> bool"
- fix n :: natural
- assume "P 0" then have init: "P (natural_of_nat 0)" by simp
- assume "\<And>n. P n \<Longrightarrow> P (Suc n)"
- then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" .
- then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))"
- by (simp add: Suc_def)
- from init step have "P (natural_of_nat (nat_of_natural n))"
- by (rule nat.induct)
- with natural_of_nat_of_natural_inverse show "P n" by simp
-qed (simp_all add: natural_eq_iff)
+ by (transfer, fact nat.induct nat.inject nat.distinct)+
lemma natural_case [case_names nat, cases type: natural]:
fixes m :: natural
assumes "\<And>n. m = of_nat n \<Longrightarrow> P"
shows P
- by (rule assms [of "nat_of_natural m"]) simp
+ using assms by transfer blast
lemma [simp, code]:
"natural_size = nat_of_natural"
@@ -778,7 +828,7 @@
lemma natural_decr [termination_simp]:
"n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
- by (simp add: natural_eq_iff)
+ by transfer simp
lemma natural_zero_minus_one:
"(0::natural) - 1 = 0"
@@ -786,26 +836,26 @@
lemma Suc_natural_minus_one:
"Suc n - 1 = n"
- by (simp add: natural_eq_iff)
+ by transfer simp
hide_const (open) Suc
subsection {* Code refinement for target language naturals *}
-definition Nat :: "integer \<Rightarrow> natural"
-where
- "Nat = natural_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> natural"
+ is nat
+ .
lemma [code_post]:
"Nat 0 = 0"
"Nat 1 = 1"
"Nat (numeral k) = numeral k"
- by (simp_all add: Nat_def nat_of_integer_def natural_of_integer_def)
+ by (transfer, simp)+
lemma [code abstype]:
"Nat (integer_of_natural n) = n"
- by (unfold Nat_def) (fact natural_of_integer_of_natural)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (natural_of_nat n) = of_nat n"
@@ -817,23 +867,23 @@
lemma [code_abbrev]:
"natural_of_integer (Code_Numeral_Types.Pos k) = numeral k"
- by (simp add: nat_of_integer_def natural_of_integer_def)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural 0 = 0"
- by (simp add: integer_eq_iff)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural 1 = 1"
- by (simp add: integer_eq_iff)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1"
- by (simp add: integer_eq_iff)
+ by transfer simp
lemma [code]:
"nat_of_natural = nat_of_integer \<circ> integer_of_natural"
- by (simp add: integer_of_natural_def fun_eq_iff)
+ by transfer (simp add: fun_eq_iff)
lemma [code, code_unfold]:
"natural_case f g n = (if n = 0 then f else g (n - 1))"
@@ -843,39 +893,39 @@
lemma [code abstract]:
"integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"
- by (simp add: integer_eq_iff)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)"
- by (simp add: integer_eq_iff)
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
- by (simp add: integer_eq_iff of_nat_mult)
+ by transfer (simp add: of_nat_mult)
lemma [code abstract]:
"integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
- by (simp add: integer_eq_iff zdiv_int)
+ by transfer (simp add: zdiv_int)
lemma [code abstract]:
"integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n"
- by (simp add: integer_eq_iff zmod_int)
+ by transfer (simp add: zmod_int)
lemma [code]:
"HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)"
- by (simp add: equal natural_eq_iff integer_eq_iff)
+ by transfer (simp add: equal)
lemma [code nbe]:
"HOL.equal n (n::natural) \<longleftrightarrow> True"
by (simp add: equal)
lemma [code]:
- "m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n"
- by (simp add: less_eq_natural_def less_eq_integer_def)
+ "m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n"
+ by transfer simp
lemma [code]:
- "m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n"
- by (simp add: less_natural_def less_integer_def)
+ "m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n"
+ by transfer simp
hide_const (open) Nat
--- a/src/HOL/Library/Code_Target_Int.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Target_Int.thy Thu Feb 14 17:06:15 2013 +0100
@@ -15,47 +15,47 @@
lemma [code]:
"integer_of_int (int_of_integer k) = k"
- by (simp add: integer_eq_iff)
+ by transfer rule
lemma [code]:
"Int.Pos = int_of_integer \<circ> integer_of_num"
- by (simp add: integer_of_num_def fun_eq_iff)
+ by transfer (simp add: fun_eq_iff)
lemma [code]:
"Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
- by (simp add: integer_of_num_def fun_eq_iff)
+ by transfer (simp add: fun_eq_iff)
lemma [code_abbrev]:
"int_of_integer (numeral k) = Int.Pos k"
- by simp
+ by transfer simp
lemma [code_abbrev]:
"int_of_integer (neg_numeral k) = Int.Neg k"
- by simp
+ by transfer simp
lemma [code, symmetric, code_post]:
"0 = int_of_integer 0"
- by simp
+ by transfer simp
lemma [code, symmetric, code_post]:
"1 = int_of_integer 1"
- by simp
+ by transfer simp
lemma [code]:
"k + l = int_of_integer (of_int k + of_int l)"
- by simp
+ by transfer simp
lemma [code]:
"- k = int_of_integer (- of_int k)"
- by simp
+ by transfer simp
lemma [code]:
"k - l = int_of_integer (of_int k - of_int l)"
- by simp
+ by transfer simp
lemma [code]:
"Int.dup k = int_of_integer (Code_Numeral_Types.dup (of_int k))"
- by simp
+ by transfer simp
lemma [code, code del]:
"Int.sub = Int.sub" ..
@@ -79,15 +79,15 @@
lemma [code]:
"HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)"
- by (simp add: equal integer_eq_iff)
+ by transfer (simp add: equal)
lemma [code]:
"k \<le> l \<longleftrightarrow> (of_int k :: integer) \<le> of_int l"
- by (simp add: less_eq_int_def)
+ by transfer rule
lemma [code]:
"k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
- by (simp add: less_int_def)
+ by transfer rule
lemma (in ring_1) of_int_code:
"of_int k = (if k = 0 then 0
@@ -107,7 +107,7 @@
lemma [code]:
"nat = nat_of_integer \<circ> of_int"
- by (simp add: fun_eq_iff nat_of_integer_def)
+ by transfer (simp add: fun_eq_iff)
code_modulename SML
Code_Target_Int Arith
--- a/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Code_Target_Nat.thy Thu Feb 14 17:06:15 2013 +0100
@@ -1,83 +1,80 @@
(* Title: HOL/Library/Code_Target_Nat.thy
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
*)
header {* Implementation of natural numbers by target-language integers *}
theory Code_Target_Nat
-imports Main Code_Numeral_Types Code_Binary_Nat
+imports Code_Abstract_Nat Code_Numeral_Types
begin
subsection {* Implementation for @{typ nat} *}
-definition Nat :: "integer \<Rightarrow> nat"
-where
- "Nat = nat_of_integer"
+lift_definition Nat :: "integer \<Rightarrow> nat"
+ is nat
+ .
lemma [code_post]:
"Nat 0 = 0"
"Nat 1 = 1"
"Nat (numeral k) = numeral k"
- by (simp_all add: Nat_def nat_of_integer_def)
+ by (transfer, simp)+
lemma [code_abbrev]:
"integer_of_nat = of_nat"
- by (fact integer_of_nat_def)
+ by transfer rule
lemma [code_unfold]:
"Int.nat (int_of_integer k) = nat_of_integer k"
- by (simp add: nat_of_integer_def)
+ by transfer rule
lemma [code abstype]:
"Code_Target_Nat.Nat (integer_of_nat n) = n"
- by (simp add: Nat_def integer_of_nat_def)
+ by transfer simp
lemma [code abstract]:
"integer_of_nat (nat_of_integer k) = max 0 k"
- by (simp add: integer_of_nat_def)
+ by transfer auto
lemma [code_abbrev]:
"nat_of_integer (numeral k) = nat_of_num k"
- by (simp add: nat_of_integer_def nat_of_num_numeral)
+ by transfer (simp add: nat_of_num_numeral)
lemma [code abstract]:
"integer_of_nat (nat_of_num n) = integer_of_num n"
- by (simp add: integer_eq_iff integer_of_num_def nat_of_num_numeral)
+ by transfer (simp add: nat_of_num_numeral)
lemma [code abstract]:
"integer_of_nat 0 = 0"
- by (simp add: integer_eq_iff integer_of_nat_def)
+ by transfer simp
lemma [code abstract]:
"integer_of_nat 1 = 1"
- by (simp add: integer_eq_iff integer_of_nat_def)
+ by transfer simp
+
+lemma [code]:
+ "Suc n = n + 1"
+ by simp
lemma [code abstract]:
"integer_of_nat (m + n) = of_nat m + of_nat n"
- by (simp add: integer_eq_iff integer_of_nat_def)
-
-lemma [code abstract]:
- "integer_of_nat (Code_Binary_Nat.dup n) = Code_Numeral_Types.dup (of_nat n)"
- by (simp add: integer_eq_iff Code_Binary_Nat.dup_def integer_of_nat_def)
-
-lemma [code, code del]:
- "Code_Binary_Nat.sub = Code_Binary_Nat.sub" ..
+ by transfer simp
lemma [code abstract]:
"integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)"
- by (simp add: integer_eq_iff integer_of_nat_def)
+ by transfer simp
lemma [code abstract]:
"integer_of_nat (m * n) = of_nat m * of_nat n"
- by (simp add: integer_eq_iff of_nat_mult integer_of_nat_def)
+ by transfer (simp add: of_nat_mult)
lemma [code abstract]:
"integer_of_nat (m div n) = of_nat m div of_nat n"
- by (simp add: integer_eq_iff zdiv_int integer_of_nat_def)
+ by transfer (simp add: zdiv_int)
lemma [code abstract]:
"integer_of_nat (m mod n) = of_nat m mod of_nat n"
- by (simp add: integer_eq_iff zmod_int integer_of_nat_def)
+ by transfer (simp add: zmod_int)
lemma [code]:
"Divides.divmod_nat m n = (m div n, m mod n)"
@@ -85,7 +82,7 @@
lemma [code]:
"HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)"
- by (simp add: equal integer_eq_iff)
+ by transfer (simp add: equal)
lemma [code]:
"m \<le> n \<longleftrightarrow> (of_nat m :: integer) \<le> of_nat n"
@@ -97,7 +94,7 @@
lemma num_of_nat_code [code]:
"num_of_nat = num_of_integer \<circ> of_nat"
- by (simp add: fun_eq_iff num_of_integer_def integer_of_nat_def)
+ by transfer (simp add: fun_eq_iff)
lemma (in semiring_1) of_nat_code:
"of_nat n = (if n = 0 then 0
@@ -124,7 +121,7 @@
lemma [code abstract]:
"integer_of_nat (nat k) = max 0 (integer_of_int k)"
- by (simp add: integer_of_nat_def of_int_of_nat max_def)
+ by transfer auto
code_modulename SML
Code_Target_Nat Arith
--- a/src/HOL/Library/Finite_Lattice.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/Finite_Lattice.thy Thu Feb 14 17:06:15 2013 +0100
@@ -1,7 +1,7 @@
(* Author: Alessandro Coglio *)
theory Finite_Lattice
-imports Product_Lattice
+imports Product_Order
begin
text {* A non-empty finite lattice is a complete lattice.
--- a/src/HOL/Library/Product_Lattice.thy Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,238 +0,0 @@
-(* Title: HOL/Library/Product_Lattice.thy
- Author: Brian Huffman
-*)
-
-header {* Lattice operations on product types *}
-
-theory Product_Lattice
-imports "~~/src/HOL/Library/Product_plus"
-begin
-
-subsection {* Pointwise ordering *}
-
-instantiation prod :: (ord, ord) ord
-begin
-
-definition
- "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
-
-definition
- "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
-
-instance ..
-
-end
-
-lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
- unfolding less_eq_prod_def by simp
-
-lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
- unfolding less_eq_prod_def by simp
-
-lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
- unfolding less_eq_prod_def by simp
-
-lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
- unfolding less_eq_prod_def by simp
-
-instance prod :: (preorder, preorder) preorder
-proof
- fix x y z :: "'a \<times> 'b"
- show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
- by (rule less_prod_def)
- show "x \<le> x"
- unfolding less_eq_prod_def
- by fast
- assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
- unfolding less_eq_prod_def
- by (fast elim: order_trans)
-qed
-
-instance prod :: (order, order) order
- by default auto
-
-
-subsection {* Binary infimum and supremum *}
-
-instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
-begin
-
-definition
- "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
-
-lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
- unfolding inf_prod_def by simp
-
-lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
- unfolding inf_prod_def by simp
-
-lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
- unfolding inf_prod_def by simp
-
-instance
- by default auto
-
-end
-
-instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
-begin
-
-definition
- "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
-
-lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
- unfolding sup_prod_def by simp
-
-lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
- unfolding sup_prod_def by simp
-
-lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
- unfolding sup_prod_def by simp
-
-instance
- by default auto
-
-end
-
-instance prod :: (lattice, lattice) lattice ..
-
-instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
- by default (auto simp add: sup_inf_distrib1)
-
-
-subsection {* Top and bottom elements *}
-
-instantiation prod :: (top, top) top
-begin
-
-definition
- "top = (top, top)"
-
-lemma fst_top [simp]: "fst top = top"
- unfolding top_prod_def by simp
-
-lemma snd_top [simp]: "snd top = top"
- unfolding top_prod_def by simp
-
-lemma Pair_top_top: "(top, top) = top"
- unfolding top_prod_def by simp
-
-instance
- by default (auto simp add: top_prod_def)
-
-end
-
-instantiation prod :: (bot, bot) bot
-begin
-
-definition
- "bot = (bot, bot)"
-
-lemma fst_bot [simp]: "fst bot = bot"
- unfolding bot_prod_def by simp
-
-lemma snd_bot [simp]: "snd bot = bot"
- unfolding bot_prod_def by simp
-
-lemma Pair_bot_bot: "(bot, bot) = bot"
- unfolding bot_prod_def by simp
-
-instance
- by default (auto simp add: bot_prod_def)
-
-end
-
-instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
-
-instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
- by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
-
-
-subsection {* Complete lattice operations *}
-
-instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
-begin
-
-definition
- "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
-
-definition
- "Inf A = (INF x:A. fst x, INF x:A. snd x)"
-
-instance
- by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
- INF_lower SUP_upper le_INF_iff SUP_le_iff)
-
-end
-
-lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
- unfolding Sup_prod_def by simp
-
-lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
- unfolding Sup_prod_def by simp
-
-lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
- unfolding Inf_prod_def by simp
-
-lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
- unfolding Inf_prod_def by simp
-
-lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
- by (simp add: SUP_def fst_Sup image_image)
-
-lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
- by (simp add: SUP_def snd_Sup image_image)
-
-lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
- by (simp add: INF_def fst_Inf image_image)
-
-lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
- by (simp add: INF_def snd_Inf image_image)
-
-lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
- by (simp add: SUP_def Sup_prod_def image_image)
-
-lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
- by (simp add: INF_def Inf_prod_def image_image)
-
-
-text {* Alternative formulations for set infima and suprema over the product
-of two complete lattices: *}
-
-lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
-by (auto simp: Inf_prod_def INF_def)
-
-lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
-by (auto simp: Sup_prod_def SUP_def)
-
-lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_compose)
-
-lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_compose)
-
-lemma INF_prod_alt_def:
- "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
-by (metis fst_INF snd_INF surjective_pairing)
-
-lemma SUP_prod_alt_def:
- "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
-by (metis fst_SUP snd_SUP surjective_pairing)
-
-
-subsection {* Complete distributive lattices *}
-
-(* Contribution: Alessandro Coglio *)
-
-instance prod ::
- (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof
- case goal1 thus ?case
- by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
-next
- case goal2 thus ?case
- by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
-qed
-
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Lexorder.thy Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,125 @@
+(* Title: HOL/Library/Product_Lexorder.thy
+ Author: Norbert Voelker
+*)
+
+header {* Lexicographic order on product types *}
+
+theory Product_Lexorder
+imports Main
+begin
+
+instantiation prod :: (ord, ord) ord
+begin
+
+definition
+ "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
+
+definition
+ "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
+
+instance ..
+
+end
+
+lemma less_eq_prod_simp [simp, code]:
+ "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+ by (simp add: less_eq_prod_def)
+
+lemma less_prod_simp [simp, code]:
+ "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+ by (simp add: less_prod_def)
+
+text {* A stronger version for partial orders. *}
+
+lemma less_prod_def':
+ fixes x y :: "'a::order \<times> 'b::ord"
+ shows "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+ by (auto simp add: less_prod_def le_less)
+
+instance prod :: (preorder, preorder) preorder
+ by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
+
+instance prod :: (order, order) order
+ by default (auto simp add: less_eq_prod_def)
+
+instance prod :: (linorder, linorder) linorder
+ by default (auto simp: less_eq_prod_def)
+
+instantiation prod :: (linorder, linorder) distrib_lattice
+begin
+
+definition
+ "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+
+definition
+ "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+
+instance
+ by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
+
+end
+
+instantiation prod :: (bot, bot) bot
+begin
+
+definition
+ "bot = (bot, bot)"
+
+instance
+ by default (auto simp add: bot_prod_def)
+
+end
+
+instantiation prod :: (top, top) top
+begin
+
+definition
+ "top = (top, top)"
+
+instance
+ by default (auto simp add: top_prod_def)
+
+end
+
+instance prod :: (wellorder, wellorder) wellorder
+proof
+ fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
+ assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+ show "P z"
+ proof (induct z)
+ case (Pair a b)
+ show "P (a, b)"
+ proof (induct a arbitrary: b rule: less_induct)
+ case (less a\<^isub>1) note a\<^isub>1 = this
+ show "P (a\<^isub>1, b)"
+ proof (induct b rule: less_induct)
+ case (less b\<^isub>1) note b\<^isub>1 = this
+ show "P (a\<^isub>1, b\<^isub>1)"
+ proof (rule P)
+ fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
+ show "P p"
+ proof (cases "fst p < a\<^isub>1")
+ case True
+ then have "P (fst p, snd p)" by (rule a\<^isub>1)
+ then show ?thesis by simp
+ next
+ case False
+ with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
+ by (simp_all add: less_prod_def')
+ from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
+ with 1 show ?thesis by simp
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
+
+text {* Legacy lemma bindings *}
+
+lemmas prod_le_def = less_eq_prod_def
+lemmas prod_less_def = less_prod_def
+lemmas prod_less_eq = less_prod_def'
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Product_Order.thy Thu Feb 14 17:06:15 2013 +0100
@@ -0,0 +1,238 @@
+(* Title: HOL/Library/Product_Order.thy
+ Author: Brian Huffman
+*)
+
+header {* Pointwise order on product types *}
+
+theory Product_Order
+imports "~~/src/HOL/Library/Product_plus"
+begin
+
+subsection {* Pointwise ordering *}
+
+instantiation prod :: (ord, ord) ord
+begin
+
+definition
+ "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y"
+
+definition
+ "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+
+instance ..
+
+end
+
+lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y"
+ unfolding less_eq_prod_def by simp
+
+lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y"
+ unfolding less_eq_prod_def by simp
+
+lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')"
+ unfolding less_eq_prod_def by simp
+
+lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
+ unfolding less_eq_prod_def by simp
+
+instance prod :: (preorder, preorder) preorder
+proof
+ fix x y z :: "'a \<times> 'b"
+ show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+ by (rule less_prod_def)
+ show "x \<le> x"
+ unfolding less_eq_prod_def
+ by fast
+ assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
+ unfolding less_eq_prod_def
+ by (fast elim: order_trans)
+qed
+
+instance prod :: (order, order) order
+ by default auto
+
+
+subsection {* Binary infimum and supremum *}
+
+instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
+begin
+
+definition
+ "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
+
+lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
+ unfolding inf_prod_def by simp
+
+lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)"
+ unfolding inf_prod_def by simp
+
+lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
+ unfolding inf_prod_def by simp
+
+instance
+ by default auto
+
+end
+
+instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
+begin
+
+definition
+ "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))"
+
+lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)"
+ unfolding sup_prod_def by simp
+
+lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)"
+ unfolding sup_prod_def by simp
+
+lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
+ unfolding sup_prod_def by simp
+
+instance
+ by default auto
+
+end
+
+instance prod :: (lattice, lattice) lattice ..
+
+instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
+ by default (auto simp add: sup_inf_distrib1)
+
+
+subsection {* Top and bottom elements *}
+
+instantiation prod :: (top, top) top
+begin
+
+definition
+ "top = (top, top)"
+
+lemma fst_top [simp]: "fst top = top"
+ unfolding top_prod_def by simp
+
+lemma snd_top [simp]: "snd top = top"
+ unfolding top_prod_def by simp
+
+lemma Pair_top_top: "(top, top) = top"
+ unfolding top_prod_def by simp
+
+instance
+ by default (auto simp add: top_prod_def)
+
+end
+
+instantiation prod :: (bot, bot) bot
+begin
+
+definition
+ "bot = (bot, bot)"
+
+lemma fst_bot [simp]: "fst bot = bot"
+ unfolding bot_prod_def by simp
+
+lemma snd_bot [simp]: "snd bot = bot"
+ unfolding bot_prod_def by simp
+
+lemma Pair_bot_bot: "(bot, bot) = bot"
+ unfolding bot_prod_def by simp
+
+instance
+ by default (auto simp add: bot_prod_def)
+
+end
+
+instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
+
+instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
+ by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+
+
+subsection {* Complete lattice operations *}
+
+instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
+begin
+
+definition
+ "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+
+definition
+ "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+
+instance
+ by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
+ INF_lower SUP_upper le_INF_iff SUP_le_iff)
+
+end
+
+lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
+ unfolding Sup_prod_def by simp
+
+lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
+ unfolding Sup_prod_def by simp
+
+lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
+ unfolding Inf_prod_def by simp
+
+lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
+ unfolding Inf_prod_def by simp
+
+lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
+ by (simp add: SUP_def fst_Sup image_image)
+
+lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
+ by (simp add: SUP_def snd_Sup image_image)
+
+lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
+ by (simp add: INF_def fst_Inf image_image)
+
+lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
+ by (simp add: INF_def snd_Inf image_image)
+
+lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
+ by (simp add: SUP_def Sup_prod_def image_image)
+
+lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
+ by (simp add: INF_def Inf_prod_def image_image)
+
+
+text {* Alternative formulations for set infima and suprema over the product
+of two complete lattices: *}
+
+lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
+by (auto simp: Inf_prod_def INF_def)
+
+lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
+by (auto simp: Sup_prod_def SUP_def)
+
+lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
+by (auto simp: INF_def Inf_prod_def image_compose)
+
+lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
+by (auto simp: SUP_def Sup_prod_def image_compose)
+
+lemma INF_prod_alt_def:
+ "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
+by (metis fst_INF snd_INF surjective_pairing)
+
+lemma SUP_prod_alt_def:
+ "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
+by (metis fst_SUP snd_SUP surjective_pairing)
+
+
+subsection {* Complete distributive lattices *}
+
+(* Contribution: Alessandro Coglio *)
+
+instance prod ::
+ (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
+proof
+ case goal1 thus ?case
+ by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
+next
+ case goal2 thus ?case
+ by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
+qed
+
+end
+
--- a/src/HOL/Library/Product_ord.thy Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-(* Title: HOL/Library/Product_ord.thy
- Author: Norbert Voelker
-*)
-
-header {* Order on product types *}
-
-theory Product_ord
-imports Main
-begin
-
-instantiation prod :: (ord, ord) ord
-begin
-
-definition
- prod_le_def: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x \<le> snd y"
-
-definition
- prod_less_def: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x \<le> fst y \<and> snd x < snd y"
-
-instance ..
-
-end
-
-lemma [code]:
- "(x1::'a::{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
- "(x1::'a::{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
- unfolding prod_le_def prod_less_def by simp_all
-
-instance prod :: (preorder, preorder) preorder
- by default (auto simp: prod_le_def prod_less_def less_le_not_le intro: order_trans)
-
-instance prod :: (order, order) order
- by default (auto simp add: prod_le_def)
-
-instance prod :: (linorder, linorder) linorder
- by default (auto simp: prod_le_def)
-
-instantiation prod :: (linorder, linorder) distrib_lattice
-begin
-
-definition
- inf_prod_def: "(inf :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
-
-definition
- sup_prod_def: "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
-
-instance
- by default (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
-
-end
-
-instantiation prod :: (bot, bot) bot
-begin
-
-definition
- bot_prod_def: "bot = (bot, bot)"
-
-instance
- by default (auto simp add: bot_prod_def prod_le_def)
-
-end
-
-instantiation prod :: (top, top) top
-begin
-
-definition
- top_prod_def: "top = (top, top)"
-
-instance
- by default (auto simp add: top_prod_def prod_le_def)
-
-end
-
-text {* A stronger version of the definition holds for partial orders. *}
-
-lemma prod_less_eq:
- fixes x y :: "'a::order \<times> 'b::ord"
- shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
- unfolding prod_less_def fst_conv snd_conv le_less by auto
-
-instance prod :: (wellorder, wellorder) wellorder
-proof
- fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
- assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
- show "P z"
- proof (induct z)
- case (Pair a b)
- show "P (a, b)"
- proof (induct a arbitrary: b rule: less_induct)
- case (less a\<^isub>1) note a\<^isub>1 = this
- show "P (a\<^isub>1, b)"
- proof (induct b rule: less_induct)
- case (less b\<^isub>1) note b\<^isub>1 = this
- show "P (a\<^isub>1, b\<^isub>1)"
- proof (rule P)
- fix p assume p: "p < (a\<^isub>1, b\<^isub>1)"
- show "P p"
- proof (cases "fst p < a\<^isub>1")
- case True
- then have "P (fst p, snd p)" by (rule a\<^isub>1)
- then show ?thesis by simp
- next
- case False
- with p have 1: "a\<^isub>1 = fst p" and 2: "snd p < b\<^isub>1"
- by (simp_all add: prod_less_eq)
- from 2 have "P (a\<^isub>1, snd p)" by (rule b\<^isub>1)
- with 1 show ?thesis by simp
- qed
- qed
- qed
- qed
- qed
-qed
-
-end
--- a/src/HOL/Library/RBT_Set.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* Implementation of sets using RBT trees *}
theory RBT_Set
-imports RBT Product_ord
+imports RBT Product_Lexorder
begin
(*
--- a/src/HOL/Lifting.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Lifting.thy Thu Feb 14 17:06:15 2013 +0100
@@ -6,7 +6,7 @@
header {* Lifting package *}
theory Lifting
-imports Plain Equiv_Relations Transfer
+imports Equiv_Relations Transfer
keywords
"print_quotmaps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
--- a/src/HOL/List.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/List.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Presburger Code_Numeral Quotient ATP
+imports Presburger Code_Numeral Quotient ATP
begin
datatype 'a list =
--- a/src/HOL/Main.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Main.thy Thu Feb 14 17:06:15 2013 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Predicate_Compile Nitpick
+imports Predicate_Compile Nitpick Extraction
begin
text {*
@@ -11,4 +11,18 @@
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
+no_notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter>_" [900] 900) and
+ Sup ("\<Squnion>_" [900] 900)
+
+no_syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
end
--- a/src/HOL/Plain.thy Thu Feb 14 16:36:21 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-header {* Plain HOL *}
-
-theory Plain
-imports Datatype FunDef Extraction Metis Num
-begin
-
-text {*
- Plain bootstrap of fundamental HOL tools and packages; does not
- include @{text Hilbert_Choice}.
-*}
-
-no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-no_syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
--- a/src/HOL/Predicate.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Predicate.thy Thu Feb 14 17:06:15 2013 +0100
@@ -8,20 +8,6 @@
imports List
begin
-notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
subsection {* The type of predicate enumerations (a monad) *}
datatype 'a pred = Pred "'a \<Rightarrow> bool"
@@ -729,20 +715,8 @@
by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900) and
bind (infixl "\<guillemotright>=" 70)
-no_syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
--- a/src/HOL/Quotient.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Quotient.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* Definition of Quotient Types *}
theory Quotient
-imports Plain Hilbert_Choice Equiv_Relations Lifting
+imports Hilbert_Choice Equiv_Relations Lifting
keywords
"print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
"quotient_type" :: thy_goal and "/" and
--- a/src/HOL/ROOT Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/ROOT Thu Feb 14 17:06:15 2013 +0100
@@ -26,6 +26,8 @@
Finite_Lattice
Code_Char_chr
Code_Char_ord
+ Product_Lexorder
+ Product_Order
Code_Integer
Efficient_Nat
(* Code_Prolog FIXME cf. 76965c356d2a *)
--- a/src/HOL/Record.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Record.thy Thu Feb 14 17:06:15 2013 +0100
@@ -9,7 +9,7 @@
header {* Extensible records with structural subtyping *}
theory Record
-imports Plain Quickcheck_Narrowing
+imports Quickcheck_Narrowing
keywords "record" :: thy_decl
begin
--- a/src/HOL/Transfer.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Transfer.thy Thu Feb 14 17:06:15 2013 +0100
@@ -5,7 +5,7 @@
header {* Generic theorem transfer using relations *}
theory Transfer
-imports Plain Hilbert_Choice
+imports Hilbert_Choice
begin
subsection {* Relator for function space *}
--- a/src/HOL/Typerep.thy Thu Feb 14 16:36:21 2013 +0100
+++ b/src/HOL/Typerep.thy Thu Feb 14 17:06:15 2013 +0100
@@ -3,7 +3,7 @@
header {* Reflecting Pure types into HOL *}
theory Typerep
-imports Plain String
+imports String
begin
datatype typerep = Typerep String.literal "typerep list"