# HG changeset patch # User blanchet # Date 1376660004 -7200 # Node ID 1b18e3ce776fd2e817fd4fbc86a2d6e50f02c25f # Parent 8444e1b8e7a384835774161d75816fe4dfb3532e# Parent 1774d569b60439e9be9340fbd2c60ca3481cfcb7 merge diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/BNF/Basic_BNFs.thy --- 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 \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a + 'c \ 'b + 'd \ bool" where -"sum_rel \ \ x y = - (case x of Inl a1 \ (case y of Inl a2 \ \ a1 a2 | Inr _ \ False) - | Inr b1 \ (case y of Inl _ \ False | Inr b2 \ \ b1 b2))" - bnf sum_map [setl, setr] "\_::'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 \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" where -"prod_rel \ \ p1 p2 = (case p1 of (a1, b1) \ case p2 of (a2, b2) \ \ a1 a2 \ \ b1 b2)" - bnf map_pair [fsts, snds] "\_::'a \ 'b. natLeq" [Pair] prod_rel proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/BNF/Examples/Process.thy --- 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") diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/BNF/More_BNFs.thy --- 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 \ Collect (split R)} (Option.map fst))\\ OO Grp {x. Option.set x \ 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 diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Library/Code_Target_Nat.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end - diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Library/Mapping.thy --- 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 \ bool" where "equal_None x \ 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" diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Library/Quotient_Option.thy --- 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 \ option_rel (\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) \ option_rel (\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 \ 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 \ 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 \ 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)]] diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Library/Quotient_Sum.thy --- 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 \ sum_rel (\x. R1 (f1 x)) (\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) \ sum_rel (\x y. R1 x (f1 y)) (\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 \ symp R2 \ 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 \ transp R2 \ 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 \ equivp R2 \ 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)]] diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Lifting_Option.thy --- 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 \ 'b \ bool) \ 'a option \ 'b option \ 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) \ True | (Some x, Some y) \ R x y | _ \ False)" - by (cases x) (cases y, simp_all)+ -fun option_pred :: "('a \ bool) \ 'a option \ 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 \ True - | Some x \ P x)" -by (cases x) simp_all +abbreviation (input) option_pred :: "('a \ bool) \ 'a option \ bool" where + "option_pred \ 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 \ B" shows "(option_rel A) \ (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 *} diff -r 8444e1b8e7a3 -r 1b18e3ce776f src/HOL/Lifting_Sum.thy --- 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 \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ bool" +definition + sum_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ 'a + 'b \ 'c + 'd \ 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) \ R1 x y + | (Inr x, Inr y) \ R2 x y + | _ \ False)" -lemma sum_rel_unfold: - "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y - | (Inr x, Inr y) \ R2 x y - | _ \ 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 \ bool) \ ('b \ bool) \ 'a + 'b \ 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 \ P1 x - | Inr x \ P2 x)" -by (cases x) simp_all +abbreviation (input) "sum_pred \ 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 \ C" assumes "B \ D" shows "(sum_rel A B) \ (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 \ reflp R2 \ 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 \ left_total R2 \ 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