# HG changeset patch # User wenzelm # Date 1259921940 -3600 # Node ID e4890d7bd9f8bba03ad1302c766f7ce12a986ae8 # Parent dbc1a5b94449334d7be9cf02df76df604fb2d82e# Parent 99b52900aec0656d06472b9c5263400fd961a633 merged diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/GCD.thy Fri Dec 04 11:19:00 2009 +0100 @@ -779,14 +779,6 @@ apply auto done -lemma coprime_divprod_nat: "(d::nat) dvd a * b \ coprime d a \ d dvd b" - using coprime_dvd_mult_iff_nat[of d a b] - by (auto simp add: mult_commute) - -lemma coprime_divprod_int: "(d::int) dvd a * b \ coprime d a \ d dvd b" - using coprime_dvd_mult_iff_int[of d a b] - by (auto simp add: mult_commute) - lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" proof- diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Inductive.thy Fri Dec 04 11:19:00 2009 +0100 @@ -262,18 +262,13 @@ theorems basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj Collect_mono in_mono vimage_mono - imp_conv_disj not_not de_Morgan_disj de_Morgan_conj - not_all not_ex - Ball_def Bex_def - induct_rulify_fallback use "Tools/inductive.ML" setup Inductive.setup theorems [mono] = imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj - imp_conv_disj not_not de_Morgan_disj de_Morgan_conj - not_all not_ex + imp_mono not_mono Ball_def Bex_def induct_rulify_fallback diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 04 11:19:00 2009 +0100 @@ -369,6 +369,7 @@ Library/Sum_Of_Squares/sos_wrapper.ML \ Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \ Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy \ + Library/Crude_Executable_Set.thy \ Library/Infinite_Set.thy Library/FuncSet.thy \ Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \ Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \ @@ -381,9 +382,9 @@ Library/Order_Relation.thy Library/Nested_Environment.thy \ Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \ Library/Library/document/root.tex Library/Library/document/root.bib \ - Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ - Library/Product_ord.thy Library/Char_nat.thy \ - Library/Char_ord.thy Library/Option_ord.thy \ + Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \ + Library/Product_ord.thy Library/Char_nat.thy \ + Library/Char_ord.thy Library/Option_ord.thy \ Library/Sublist_Order.thy Library/List_lexord.thy \ Library/Coinductive_List.thy Library/AssocList.thy \ Library/Formal_Power_Series.thy Library/Binomial.thy \ diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Library/Crude_Executable_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Crude_Executable_Set.thy Fri Dec 04 11:19:00 2009 +0100 @@ -0,0 +1,259 @@ +(* Title: HOL/Library/Crude_Executable_Set.thy + Author: Florian Haftmann, TU Muenchen +*) + +header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} + +theory Crude_Executable_Set +imports List_Set +begin + +declare mem_def [code del] +declare Collect_def [code del] +declare insert_code [code del] +declare vimage_code [code del] + +subsection {* Set representation *} + +setup {* + Code.add_type_cmd "set" +*} + +definition Set :: "'a list \ 'a set" where + [simp]: "Set = set" + +definition Coset :: "'a list \ 'a set" where + [simp]: "Coset xs = - set xs" + +setup {* + Code.add_signature_cmd ("Set", "'a list \ 'a set") + #> Code.add_signature_cmd ("Coset", "'a list \ 'a set") + #> Code.add_signature_cmd ("set", "'a list \ 'a set") + #> Code.add_signature_cmd ("op \", "'a \ 'a set \ bool") +*} + +code_datatype Set Coset + + +subsection {* Basic operations *} + +lemma [code]: + "set xs = Set (remdups xs)" + by simp + +lemma [code]: + "x \ Set xs \ member x xs" + "x \ Coset xs \ \ member x xs" + by (simp_all add: mem_iff) + +definition is_empty :: "'a set \ bool" where + [simp]: "is_empty A \ A = {}" + +lemma [code_inline]: + "A = {} \ is_empty A" + by simp + +definition empty :: "'a set" where + [simp]: "empty = {}" + +lemma [code_inline]: + "{} = empty" + by simp + +setup {* + Code.add_signature_cmd ("is_empty", "'a set \ bool") + #> Code.add_signature_cmd ("empty", "'a set") + #> Code.add_signature_cmd ("insert", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("List_Set.remove", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("image", "('a \ 'b) \ 'a set \ 'b set") + #> Code.add_signature_cmd ("List_Set.project", "('a \ bool) \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Ball", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("Bex", "'a set \ ('a \ bool) \ bool") + #> Code.add_signature_cmd ("card", "'a set \ nat") +*} + +lemma is_empty_Set [code]: + "is_empty (Set xs) \ null xs" + by (simp add: empty_null) + +lemma empty_Set [code]: + "empty = Set []" + by simp + +lemma insert_Set [code]: + "insert x (Set xs) = Set (List_Set.insert x xs)" + "insert x (Coset xs) = Coset (remove_all x xs)" + by (simp_all add: insert_set insert_set_compl) + +lemma remove_Set [code]: + "remove x (Set xs) = Set (remove_all x xs)" + "remove x (Coset xs) = Coset (List_Set.insert x xs)" + by (simp_all add:remove_set remove_set_compl) + +lemma image_Set [code]: + "image f (Set xs) = Set (remdups (map f xs))" + by simp + +lemma project_Set [code]: + "project P (Set xs) = Set (filter P xs)" + by (simp add: project_set) + +lemma Ball_Set [code]: + "Ball (Set xs) P \ list_all P xs" + by (simp add: ball_set) + +lemma Bex_Set [code]: + "Bex (Set xs) P \ list_ex P xs" + by (simp add: bex_set) + +lemma card_Set [code]: + "card (Set xs) = length (remdups xs)" +proof - + have "card (set (remdups xs)) = length (remdups xs)" + by (rule distinct_card) simp + then show ?thesis by simp +qed + + +subsection {* Derived operations *} + +definition set_eq :: "'a set \ 'a set \ bool" where + [simp]: "set_eq = op =" + +lemma [code_inline]: + "op = = set_eq" + by simp + +definition subset_eq :: "'a set \ 'a set \ bool" where + [simp]: "subset_eq = op \" + +lemma [code_inline]: + "op \ = subset_eq" + by simp + +definition subset :: "'a set \ 'a set \ bool" where + [simp]: "subset = op \" + +lemma [code_inline]: + "op \ = subset" + by simp + +setup {* + Code.add_signature_cmd ("set_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset_eq", "'a set \ 'a set \ bool") + #> Code.add_signature_cmd ("subset", "'a set \ 'a set \ bool") +*} + +lemma set_eq_subset_eq [code]: + "set_eq A B \ subset_eq A B \ subset_eq B A" + by auto + +lemma subset_eq_forall [code]: + "subset_eq A B \ (\x\A. x \ B)" + by (simp add: subset_eq) + +lemma subset_subset_eq [code]: + "subset A B \ subset_eq A B \ \ subset_eq B A" + by (simp add: subset) + + +subsection {* Functorial operations *} + +definition inter :: "'a set \ 'a set \ 'a set" where + [simp]: "inter = op \" + +lemma [code_inline]: + "op \ = inter" + by simp + +definition subtract :: "'a set \ 'a set \ 'a set" where + [simp]: "subtract A B = B - A" + +lemma [code_inline]: + "B - A = subtract A B" + by simp + +definition union :: "'a set \ 'a set \ 'a set" where + [simp]: "union = op \" + +lemma [code_inline]: + "op \ = union" + by simp + +definition Inf :: "'a::complete_lattice set \ 'a" where + [simp]: "Inf = Complete_Lattice.Inf" + +lemma [code_inline]: + "Complete_Lattice.Inf = Inf" + by simp + +definition Sup :: "'a::complete_lattice set \ 'a" where + [simp]: "Sup = Complete_Lattice.Sup" + +lemma [code_inline]: + "Complete_Lattice.Sup = Sup" + by simp + +definition Inter :: "'a set set \ 'a set" where + [simp]: "Inter = Inf" + +lemma [code_inline]: + "Inf = Inter" + by simp + +definition Union :: "'a set set \ 'a set" where + [simp]: "Union = Sup" + +lemma [code_inline]: + "Sup = Union" + by simp + +setup {* + Code.add_signature_cmd ("inter", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("subtract", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("union", "'a set \ 'a set \ 'a set") + #> Code.add_signature_cmd ("Inf", "'a set \ 'a") + #> Code.add_signature_cmd ("Sup", "'a set \ 'a") + #> Code.add_signature_cmd ("Inter", "'a set set \ 'a set") + #> Code.add_signature_cmd ("Union", "'a set set \ 'a set") +*} + +lemma inter_project [code]: + "inter A (Set xs) = Set (List.filter (\x. x \ A) xs)" + "inter A (Coset xs) = foldl (\A x. remove x A) A xs" + by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) + +lemma subtract_remove [code]: + "subtract (Set xs) A = foldl (\A x. remove x A) A xs" + "subtract (Coset xs) A = Set (List.filter (\x. x \ A) xs)" + by (auto simp add: minus_set) + +lemma union_insert [code]: + "union (Set xs) A = foldl (\A x. insert x A) A xs" + "union (Coset xs) A = Coset (List.filter (\x. x \ A) xs)" + by (auto simp add: union_set) + +lemma Inf_inf [code]: + "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" + "Inf (Coset []) = (bot :: 'a::complete_lattice)" + by (simp_all add: Inf_Univ bot_def [symmetric] Inf_set_fold) + +lemma Sup_sup [code]: + "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" + "Sup (Coset []) = (top :: 'a::complete_lattice)" + by (simp_all add: Sup_Univ top_def [symmetric] Sup_set_fold) + +lemma Inter_inter [code]: + "Inter (Set xs) = foldl inter (Coset []) xs" + "Inter (Coset []) = empty" + unfolding Inter_def Inf_inf by simp_all + +lemma Union_union [code]: + "Union (Set xs) = foldl union empty xs" + "Union (Coset []) = Coset []" + unfolding Union_def Sup_sup by simp_all + +hide (open) const is_empty empty remove + set_eq subset_eq subset inter union subtract Inf Sup Inter Union + +end diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Library/Fset.thy Fri Dec 04 11:19:00 2009 +0100 @@ -210,7 +210,7 @@ member (foldl (\B A. Fset (member B \ A)) (Coset []) (List.map member As))" by (rule foldl_apply_inv) simp then show "Inter (Set As) = foldl inter (Coset []) As" - by (simp add: Inter_set image_set inter inter_def_raw foldl_map) + by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map) show "Inter (Coset []) = empty" by simp qed @@ -229,7 +229,7 @@ member (foldl (\B A. Fset (member B \ A)) empty (List.map member As))" by (rule foldl_apply_inv) simp then show "Union (Set As) = foldl union empty As" - by (simp add: Union_set image_set union_def_raw foldl_map) + by (simp add: Sup_set_fold image_set union_def_raw foldl_map) show "Union (Coset []) = Coset []" by simp qed diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Library/Library.thy Fri Dec 04 11:19:00 2009 +0100 @@ -14,6 +14,7 @@ Continuity ContNotDenum Countable + Crude_Executable_Set Diagonalize Efficient_Nat Enum diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Library/List_Set.thy --- a/src/HOL/Library/List_Set.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Library/List_Set.thy Fri Dec 04 11:19:00 2009 +0100 @@ -85,6 +85,50 @@ "project P (set xs) = set (filter P xs)" by (auto simp add: project_def) +text {* FIXME move the following to @{text Finite_Set.thy} *} + +lemma fun_left_comm_idem_inf: + "fun_left_comm_idem inf" +proof +qed (auto simp add: inf_left_commute) + +lemma fun_left_comm_idem_sup: + "fun_left_comm_idem sup" +proof +qed (auto simp add: sup_left_commute) + +lemma inf_Inf_fold_inf: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "inf B (Inf A) = fold inf B A" +proof - + interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) + from `finite A` show ?thesis by (induct A arbitrary: B) + (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm) +qed + +lemma sup_Sup_fold_sup: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "sup B (Sup A) = fold sup B A" +proof - + interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) + from `finite A` show ?thesis by (induct A arbitrary: B) + (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm) +qed + +lemma Inf_fold_inf: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "Inf A = fold inf top A" + using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2) + +lemma Sup_fold_sup: + fixes A :: "'a::complete_lattice set" + assumes "finite A" + shows "Sup A = fold sup bot A" + using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2) + subsection {* Functorial set operations *} @@ -105,41 +149,13 @@ by (simp add: minus_fold_remove [of _ A] fold_set) qed -lemma Inter_set: - "Inter (set As) = foldl (op \) UNIV As" -proof - - have "fold (op \) UNIV (set As) = foldl (\y x. x \ y) UNIV As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: Inter_fold_inter finite_set Int_commute) -qed - -lemma Union_set: - "Union (set As) = foldl (op \) {} As" -proof - - have "fold (op \) {} (set As) = foldl (\y x. x \ y) {} As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: Union_fold_union finite_set Un_commute) -qed +lemma INFI_set_fold: -- "FIXME move to List.thy" + "INFI (set xs) f = foldl (\y x. inf (f x) y) top xs" + unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute) -lemma INTER_set: - "INTER (set As) f = foldl (\B A. f A \ B) UNIV As" -proof - - have "fold (\A. op \ (f A)) UNIV (set As) = foldl (\B A. f A \ B) UNIV As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: INTER_fold_inter finite_set) -qed - -lemma UNION_set: - "UNION (set As) f = foldl (\B A. f A \ B) {} As" -proof - - have "fold (\A. op \ (f A)) {} (set As) = foldl (\B A. f A \ B) {} As" - by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) - then show ?thesis - by (simp only: UNION_fold_union finite_set) -qed +lemma SUPR_set_fold: -- "FIXME move to List.thy" + "SUPR (set xs) f = foldl (\y x. sup (f x) y) bot xs" + unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute) subsection {* Derived set operations *} diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/List.thy --- a/src/HOL/List.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/List.thy Fri Dec 04 11:19:00 2009 +0100 @@ -2665,6 +2665,10 @@ apply(rule length_remdups_leq) done +lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)" +apply(induct xs) +apply auto +done lemma distinct_map: "distinct(map f xs) = (distinct xs & inj_on f (set xs))" diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Number_Theory/Primes.thy Fri Dec 04 11:19:00 2009 +0100 @@ -360,16 +360,15 @@ from prime_dvd_mult_nat[OF p pab'] have "p dvd a \ p dvd b" . moreover - {assume pa: "p dvd a" - have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) + { assume pa: "p dvd a" from coprime_common_divisor_nat [OF ab, OF pa] p have "\ p dvd b" by auto with p have "coprime b p" by (subst gcd_commute_nat, intro prime_imp_coprime_nat) hence pnb: "coprime (p^n) b" by (subst gcd_commute_nat, rule coprime_exp_nat) - from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast } + from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } moreover - {assume pb: "p dvd b" + { assume pb: "p dvd b" have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) from coprime_common_divisor_nat [OF ab, of p] pb p have "\ p dvd a" by auto @@ -377,7 +376,7 @@ by (subst gcd_commute_nat, intro prime_imp_coprime_nat) hence pna: "coprime (p^n) a" by (subst gcd_commute_nat, rule coprime_exp_nat) - from coprime_divprod_nat[OF pab pna] have ?thesis by blast } + from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } ultimately have ?thesis by blast} ultimately show ?thesis by blast qed diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Set.thy Fri Dec 04 11:19:00 2009 +0100 @@ -1556,6 +1556,9 @@ lemma imp_refl: "P --> P" .. +lemma not_mono: "Q --> P ==> ~ P --> ~ Q" + by iprover + lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)" by iprover @@ -1576,9 +1579,6 @@ lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c" by iprover -lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c" - by iprover - subsubsection {* Inverse image of a function *} @@ -1724,7 +1724,6 @@ val contra_subsetD = @{thm contra_subsetD} val distinct_lemma = @{thm distinct_lemma} val eq_to_mono = @{thm eq_to_mono} -val eq_to_mono2 = @{thm eq_to_mono2} val equalityCE = @{thm equalityCE} val equalityD1 = @{thm equalityD1} val equalityD2 = @{thm equalityD2} diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Dec 04 11:19:00 2009 +0100 @@ -177,26 +177,22 @@ fun mk_mono thm = let - val concl = concl_of thm; - fun eq2mono thm' = [thm' RS (thm' RS eq_to_mono)] @ - (case concl of - (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] - | _ => [thm' RS (thm' RS eq_to_mono2)]); + fun eq2mono thm' = thm' RS (thm' RS eq_to_mono); fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) handle THM _ => thm RS @{thm le_boolD} in - case concl of + case concl_of thm of Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) => - [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL - (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))] - | _ => [thm] + dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL + (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) + | _ => thm end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm); -val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono); -val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono); +val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono); +val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono); @@ -338,7 +334,7 @@ REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1), REPEAT (FIRST [atac 1, - resolve_tac (maps mk_mono monos @ get_monos ctxt) 1, + resolve_tac (map mk_mono monos @ get_monos ctxt) 1, etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])); diff -r 99b52900aec0 -r e4890d7bd9f8 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Fri Dec 04 11:19:00 2009 +0100 @@ -311,7 +311,7 @@ fun int_from_string s = case Int.fromString s of SOME i => i - | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") + | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") (* int list -> int list list *) fun clauses xs = let @@ -350,7 +350,7 @@ o (map (map literal_from_int)) o clauses o (map int_from_string) - o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) + o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"]))) o filter_preamble o filter (fn l => l <> "") o split_lines diff -r 99b52900aec0 -r e4890d7bd9f8 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/Pure/Isar/code.ML Fri Dec 04 11:19:00 2009 +0100 @@ -12,6 +12,10 @@ val read_bare_const: theory -> string -> string * typ val read_const: theory -> string -> string val string_of_const: theory -> string -> string + val cert_signature: theory -> typ -> typ + val read_signature: theory -> string -> typ + val const_typ: theory -> string -> typ + val subst_signatures: theory -> term -> term val args_number: theory -> string -> int (*constructor sets*) @@ -31,6 +35,10 @@ val standard_typscheme: theory -> thm list -> thm list (*executable code*) + val add_type: string -> theory -> theory + val add_type_cmd: string -> theory -> theory + val add_signature: string * typ -> theory -> theory + val add_signature_cmd: string * string -> theory -> theory val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory val type_interpretation: @@ -102,6 +110,8 @@ (* constants *) +fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys); + fun check_bare_const thy t = case try dest_Const t of SOME c_ty => c_ty | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); @@ -147,6 +157,7 @@ datatype spec = Spec of { history_concluded: bool, + signatures: int Symtab.table * typ Symtab.table, eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table (*with explicit history*), dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table @@ -154,16 +165,19 @@ cases: (int * (int * string list)) Symtab.table * unit Symtab.table }; -fun make_spec (history_concluded, (eqns, (dtyps, cases))) = - Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases }; -fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns, - dtyps = dtyps, cases = cases }) = - make_spec (f (history_concluded, (eqns, (dtyps, cases)))); -fun merge_spec (Spec { history_concluded = _, eqns = eqns1, +fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) = + Spec { history_concluded = history_concluded, + signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases }; +fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures, + eqns = eqns, dtyps = dtyps, cases = cases }) = + make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases)))); +fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) }, - Spec { history_concluded = _, eqns = eqns2, + Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) = let + val signatures = (Symtab.merge (op =) (tycos1, tycos2), + Symtab.merge typ_equiv (sigs1, sigs2)); fun merge_eqns ((_, history1), (_, history2)) = let val raw_history = AList.merge (op = : serial * serial -> bool) @@ -176,14 +190,16 @@ val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); val cases = (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2)); - in make_spec (false, (eqns, (dtyps, cases))) end; + in make_spec (false, ((signatures, eqns), (dtyps, cases))) end; fun history_concluded (Spec { history_concluded, ... }) = history_concluded; +fun the_signatures (Spec { signatures, ... }) = signatures; fun the_eqns (Spec { eqns, ... }) = eqns; fun the_dtyps (Spec { dtyps, ... }) = dtyps; fun the_cases (Spec { cases, ... }) = cases; val map_history_concluded = map_spec o apfst; -val map_eqns = map_spec o apsnd o apfst; +val map_signatures = map_spec o apsnd o apfst o apfst; +val map_eqns = map_spec o apsnd o apfst o apsnd; val map_dtyps = map_spec o apsnd o apsnd o apfst; val map_cases = map_spec o apsnd o apsnd o apsnd; @@ -236,11 +252,11 @@ structure Code_Data = TheoryDataFun ( type T = spec * data Unsynchronized.ref; - val empty = (make_spec (false, - (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data); + val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty), + (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data); fun copy (spec, data) = (spec, Unsynchronized.ref (! data)); val extend = copy; - fun merge pp ((spec1, data1), (spec2, data2)) = + fun merge _ ((spec1, data1), (spec2, data2)) = (merge_spec (spec1, spec2), Unsynchronized.ref empty_data); ); @@ -334,7 +350,44 @@ (* constants *) -fun args_number thy = length o fst o strip_type o Sign.the_const_type thy; +fun arity_number thy tyco = case Symtab.lookup ((fst o the_signatures o the_exec) thy) tyco + of SOME n => n + | NONE => Sign.arity_number thy tyco; + +fun build_tsig thy = + let + val (tycos, _) = (the_signatures o the_exec) thy; + val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy + |> apsnd (Symtab.fold (fn (tyco, n) => + Symtab.update (tyco, Type.LogicalType n)) tycos); + in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end; + +fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars; + +fun read_signature thy = cert_signature thy o Type.strip_sorts + o Syntax.parse_typ (ProofContext.init thy); + +fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy); + +fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy); + +fun const_typ thy c = case lookup_typ thy c + of SOME ty => ty + | NONE => (Type.strip_sorts o Sign.the_const_type thy) c; + +fun subst_signature thy c ty = + let + fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) = + fold2 mk_subst tys1 tys2 + | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty)) + in case lookup_typ thy c + of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty' + | NONE => ty + end; + +fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t); + +fun args_number thy = length o fst o strip_type o const_typ thy; (* datatypes *) @@ -355,9 +408,10 @@ val _ = if length tfrees <> length vs then no_constr "type variables missing in datatype" c_ty else (); in (tyco, vs) end; - fun ty_sorts (c, ty) = + fun ty_sorts (c, raw_ty) = let - val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; + val ty = subst_signature thy c raw_ty; + val ty_decl = (Logic.unvarifyT o const_typ thy) c; val (tyco, _) = last_typ (c, ty) ty_decl; val (_, vs) = last_typ (c, ty) ty; in ((tyco, map snd vs), (c, (map fst vs, ty))) end; @@ -382,13 +436,13 @@ fun get_datatype thy tyco = case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) of (_, spec) :: _ => spec - | [] => Sign.arity_number thy tyco + | [] => arity_number thy tyco |> Name.invents Name.context Name.aT |> map (rpair []) |> rpair []; fun get_datatype_of_constr thy c = - case (snd o strip_type o Sign.the_const_type thy) c + case (snd o strip_type o const_typ thy) c of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c then SOME tyco else NONE | _ => NONE; @@ -446,21 +500,25 @@ ("Variable with application on left hand side of equation\n" ^ Display.string_of_thm_global thy thm) | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) - | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty - then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) - then () - else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" - ^ Display.string_of_thm_global thy thm) - else bad_thm - ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" - ^ Display.string_of_thm_global thy thm); + | check n (Const (c_ty as (_, ty))) = + let + val c' = AxClass.unoverload_const thy c_ty + in if n = (length o fst o strip_type o subst_signature thy c') ty + then if not proper orelse is_constr_pat c' + then () + else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" + ^ Display.string_of_thm_global thy thm) + else bad_thm + ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" + ^ Display.string_of_thm_global thy thm) + end; val _ = map (check 0) args; val _ = if not proper orelse is_linear thm then () else bad_thm ("Duplicate variables on left hand side of equation\n" ^ Display.string_of_thm_global thy thm); val _ = if (is_none o AxClass.class_of_param thy) c then () - else bad_thm ("Polymorphic constant as head in equation\n" + else bad_thm ("Overloaded constant as head in equation\n" ^ Display.string_of_thm_global thy thm) val _ = if not (is_constr thy c) then () @@ -488,29 +546,34 @@ fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm)) o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; -(*those following are permissive wrt. to overloaded constants!*) +val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; -val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; fun const_typ_eqn thy thm = let val (c, ty) = head_eqn thm; val c' = AxClass.unoverload_const thy (c, ty); + (*permissive wrt. to overloaded constants!*) in (c', ty) end; + fun const_eqn thy = fst o const_typ_eqn thy; -fun typscheme thy (c, ty) = +fun raw_typscheme thy (c, ty) = (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); + +fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty); + fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy; + fun typscheme_eqns thy c [] = let - val raw_ty = Sign.the_const_type thy c; + val raw_ty = const_typ thy c; val tvars = Term.add_tvar_namesT raw_ty []; val tvars' = case AxClass.class_of_param thy c of SOME class => [TFree (Name.aT, [class])] | NONE => Name.invent_list [] Name.aT (length tvars) |> map (fn v => TFree (v, [])); val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; - in typscheme thy (c, ty) end + in raw_typscheme thy (c, ty) end | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm; fun assert_eqns_const thy c eqns = @@ -639,6 +702,34 @@ (** declaring executable ingredients **) +(* constant signatures *) + +fun add_type tyco thy = + case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco + of SOME (Type.Abbreviation (vs, _, _)) => + (map_exec_purge NONE o map_signatures o apfst) + (Symtab.update (tyco, length vs)) thy + | _ => error ("No such type abbreviation: " ^ quote tyco); + +fun add_type_cmd s thy = add_type (Sign.intern_type thy s) thy; + +fun gen_add_signature prep_const prep_signature (raw_c, raw_ty) thy = + let + val c = prep_const thy raw_c; + val ty = prep_signature thy raw_ty; + val ty' = expand_signature thy ty; + val ty'' = Sign.the_const_type thy c; + val _ = if typ_equiv (ty', ty'') then () else + error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty); + in + thy + |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty)) + end; + +val add_signature = gen_add_signature (K I) cert_signature; +val add_signature_cmd = gen_add_signature read_const read_signature; + + (* datatypes *) structure Type_Interpretation = diff -r 99b52900aec0 -r e4890d7bd9f8 src/Pure/type.ML --- a/src/Pure/type.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/Pure/type.ML Fri Dec 04 11:19:00 2009 +0100 @@ -19,6 +19,7 @@ types: decl Name_Space.table, log_types: string list} val empty_tsig: tsig + val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool diff -r 99b52900aec0 -r e4890d7bd9f8 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/Tools/Code/code_preproc.ML Fri Dec 04 11:19:00 2009 +0100 @@ -111,7 +111,7 @@ -- perhaps by means of upcoming code certificates with a corresponding preprocessor protocol*); -fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); +fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); fun eqn_conv conv = let @@ -148,7 +148,7 @@ in ct |> Simplifier.rewrite pre - |> rhs_conv (AxClass.unoverload_conv thy) + |> trans_conv_rule (AxClass.unoverload_conv thy) end; fun postprocess_conv thy ct = @@ -157,7 +157,7 @@ in ct |> AxClass.overload_conv thy - |> rhs_conv (Simplifier.rewrite post) + |> trans_conv_rule (Simplifier.rewrite post) end; fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); diff -r 99b52900aec0 -r e4890d7bd9f8 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Dec 03 19:31:55 2009 +0100 +++ b/src/Tools/Code/code_thingol.ML Fri Dec 04 11:19:00 2009 +0100 @@ -711,7 +711,7 @@ and translate_eqn thy algbr eqngr (thm, proper) = let val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals - o Logic.unvarify o prop_of) thm; + o Code.subst_signatures thy o Logic.unvarify o prop_of) thm; in fold_map (translate_term thy algbr eqngr (SOME thm)) args ##>> translate_term thy algbr eqngr (SOME thm) rhs @@ -888,7 +888,7 @@ val stmt_value = fold_map (translate_tyvar_sort thy algbr eqngr) vs ##>> translate_typ thy algbr eqngr ty - ##>> translate_term thy algbr eqngr NONE t + ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t) #>> (fn ((vs, ty), t) => Fun (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))]))); fun term_value (dep, (naming, program1)) =