# HG changeset patch # User blanchet # Date 1409697098 -7200 # Node ID e4965b677ba980249d7d4411514d4f85402054a6 # Parent e3d1912a0c8f932e3815c9b1a98647885b3c5ef2 added countable tactic for new-style datatypes diff -r e3d1912a0c8f -r e4965b677ba9 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Wed Sep 03 00:31:37 2014 +0200 +++ b/src/HOL/Library/Countable.thy Wed Sep 03 00:31:38 2014 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/Library/Countable.thy Author: Alexander Krauss, TU Muenchen Author: Brian Huffman, Portland State University + Author: Jasmin Blanchette, TU Muenchen *) header {* Encoding (almost) everything into natural numbers *} @@ -49,10 +50,7 @@ by (simp add: from_nat_def) -subsection {* Countable types *} - -instance nat :: countable - by (rule countable_classI [of "id"]) simp +subsection {* Finite types are countable *} subclass (in finite) countable proof @@ -65,113 +63,8 @@ then show "\to_nat \ 'a \ nat. inj to_nat" by (rule exI[of inj]) qed -text {* Pairs *} -instance prod :: (countable, countable) countable - by (rule countable_classI [of "\(x, y). prod_encode (to_nat x, to_nat y)"]) - (auto simp add: prod_encode_eq) - - -text {* Sums *} - -instance sum :: (countable, countable) countable - by (rule countable_classI [of "(\x. case x of Inl a \ to_nat (False, to_nat a) - | Inr b \ to_nat (True, to_nat b))"]) - (simp split: sum.split_asm) - - -text {* Integers *} - -instance int :: countable - by (rule countable_classI [of "int_encode"]) - (simp add: int_encode_eq) - - -text {* Options *} - -instance option :: (countable) countable - by (rule countable_classI [of "case_option 0 (Suc \ to_nat)"]) - (simp split: option.split_asm) - - -text {* Lists *} - -instance list :: (countable) countable - by (rule countable_classI [of "list_encode \ map to_nat"]) - (simp add: list_encode_eq) - - -text {* Further *} - -instance String.literal :: countable - by (rule countable_classI [of "to_nat o String.explode"]) - (auto simp add: explode_inject) - -text {* Functions *} - -instance "fun" :: (finite, countable) countable -proof - obtain xs :: "'a list" where xs: "set xs = UNIV" - using finite_list [OF finite_UNIV] .. - show "\to_nat::('a \ 'b) \ nat. inj to_nat" - proof - show "inj (\f. to_nat (map f xs))" - by (rule injI, simp add: xs fun_eq_iff) - qed -qed - - -subsection {* The Rationals are Countably Infinite *} - -definition nat_to_rat_surj :: "nat \ rat" where -"nat_to_rat_surj n = (let (a,b) = prod_decode n - in Fract (int_decode a) (int_decode b))" - -lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" -unfolding surj_def -proof - fix r::rat - show "\n. r = nat_to_rat_surj n" - proof (cases r) - fix i j assume [simp]: "r = Fract i j" and "j > 0" - have "r = (let m = int_encode i; n = int_encode j - in nat_to_rat_surj(prod_encode (m,n)))" - by (simp add: Let_def nat_to_rat_surj_def) - thus "\n. r = nat_to_rat_surj n" by(auto simp:Let_def) - qed -qed - -lemma Rats_eq_range_nat_to_rat_surj: "\ = range nat_to_rat_surj" -by (simp add: Rats_def surj_nat_to_rat_surj) - -context field_char_0 -begin - -lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: - "\ = range (of_rat o nat_to_rat_surj)" -using surj_nat_to_rat_surj -by (auto simp: Rats_def image_def surj_def) - (blast intro: arg_cong[where f = of_rat]) - -lemma surj_of_rat_nat_to_rat_surj: - "r\\ \ \n. r = of_rat(nat_to_rat_surj n)" -by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def) - -end - -instance rat :: countable -proof - show "\to_nat::rat \ nat. inj to_nat" - proof - have "surj nat_to_rat_surj" - by (rule surj_nat_to_rat_surj) - then show "inj (inv nat_to_rat_surj)" - by (rule surj_imp_inj_inv) - qed -qed - - -subsection {* Automatically proving countability of datatypes *} +subsection {* Automatically proving countability of old-style datatypes *} inductive finite_item :: "'a Old_Datatype.item \ bool" where undefined: "finite_item undefined" @@ -268,8 +161,8 @@ qed ML {* - fun countable_tac ctxt = - SUBGOAL (fn (goal, i) => + fun old_countable_tac ctxt = + SUBGOAL (fn (goal, _) => let val ty_name = (case goal of @@ -279,7 +172,7 @@ val typedef_thm = #type_definition (snd typedef_info) val pred_name = (case HOLogic.dest_Trueprop (concl_of typedef_thm) of - (typedef $ rep $ abs $ (collect $ Const (n, _))) => n + (_ $ _ $ _ $ (_ $ Const (n, _))) => n | _ => raise Match) val induct_info = Inductive.the_inductive ctxt pred_name val pred_names = #names (fst induct_info) @@ -301,33 +194,124 @@ end) *} -method_setup countable_datatype = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt)) -*} "prove countable class instances for datatypes" - hide_const (open) finite_item nth_item -subsection {* Countable datatypes *} +subsection {* Automatically proving countability of new-style datatypes *} + +ML_file "bnf_lfp_countable.ML" + +method_setup countable_datatype = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD (fn st => HEADGOAL (old_countable_tac ctxt) st + handle ERROR _ => BNF_LFP_Countable.countable_tac ctxt st)) +*} "prove countable class instances for datatypes" + + +subsection {* More Countable types *} + +text {* Naturals *} -(* TODO: automate *) +instance nat :: countable + by (rule countable_classI [of "id"]) simp + +text {* Pairs *} + +instance prod :: (countable, countable) countable + by (rule countable_classI [of "\(x, y). prod_encode (to_nat x, to_nat y)"]) + (auto simp add: prod_encode_eq) -primrec encode_typerep :: "typerep \ nat" where - "encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))" +text {* Sums *} + +instance sum :: (countable, countable) countable + by (rule countable_classI [of "(\x. case x of Inl a \ to_nat (False, to_nat a) + | Inr b \ to_nat (True, to_nat b))"]) + (simp split: sum.split_asm) + +text {* Integers *} -lemma encode_typerep_injective: "\u. encode_typerep t = encode_typerep u \ t = u" - apply (induct t) - apply (rule allI) - apply (case_tac u) - apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1]) - done +instance int :: countable + by (rule countable_classI [of int_encode]) (simp add: int_encode_eq) + +text {* Options *} + +instance option :: (countable) countable + by countable_datatype + +text {* Lists *} + +instance list :: (countable) countable + by countable_datatype + +text {* String literals *} + +instance String.literal :: countable + by (rule countable_classI [of "to_nat o String.explode"]) (auto simp add: explode_inject) + +text {* Functions *} + +instance "fun" :: (finite, countable) countable +proof + obtain xs :: "'a list" where xs: "set xs = UNIV" + using finite_list [OF finite_UNIV] .. + show "\to_nat::('a \ 'b) \ nat. inj to_nat" + proof + show "inj (\f. to_nat (map f xs))" + by (rule injI, simp add: xs fun_eq_iff) + qed +qed + +text {* Typereps *} instance typerep :: countable - apply default - apply (unfold inj_on_def ball_UNIV) - apply (rule exI) - apply (rule allI) - apply (rule encode_typerep_injective) - done + by countable_datatype + + +subsection {* The rationals are countably infinite *} + +definition nat_to_rat_surj :: "nat \ rat" where + "nat_to_rat_surj n = (let (a, b) = prod_decode n in Fract (int_decode a) (int_decode b))" + +lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" +unfolding surj_def +proof + fix r::rat + show "\n. r = nat_to_rat_surj n" + proof (cases r) + fix i j assume [simp]: "r = Fract i j" and "j > 0" + have "r = (let m = int_encode i; n = int_encode j + in nat_to_rat_surj(prod_encode (m,n)))" + by (simp add: Let_def nat_to_rat_surj_def) + thus "\n. r = nat_to_rat_surj n" by(auto simp:Let_def) + qed +qed + +lemma Rats_eq_range_nat_to_rat_surj: "\ = range nat_to_rat_surj" + by (simp add: Rats_def surj_nat_to_rat_surj) + +context field_char_0 +begin + +lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: + "\ = range (of_rat o nat_to_rat_surj)" + using surj_nat_to_rat_surj + by (auto simp: Rats_def image_def surj_def) (blast intro: arg_cong[where f = of_rat]) + +lemma surj_of_rat_nat_to_rat_surj: + "r\\ \ \n. r = of_rat(nat_to_rat_surj n)" + by (simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def) end + +instance rat :: countable +proof + show "\to_nat::rat \ nat. inj to_nat" + proof + have "surj nat_to_rat_surj" + by (rule surj_nat_to_rat_surj) + then show "inj (inv nat_to_rat_surj)" + by (rule surj_imp_inj_inv) + qed +qed + +end diff -r e3d1912a0c8f -r e4965b677ba9 src/HOL/Library/bnf_lfp_countable.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/bnf_lfp_countable.ML Wed Sep 03 00:31:38 2014 +0200 @@ -0,0 +1,183 @@ +(* Title: HOL/Library/bnf_lfp_countable.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2014 + +Countability tactic for BNF datatypes. +*) + +signature BNF_LFP_COUNTABLE = +sig + val countable_tac: Proof.context -> tactic +end; + +structure BNF_LFP_Countable : BNF_LFP_COUNTABLE = +struct + +open BNF_FP_Rec_Sugar_Util +open BNF_Def +open BNF_Util +open BNF_Tactics +open BNF_FP_Util +open BNF_FP_Def_Sugar + +fun nchotomy_tac nchotomy = + HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN' + CHANGED_PROP o REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' + CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac [exE, disjE])); + +fun meta_spec_mp_tac 0 = K all_tac + | meta_spec_mp_tac n = + dtac meta_spec THEN' meta_spec_mp_tac (n - 1) THEN' dtac meta_mp THEN' atac; + +val use_induction_hypothesis_tac = + DEEPEN (1, 1000000 (* large number *)) + (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0; + +val same_ctr_simps = + @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split simp_thms snd_conv}; + +fun same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' = + HEADGOAL (asm_full_simp_tac (ss_only (injects @ recs @ map_comps' @ same_ctr_simps) ctxt) THEN' + REPEAT_DETERM o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac (conjE :: inj_map_strongs')) + THEN_ALL_NEW use_induction_hypothesis_tac); + +fun distinct_ctrs_tac ctxt recs = + HEADGOAL (asm_full_simp_tac (ss_only (recs @ + @{thms sum_encode_eq sum.inject sum.distinct simp_thms}) ctxt)); + +fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = + let val ks = 1 upto n in + EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' => + if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' + else distinct_ctrs_tac ctxt recs) ks) ks) + end; + +fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' = + HEADGOAL (rtac induct) THEN + EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs => + mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs') + ns nchotomys injectss recss); + +fun endgame_tac ctxt encode_injectives = + unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN + ALLGOALS (rtac exI THEN' rtac allI THEN' resolve_tac encode_injectives); + +fun encode_sumN n k t = + Balanced_Tree.access {init = t, + left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t), + right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)} + n k; + +fun encode_tuple [] = @{term "0 :: nat"} + | encode_tuple ts = + Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts; + +fun mk_to_nat T = Const (@{const_name to_nat}, T --> HOLogic.natT); + +fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 = + let + val thy = Proof_Context.theory_of ctxt; + + val nn = length ns; + val recs as rec1 :: _ = + map2 (fn fpT => mk_co_rec thy Least_FP fpT (replicate nn HOLogic.natT)) fpTs recs0; + val arg_Ts = binder_fun_types (fastype_of rec1); + val arg_Tss = Library.unflat ctrss0 arg_Ts; + + fun mk_U (Type (@{type_name prod}, [T1, T2])) = + if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2) + | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts) + | mk_U T = T; + + fun mk_nat (j, T) = + if T = HOLogic.natT then + SOME (Bound j) + else if member (op =) fpTs T then + NONE + else if exists_subtype_in fpTs T then + let val U = mk_U T in + SOME (mk_to_nat U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j)) + end + else + SOME (mk_to_nat T $ Bound j); + + fun mk_arg n (k, arg_T) = + let + val bound_Ts = rev (binder_types arg_T); + val nats = map_filter mk_nat (tag_list 0 bound_Ts); + in + fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats)) + end; + + val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss); + in + map (fn recx => Term.list_comb (recx, flat argss)) recs + end; + +fun mk_encode_injective_thms _ [] = [] + | mk_encode_injective_thms ctxt fpT_names0 = + let + fun not_datatype s = error (quote s ^ " is not a new-style datatype"); + fun not_mutually_recursive ss = + error ("{" ^ commas ss ^ "} is not a set of mutually recursive new-style datatypes"); + + fun lfp_sugar_of s = + (case fp_sugar_of ctxt s of + SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar + | _ => not_datatype s); + + val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0))); + val fpT_names = map (fst o dest_Type) fpTs0; + + val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt; + val As = + map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) @{sort countable} S)) + As_names var_As; + val fpTs = map (fn s => Type (s, As)) fpT_names; + + val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0; + + fun mk_conjunct fpT x encode_fun = + HOLogic.all_const fpT $ Abs (Name.uu, fpT, + HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0), + HOLogic.eq_const fpT $ x $ Bound 0)); + + val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ = + map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; + val ctr_sugars = map #ctr_sugar fp_sugars; + + val ctrss0 = map #ctrs ctr_sugars; + val ns = map length ctrss0; + val recs0 = map #co_rec fp_sugars; + val nchotomys = map #nchotomy ctr_sugars; + val injectss = map #injects ctr_sugars; + val rec_thmss = map #co_rec_thms fp_sugars; + val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs; + val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs; + + val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs; + + val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); + val goal = HOLogic.mk_Trueprop (Balanced_Tree.make HOLogic.mk_conj conjuncts); + in + Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} => + mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps' + inj_map_strongs') + |> HOLogic.conj_elims + |> Proof_Context.export names_ctxt ctxt + |> map Thm.close_derivation + end; + +fun get_countable_goal_typ (@{const Trueprop} $ (Const (@{const_name Ex}, _) + $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0 + $ Const (@{const_name top}, _)))) = s + | get_countable_goal_typ _ = error "Wrong goal format for countable tactic"; + +fun core_countable_tac ctxt st = + endgame_tac ctxt (mk_encode_injective_thms ctxt (map get_countable_goal_typ (Thm.prems_of st))) + st; + +fun countable_tac ctxt = + TRY (Class.intro_classes_tac []) THEN core_countable_tac ctxt; + +end;