1.1 --- a/src/HOL/BNF/Basic_BNFs.thy Wed Aug 14 14:05:54 2013 +0200
1.2 +++ b/src/HOL/BNF/Basic_BNFs.thy Fri Aug 16 15:33:24 2013 +0200
1.3 @@ -48,11 +48,6 @@
1.4
1.5 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
1.6
1.7 -definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where
1.8 -"sum_rel \<phi> \<psi> x y =
1.9 - (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
1.10 - | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
1.11 -
1.12 bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
1.13 proof -
1.14 show "sum_map id id = id" by (rule sum_map.id)
1.15 @@ -153,9 +148,6 @@
1.16
1.17 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
1.18
1.19 -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
1.20 -"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)"
1.21 -
1.22 bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. natLeq" [Pair] prod_rel
1.23 proof (unfold prod_set_defs)
1.24 show "map_pair id id = id" by (rule map_pair.id)
2.1 --- a/src/HOL/BNF/Examples/Process.thy Wed Aug 14 14:05:54 2013 +0200
2.2 +++ b/src/HOL/BNF/Examples/Process.thy Fri Aug 16 15:33:24 2013 +0200
2.3 @@ -11,8 +11,6 @@
2.4 imports "../BNF"
2.5 begin
2.6
2.7 -hide_fact (open) Lifting_Product.prod_rel_def
2.8 -
2.9 codatatype 'a process =
2.10 isAction: Action (prefOf: 'a) (contOf: "'a process") |
2.11 isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")
3.1 --- a/src/HOL/BNF/More_BNFs.thy Wed Aug 14 14:05:54 2013 +0200
3.2 +++ b/src/HOL/BNF/More_BNFs.thy Fri Aug 16 15:33:24 2013 +0200
3.3 @@ -68,7 +68,7 @@
3.4 show "option_rel R =
3.5 (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
3.6 Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
3.7 - unfolding option_rel_unfold Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
3.8 + unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
3.9 by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
3.10 split: option.splits)
3.11 qed
4.1 --- a/src/HOL/Library/Code_Target_Nat.thy Wed Aug 14 14:05:54 2013 +0200
4.2 +++ b/src/HOL/Library/Code_Target_Nat.thy Fri Aug 16 15:33:24 2013 +0200
4.3 @@ -123,9 +123,27 @@
4.4 "integer_of_nat (nat k) = max 0 (integer_of_int k)"
4.5 by transfer auto
4.6
4.7 +lemma term_of_nat_code [code]:
4.8 + -- {* Use @{term Code_Numeral.nat_of_integer} in term reconstruction
4.9 + instead of @{term Code_Target_Nat.Nat} such that reconstructed
4.10 + terms can be fed back to the code generator *}
4.11 + "term_of_class.term_of n =
4.12 + Code_Evaluation.App
4.13 + (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'')
4.14 + (typerep.Typerep (STR ''fun'')
4.15 + [typerep.Typerep (STR ''Code_Numeral.integer'') [],
4.16 + typerep.Typerep (STR ''Nat.nat'') []]))
4.17 + (term_of_class.term_of (integer_of_nat n))"
4.18 +by(simp add: term_of_anything)
4.19 +
4.20 +lemma nat_of_integer_code_post [code_post]:
4.21 + "nat_of_integer 0 = 0"
4.22 + "nat_of_integer 1 = 1"
4.23 + "nat_of_integer (numeral k) = numeral k"
4.24 +by(transfer, simp)+
4.25 +
4.26 code_identifier
4.27 code_module Code_Target_Nat \<rightharpoonup>
4.28 (SML) Arith and (OCaml) Arith and (Haskell) Arith
4.29
4.30 end
4.31 -
5.1 --- a/src/HOL/Library/Mapping.thy Wed Aug 14 14:05:54 2013 +0200
5.2 +++ b/src/HOL/Library/Mapping.thy Fri Aug 16 15:33:24 2013 +0200
5.3 @@ -33,7 +33,7 @@
5.4 definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
5.5
5.6 lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None"
5.7 -unfolding fun_rel_def option_rel_unfold equal_None_def by (auto split: option.split)
5.8 +unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
5.9
5.10 lemma dom_transfer:
5.11 assumes [transfer_rule]: "bi_total A"
6.1 --- a/src/HOL/Library/Quotient_Option.thy Wed Aug 14 14:05:54 2013 +0200
6.2 +++ b/src/HOL/Library/Quotient_Option.thy Fri Aug 16 15:33:24 2013 +0200
6.3 @@ -12,11 +12,11 @@
6.4
6.5 lemma option_rel_map1:
6.6 "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
6.7 - by (simp add: option_rel_unfold split: option.split)
6.8 + by (simp add: option_rel_def split: option.split)
6.9
6.10 lemma option_rel_map2:
6.11 "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
6.12 - by (simp add: option_rel_unfold split: option.split)
6.13 + by (simp add: option_rel_def split: option.split)
6.14
6.15 lemma option_map_id [id_simps]:
6.16 "Option.map id = id"
6.17 @@ -24,15 +24,15 @@
6.18
6.19 lemma option_rel_eq [id_simps]:
6.20 "option_rel (op =) = (op =)"
6.21 - by (simp add: option_rel_unfold fun_eq_iff split: option.split)
6.22 + by (simp add: option_rel_def fun_eq_iff split: option.split)
6.23
6.24 lemma option_symp:
6.25 "symp R \<Longrightarrow> symp (option_rel R)"
6.26 - unfolding symp_def split_option_all option_rel.simps by fast
6.27 + unfolding symp_def split_option_all option_rel_simps by fast
6.28
6.29 lemma option_transp:
6.30 "transp R \<Longrightarrow> transp (option_rel R)"
6.31 - unfolding transp_def split_option_all option_rel.simps by fast
6.32 + unfolding transp_def split_option_all option_rel_simps by fast
6.33
6.34 lemma option_equivp [quot_equiv]:
6.35 "equivp R \<Longrightarrow> equivp (option_rel R)"
6.36 @@ -44,7 +44,7 @@
6.37 apply (rule Quotient3I)
6.38 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])
6.39 using Quotient3_rel [OF assms]
6.40 - apply (simp add: option_rel_unfold split: option.split)
6.41 + apply (simp add: option_rel_def split: option.split)
6.42 done
6.43
6.44 declare [[mapQ3 option = (option_rel, option_quotient)]]
7.1 --- a/src/HOL/Library/Quotient_Sum.thy Wed Aug 14 14:05:54 2013 +0200
7.2 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Aug 16 15:33:24 2013 +0200
7.3 @@ -12,11 +12,11 @@
7.4
7.5 lemma sum_rel_map1:
7.6 "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"
7.7 - by (simp add: sum_rel_unfold split: sum.split)
7.8 + by (simp add: sum_rel_def split: sum.split)
7.9
7.10 lemma sum_rel_map2:
7.11 "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"
7.12 - by (simp add: sum_rel_unfold split: sum.split)
7.13 + by (simp add: sum_rel_def split: sum.split)
7.14
7.15 lemma sum_map_id [id_simps]:
7.16 "sum_map id id = id"
7.17 @@ -24,15 +24,15 @@
7.18
7.19 lemma sum_rel_eq [id_simps]:
7.20 "sum_rel (op =) (op =) = (op =)"
7.21 - by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
7.22 + by (simp add: sum_rel_def fun_eq_iff split: sum.split)
7.23
7.24 lemma sum_symp:
7.25 "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
7.26 - unfolding symp_def split_sum_all sum_rel.simps by fast
7.27 + unfolding symp_def split_sum_all sum_rel_simps by fast
7.28
7.29 lemma sum_transp:
7.30 "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
7.31 - unfolding transp_def split_sum_all sum_rel.simps by fast
7.32 + unfolding transp_def split_sum_all sum_rel_simps by fast
7.33
7.34 lemma sum_equivp [quot_equiv]:
7.35 "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
7.36 @@ -46,7 +46,7 @@
7.37 apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
7.38 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
7.39 using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
7.40 - apply (simp add: sum_rel_unfold comp_def split: sum.split)
7.41 + apply (simp add: sum_rel_def comp_def split: sum.split)
7.42 done
7.43
7.44 declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
8.1 --- a/src/HOL/Lifting_Option.thy Wed Aug 14 14:05:54 2013 +0200
8.2 +++ b/src/HOL/Lifting_Option.thy Fri Aug 16 15:33:24 2013 +0200
8.3 @@ -5,52 +5,45 @@
8.4 header {* Setup for Lifting/Transfer for the option type *}
8.5
8.6 theory Lifting_Option
8.7 -imports Lifting FunDef
8.8 +imports Lifting
8.9 begin
8.10
8.11 subsection {* Relator and predicator properties *}
8.12
8.13 -fun
8.14 +definition
8.15 option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
8.16 where
8.17 - "option_rel R None None = True"
8.18 -| "option_rel R (Some x) None = False"
8.19 -| "option_rel R None (Some x) = False"
8.20 -| "option_rel R (Some x) (Some y) = R x y"
8.21 -
8.22 -lemma option_rel_unfold:
8.23 "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
8.24 | (Some x, Some y) \<Rightarrow> R x y
8.25 | _ \<Rightarrow> False)"
8.26 - by (cases x) (cases y, simp_all)+
8.27
8.28 -fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
8.29 -where
8.30 - "option_pred R None = True"
8.31 -| "option_pred R (Some x) = R x"
8.32 +lemma option_rel_simps[simp]:
8.33 + "option_rel R None None = True"
8.34 + "option_rel R (Some x) None = False"
8.35 + "option_rel R None (Some y) = False"
8.36 + "option_rel R (Some x) (Some y) = R x y"
8.37 + unfolding option_rel_def by simp_all
8.38
8.39 -lemma option_pred_unfold:
8.40 - "option_pred P x = (case x of None \<Rightarrow> True
8.41 - | Some x \<Rightarrow> P x)"
8.42 -by (cases x) simp_all
8.43 +abbreviation (input) option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool" where
8.44 + "option_pred \<equiv> option_case True"
8.45
8.46 lemma option_rel_eq [relator_eq]:
8.47 "option_rel (op =) = (op =)"
8.48 - by (simp add: option_rel_unfold fun_eq_iff split: option.split)
8.49 + by (simp add: option_rel_def fun_eq_iff split: option.split)
8.50
8.51 lemma option_rel_mono[relator_mono]:
8.52 assumes "A \<le> B"
8.53 shows "(option_rel A) \<le> (option_rel B)"
8.54 -using assms by (auto simp: option_rel_unfold split: option.splits)
8.55 +using assms by (auto simp: option_rel_def split: option.splits)
8.56
8.57 lemma option_rel_OO[relator_distr]:
8.58 "(option_rel A) OO (option_rel B) = option_rel (A OO B)"
8.59 -by (rule ext)+ (auto simp: option_rel_unfold OO_def split: option.split)
8.60 +by (rule ext)+ (auto simp: option_rel_def OO_def split: option.split)
8.61
8.62 lemma Domainp_option[relator_domain]:
8.63 assumes "Domainp A = P"
8.64 shows "Domainp (option_rel A) = (option_pred P)"
8.65 -using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
8.66 +using assms unfolding Domainp_iff[abs_def] option_rel_def[abs_def]
8.67 by (auto iff: fun_eq_iff split: option.split)
8.68
8.69 lemma reflp_option_rel[reflexivity_rule]:
8.70 @@ -91,7 +84,7 @@
8.71 assumes "Quotient R Abs Rep T"
8.72 shows "Quotient (option_rel R) (Option.map Abs)
8.73 (Option.map Rep) (option_rel T)"
8.74 - using assms unfolding Quotient_alt_def option_rel_unfold
8.75 + using assms unfolding Quotient_alt_def option_rel_def
8.76 by (simp split: option.split)
8.77
8.78 subsection {* Transfer rules for the Transfer package *}
9.1 --- a/src/HOL/Lifting_Sum.thy Wed Aug 14 14:05:54 2013 +0200
9.2 +++ b/src/HOL/Lifting_Sum.thy Fri Aug 16 15:33:24 2013 +0200
9.3 @@ -5,59 +5,52 @@
9.4 header {* Setup for Lifting/Transfer for the sum type *}
9.5
9.6 theory Lifting_Sum
9.7 -imports Lifting FunDef
9.8 +imports Lifting
9.9 begin
9.10
9.11 subsection {* Relator and predicator properties *}
9.12
9.13 -fun
9.14 - sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
9.15 +definition
9.16 + sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
9.17 where
9.18 + "sum_rel R1 R2 x y =
9.19 + (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
9.20 + | (Inr x, Inr y) \<Rightarrow> R2 x y
9.21 + | _ \<Rightarrow> False)"
9.22 +
9.23 +lemma sum_rel_simps[simp]:
9.24 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
9.25 -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
9.26 -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
9.27 -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
9.28 + "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
9.29 + "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
9.30 + "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
9.31 + unfolding sum_rel_def by simp_all
9.32
9.33 -lemma sum_rel_unfold:
9.34 - "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
9.35 - | (Inr x, Inr y) \<Rightarrow> R2 x y
9.36 - | _ \<Rightarrow> False)"
9.37 - by (cases x) (cases y, simp_all)+
9.38 -
9.39 -fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
9.40 -where
9.41 - "sum_pred P1 P2 (Inl a) = P1 a"
9.42 -| "sum_pred P1 P2 (Inr a) = P2 a"
9.43 -
9.44 -lemma sum_pred_unfold:
9.45 - "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
9.46 - | Inr x \<Rightarrow> P2 x)"
9.47 -by (cases x) simp_all
9.48 +abbreviation (input) "sum_pred \<equiv> sum_case"
9.49
9.50 lemma sum_rel_eq [relator_eq]:
9.51 "sum_rel (op =) (op =) = (op =)"
9.52 - by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
9.53 + by (simp add: sum_rel_def fun_eq_iff split: sum.split)
9.54
9.55 lemma sum_rel_mono[relator_mono]:
9.56 assumes "A \<le> C"
9.57 assumes "B \<le> D"
9.58 shows "(sum_rel A B) \<le> (sum_rel C D)"
9.59 -using assms by (auto simp: sum_rel_unfold split: sum.splits)
9.60 +using assms by (auto simp: sum_rel_def split: sum.splits)
9.61
9.62 lemma sum_rel_OO[relator_distr]:
9.63 "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
9.64 -by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
9.65 +by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
9.66
9.67 lemma Domainp_sum[relator_domain]:
9.68 assumes "Domainp R1 = P1"
9.69 assumes "Domainp R2 = P2"
9.70 shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
9.71 using assms
9.72 -by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
9.73 +by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
9.74
9.75 lemma reflp_sum_rel[reflexivity_rule]:
9.76 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
9.77 - unfolding reflp_def split_sum_all sum_rel.simps by fast
9.78 + unfolding reflp_def split_sum_all sum_rel_simps by fast
9.79
9.80 lemma left_total_sum_rel[reflexivity_rule]:
9.81 "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
9.82 @@ -85,7 +78,7 @@
9.83
9.84 lemma sum_invariant_commute [invariant_commute]:
9.85 "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
9.86 - by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
9.87 + by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split)
9.88
9.89 subsection {* Quotient theorem for the Lifting package *}
9.90
9.91 @@ -111,7 +104,7 @@
9.92
9.93 lemma sum_case_transfer [transfer_rule]:
9.94 "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case"
9.95 - unfolding fun_rel_def sum_rel_unfold by (simp split: sum.split)
9.96 + unfolding fun_rel_def sum_rel_def by (simp split: sum.split)
9.97
9.98 end
9.99