--- a/src/HOL/BNF/Basic_BNFs.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy Fri Aug 16 15:33:24 2013 +0200
@@ -48,11 +48,6 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
-"sum_rel \<phi> \<psi> x y =
- (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
- | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
-
bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
proof -
show "sum_map id id = id" by (rule sum_map.id)
@@ -153,9 +148,6 @@
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
-definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
-"prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
-
bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" [Pair] prod_rel
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
--- a/src/HOL/BNF/Examples/Process.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy Fri Aug 16 15:33:24 2013 +0200
@@ -11,8 +11,6 @@
imports "../BNF"
begin
-hide_fact (open) Lifting_Product.prod_rel_def
-
codatatype 'a process =
isAction: Action (prefOf: 'a) (contOf: "'a process") |
isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")
--- a/src/HOL/BNF/More_BNFs.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Fri Aug 16 15:33:24 2013 +0200
@@ -68,7 +68,7 @@
show "option_rel R =
(Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
- unfolding option_rel_unfold Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
+ unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
split: option.splits)
qed
--- a/src/HOL/Library/Code_Target_Nat.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Fri Aug 16 15:33:24 2013 +0200
@@ -123,9 +123,27 @@
"integer_of_nat (nat k) = max 0 (integer_of_int k)"
by transfer auto
+lemma term_of_nat_code [code]:
+ -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
+ instead of @{term Code_Target_Nat.Nat} such that reconstructed
+ terms can be fed back to the code generator *}
+ "term_of_class.term_of n =
+ Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
+ (typerep.Typerep (STR ''fun'')
+ [typerep.Typerep (STR ''Code_Numeral.integer'') [],
+ typerep.Typerep (STR ''Nat.nat'') []]))
+ (term_of_class.term_of (integer_of_nat n))"
+by(simp add: term_of_anything)
+
+lemma nat_of_integer_code_post [code_post]:
+ "nat_of_integer 0 = 0"
+ "nat_of_integer 1 = 1"
+ "nat_of_integer (numeral k) = numeral k"
+by(transfer, simp)+
+
code_identifier
code_module Code_Target_Nat \<rightharpoonup>
(SML) Arith and (OCaml) Arith and (Haskell) Arith
end
-
--- a/src/HOL/Library/Mapping.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Library/Mapping.thy Fri Aug 16 15:33:24 2013 +0200
@@ -33,7 +33,7 @@
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None"
-unfolding fun_rel_def option_rel_unfold equal_None_def by (auto split: option.split)
+unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
lemma dom_transfer:
assumes [transfer_rule]: "bi_total A"
--- a/src/HOL/Library/Quotient_Option.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Fri Aug 16 15:33:24 2013 +0200
@@ -12,11 +12,11 @@
lemma option_rel_map1:
"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
- by (simp add: option_rel_unfold split: option.split)
+ by (simp add: option_rel_def split: option.split)
lemma option_rel_map2:
"option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
- by (simp add: option_rel_unfold split: option.split)
+ by (simp add: option_rel_def split: option.split)
lemma option_map_id [id_simps]:
"Option.map id = id"
@@ -24,15 +24,15 @@
lemma option_rel_eq [id_simps]:
"option_rel (op =) = (op =)"
- by (simp add: option_rel_unfold fun_eq_iff split: option.split)
+ by (simp add: option_rel_def fun_eq_iff split: option.split)
lemma option_symp:
"symp R \<Longrightarrow> symp (option_rel R)"
- unfolding symp_def split_option_all option_rel.simps by fast
+ unfolding symp_def split_option_all option_rel_simps by fast
lemma option_transp:
"transp R \<Longrightarrow> transp (option_rel R)"
- unfolding transp_def split_option_all option_rel.simps by fast
+ unfolding transp_def split_option_all option_rel_simps by fast
lemma option_equivp [quot_equiv]:
"equivp R \<Longrightarrow> equivp (option_rel R)"
@@ -44,7 +44,7 @@
apply (rule Quotient3I)
apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
using Quotient3_rel [OF assms]
- apply (simp add: option_rel_unfold split: option.split)
+ apply (simp add: option_rel_def split: option.split)
done
declare [[mapQ3 option = (option_rel, option_quotient)]]
--- a/src/HOL/Library/Quotient_Sum.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Aug 16 15:33:24 2013 +0200
@@ -12,11 +12,11 @@
lemma sum_rel_map1:
"sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
- by (simp add: sum_rel_unfold split: sum.split)
+ by (simp add: sum_rel_def split: sum.split)
lemma sum_rel_map2:
"sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
- by (simp add: sum_rel_unfold split: sum.split)
+ by (simp add: sum_rel_def split: sum.split)
lemma sum_map_id [id_simps]:
"sum_map id id = id"
@@ -24,15 +24,15 @@
lemma sum_rel_eq [id_simps]:
"sum_rel (op =) (op =) = (op =)"
- by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
+ by (simp add: sum_rel_def fun_eq_iff split: sum.split)
lemma sum_symp:
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
- unfolding symp_def split_sum_all sum_rel.simps by fast
+ unfolding symp_def split_sum_all sum_rel_simps by fast
lemma sum_transp:
"transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
- unfolding transp_def split_sum_all sum_rel.simps by fast
+ unfolding transp_def split_sum_all sum_rel_simps by fast
lemma sum_equivp [quot_equiv]:
"equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
@@ -46,7 +46,7 @@
apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
- apply (simp add: sum_rel_unfold comp_def split: sum.split)
+ apply (simp add: sum_rel_def comp_def split: sum.split)
done
declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
--- a/src/HOL/Lifting_Option.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Lifting_Option.thy Fri Aug 16 15:33:24 2013 +0200
@@ -5,52 +5,45 @@
header {* Setup for Lifting/Transfer for the option type *}
theory Lifting_Option
-imports Lifting FunDef
+imports Lifting
begin
subsection {* Relator and predicator properties *}
-fun
+definition
option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
where
- "option_rel R None None = True"
-| "option_rel R (Some x) None = False"
-| "option_rel R None (Some x) = False"
-| "option_rel R (Some x) (Some y) = R x y"
-
-lemma option_rel_unfold:
"option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
| (Some x, Some y) \<Rightarrow> R x y
| _ \<Rightarrow> False)"
- by (cases x) (cases y, simp_all)+
-fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
-where
- "option_pred R None = True"
-| "option_pred R (Some x) = R x"
+lemma option_rel_simps[simp]:
+ "option_rel R None None = True"
+ "option_rel R (Some x) None = False"
+ "option_rel R None (Some y) = False"
+ "option_rel R (Some x) (Some y) = R x y"
+ unfolding option_rel_def by simp_all
-lemma option_pred_unfold:
- "option_pred P x = (case x of None \<Rightarrow> True
- | Some x \<Rightarrow> P x)"
-by (cases x) simp_all
+abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
+ "option_pred \<equiv> option_case True"
lemma option_rel_eq [relator_eq]:
"option_rel (op =) = (op =)"
- by (simp add: option_rel_unfold fun_eq_iff split: option.split)
+ by (simp add: option_rel_def fun_eq_iff split: option.split)
lemma option_rel_mono[relator_mono]:
assumes "A \<le> B"
shows "(option_rel A) \<le> (option_rel B)"
-using assms by (auto simp: option_rel_unfold split: option.splits)
+using assms by (auto simp: option_rel_def split: option.splits)
lemma option_rel_OO[relator_distr]:
"(option_rel A) OO (option_rel B) = option_rel (A OO B)"
-by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
+by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split)
lemma Domainp_option[relator_domain]:
assumes "Domainp A = P"
shows "Domainp (option_rel A) = (option_pred P)"
-using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
+using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def]
by (auto iff: fun_eq_iff split: option.split)
lemma reflp_option_rel[reflexivity_rule]:
@@ -91,7 +84,7 @@
assumes "Quotient R Abs Rep T"
shows "Quotient (option_rel R) (Option.map Abs)
(Option.map Rep) (option_rel T)"
- using assms unfolding Quotient_alt_def option_rel_unfold
+ using assms unfolding Quotient_alt_def option_rel_def
by (simp split: option.split)
subsection {* Transfer rules for the Transfer package *}
--- a/src/HOL/Lifting_Sum.thy Wed Aug 14 14:05:54 2013 +0200
+++ b/src/HOL/Lifting_Sum.thy Fri Aug 16 15:33:24 2013 +0200
@@ -5,59 +5,52 @@
header {* Setup for Lifting/Transfer for the sum type *}
theory Lifting_Sum
-imports Lifting FunDef
+imports Lifting
begin
subsection {* Relator and predicator properties *}
-fun
- sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+definition
+ sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
where
- "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
-| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
-| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
-| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+ "sum_rel R1 R2 x y =
+ (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
-lemma sum_rel_unfold:
- "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
- | (Inr x, Inr y) \<Rightarrow> R2 x y
- | _ \<Rightarrow> False)"
- by (cases x) (cases y, simp_all)+
+lemma sum_rel_simps[simp]:
+ "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+ "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
+ "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
+ "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+ unfolding sum_rel_def by simp_all
-fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
-where
- "sum_pred P1 P2 (Inl a) = P1 a"
-| "sum_pred P1 P2 (Inr a) = P2 a"
-
-lemma sum_pred_unfold:
- "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
- | Inr x \<Rightarrow> P2 x)"
-by (cases x) simp_all
+abbreviation (input) "sum_pred \<equiv> sum_case"
lemma sum_rel_eq [relator_eq]:
"sum_rel (op =) (op =) = (op =)"
- by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
+ by (simp add: sum_rel_def fun_eq_iff split: sum.split)
lemma sum_rel_mono[relator_mono]:
assumes "A \<le> C"
assumes "B \<le> D"
shows "(sum_rel A B) \<le> (sum_rel C D)"
-using assms by (auto simp: sum_rel_unfold split: sum.splits)
+using assms by (auto simp: sum_rel_def split: sum.splits)
lemma sum_rel_OO[relator_distr]:
"(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
-by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
+by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
lemma Domainp_sum[relator_domain]:
assumes "Domainp R1 = P1"
assumes "Domainp R2 = P2"
shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
using assms
-by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
+by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
lemma reflp_sum_rel[reflexivity_rule]:
"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
- unfolding reflp_def split_sum_all sum_rel.simps by fast
+ unfolding reflp_def split_sum_all sum_rel_simps by fast
lemma left_total_sum_rel[reflexivity_rule]:
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
@@ -85,7 +78,7 @@
lemma sum_invariant_commute [invariant_commute]:
"sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
- by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
+ by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split)
subsection {* Quotient theorem for the Lifting package *}
@@ -111,7 +104,7 @@
lemma sum_case_transfer [transfer_rule]:
"((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
- unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
+ unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
end