# HG changeset patch # User blanchet # Date 1458646777 -3600 # Node ID 9bfcbab7cd9903112be28337deb539f8e9aecf81 # Parent c4fad0569a246397324df4cfc8eff9fecf27b1b8 put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Library/BNF_Axiomatization.thy --- a/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 22 08:00:33 2016 +0100 +++ b/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 22 12:39:37 2016 +0100 @@ -13,6 +13,6 @@ "bnf_axiomatization" :: thy_decl begin -ML_file "bnf_axiomatization.ML" +ML_file "../Tools/BNF/bnf_axiomatization.ML" end diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Tue Mar 22 08:00:33 2016 +0100 +++ b/src/HOL/Library/Countable.thy Tue Mar 22 12:39:37 2016 +0100 @@ -200,7 +200,7 @@ subsection \Automatically proving countability of datatypes\ -ML_file "bnf_lfp_countable.ML" +ML_file "../Tools/BNF/bnf_lfp_countable.ML" ML \ fun countable_datatype_tac ctxt st = diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Tue Mar 22 08:00:33 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,128 +0,0 @@ -(* Title: HOL/Library/bnf_axiomatization.ML - Author: Dmitriy Traytel, TU Muenchen - Copyright 2013 - -Axiomatic declaration of bounded natural functors. -*) - -signature BNF_AXIOMATIZATION = -sig - val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> - mixfix -> binding -> binding -> binding -> typ list -> local_theory -> - BNF_Def.bnf * local_theory -end - -structure BNF_Axiomatization : BNF_AXIOMATIZATION = -struct - -open BNF_Util -open BNF_Def - -fun prepare_decl prepare_plugins prepare_constraint prepare_typ - raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy = - let - val plugins = prepare_plugins lthy raw_plugins; - - fun prepare_type_arg (set_opt, (ty, c)) = - let val s = fst (dest_TFree (prepare_typ lthy ty)) in - (set_opt, (s, prepare_constraint lthy c)) - end; - val ((user_setbs, vars), raw_vars') = - map prepare_type_arg raw_vars - |> `split_list - |>> apfst (map_filter I); - val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; - - fun mk_b name user_b = - (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) - |> Binding.qualify false (Binding.name_of b); - val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy; - val (bd_type_Tname, lthy) = lthy - |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn); - val T = Type (Tname, map TFree vars); - val bd_type_T = Type (bd_type_Tname, map TFree deads); - val lives = map TFree (filter_out (member (op =) deads) vars); - val live = length lives; - val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; - val (lives', _) = BNF_Util.mk_TFrees (length lives) - (fold Variable.declare_typ (map TFree vars) lthy); - val T' = Term.typ_subst_atomic (lives ~~ lives') T; - val mapT = map2 (curry op -->) lives lives' ---> T --> T'; - val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; - val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); - val mapb = mk_b mapN user_mapb; - val bdb = mk_b "bd" Binding.empty; - val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs - (if live = 1 then [0] else 1 upto live); - - val witTs = map (prepare_typ lthy) user_witTs; - val nwits = length witTs; - val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) - (if nwits = 1 then [0] else 1 upto nwits); - - val lthy = Local_Theory.background_theory - (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: - map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ - map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) - lthy; - val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); - val Fsets = map2 (fn setb => fn setT => - Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; - val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); - val Fwits = map2 (fn witb => fn witT => - Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; - val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = - prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) - user_mapb user_relb user_predb user_setbs - (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE) - lthy; - - fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; - val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; - val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); - - val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result - (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy; - - fun mk_wit_thms set_maps = - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) - (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) - |> Thm.close_derivation - |> Conjunction.elim_balanced (length wit_goals) - |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> (map o map) (Thm.forall_elim_vars 0); - val phi = Local_Theory.target_morphism lthy; - val thms = unflat all_goalss (Morphism.fact phi raw_thms); - - val (bnf, lthy') = after_qed mk_wit_thms thms lthy - in - (bnf, register_bnf plugins key bnf lthy') - end; - -val bnf_axiomatization = prepare_decl (K I) (K I) (K I); - -fun read_constraint _ NONE = @{sort type} - | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; - -val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ; - -val parse_witTs = - @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ - >> (fn ("wits", Ts) => Ts - | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| - @{keyword "]"} || Scan.succeed []; - -val parse_bnf_axiomatization_options = - Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true)); - -val parse_bnf_axiomatization = - parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- - parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings; - -val _ = - Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration" - (parse_bnf_axiomatization >> - (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) => - bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd)); - -end; diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Library/bnf_lfp_countable.ML --- a/src/HOL/Library/bnf_lfp_countable.ML Tue Mar 22 08:00:33 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -(* 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 derive_encode_injectives_thms: Proof.context -> string list -> thm list - val countable_datatype_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 - -val countableS = @{sort countable}; - -fun nchotomy_tac ctxt nchotomy = - HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN' - REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE])); - -fun meta_spec_mp_tac ctxt 0 = K all_tac - | meta_spec_mp_tac ctxt depth = - dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' - dtac ctxt meta_mp THEN' assume_tac ctxt; - -fun use_induction_hypothesis_tac ctxt = - DEEPEN (1, 64 (* large number *)) - (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN' - assume_tac ctxt THEN' assume_tac ctxt) 0; - -val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split - id_apply snd_conv simp_thms}; -val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; - -fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = - HEADGOAL (asm_full_simp_tac - (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' - TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW - REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW - (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt)); - -fun distinct_ctrs_tac ctxt recs = - HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) 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 ctxt 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 ctxt induct) THEN - EVERY (@{map 4} (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 ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt 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_encode_funs ctxt fpTs ns ctrss0 recs0 = - let - val thy = Proof_Context.theory_of ctxt; - - fun check_countable T = - Sign.of_sort thy (T, countableS) orelse - raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []); - - fun mk_to_nat_checked T = - Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT); - - val nn = length ns; - val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (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_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j)) - end - else - SOME (mk_to_nat_checked 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 derive_encode_injectives_thms _ [] = [] - | derive_encode_injectives_thms ctxt fpT_names0 = - let - fun not_datatype s = error (quote s ^ " is not a datatype"); - fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive 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) :: _ = - map (#T o lfp_sugar_of o fst o dest_Type) (#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 =) countableS 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, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = - map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; - val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; - - val ctrss0 = map #ctrs ctr_sugars; - val ns = map length ctrss0; - val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars; - val nchotomys = map #nchotomy ctr_sugars; - val injectss = map #injects ctr_sugars; - val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) 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 = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); - val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts); - in - Goal.prove (*no 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 ctxt - |> Proof_Context.export names_ctxt ctxt - |> map Thm.close_derivation - end; - -fun get_countable_goal_type_name (@{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_type_name _ = error "Wrong goal format for datatype countability tactic"; - -fun core_countable_datatype_tac ctxt st = - let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in - endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st - end; - -fun countable_datatype_tac ctxt = - TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt; - -end; diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Tools/BNF/bnf_axiomatization.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Tue Mar 22 12:39:37 2016 +0100 @@ -0,0 +1,128 @@ +(* Title: HOL/Tools/BNF/bnf_axiomatization.ML + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +signature BNF_AXIOMATIZATION = +sig + val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> + mixfix -> binding -> binding -> binding -> typ list -> local_theory -> + BNF_Def.bnf * local_theory +end + +structure BNF_Axiomatization : BNF_AXIOMATIZATION = +struct + +open BNF_Util +open BNF_Def + +fun prepare_decl prepare_plugins prepare_constraint prepare_typ + raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy = + let + val plugins = prepare_plugins lthy raw_plugins; + + fun prepare_type_arg (set_opt, (ty, c)) = + let val s = fst (dest_TFree (prepare_typ lthy ty)) in + (set_opt, (s, prepare_constraint lthy c)) + end; + val ((user_setbs, vars), raw_vars') = + map prepare_type_arg raw_vars + |> `split_list + |>> apfst (map_filter I); + val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; + + fun mk_b name user_b = + (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) + |> Binding.qualify false (Binding.name_of b); + val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy; + val (bd_type_Tname, lthy) = lthy + |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn); + val T = Type (Tname, map TFree vars); + val bd_type_T = Type (bd_type_Tname, map TFree deads); + val lives = map TFree (filter_out (member (op =) deads) vars); + val live = length lives; + val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; + val (lives', _) = BNF_Util.mk_TFrees (length lives) + (fold Variable.declare_typ (map TFree vars) lthy); + val T' = Term.typ_subst_atomic (lives ~~ lives') T; + val mapT = map2 (curry op -->) lives lives' ---> T --> T'; + val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; + val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); + val mapb = mk_b mapN user_mapb; + val bdb = mk_b "bd" Binding.empty; + val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs + (if live = 1 then [0] else 1 upto live); + + val witTs = map (prepare_typ lthy) user_witTs; + val nwits = length witTs; + val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) + (if nwits = 1 then [0] else 1 upto nwits); + + val lthy = Local_Theory.background_theory + (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: + map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ + map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) + lthy; + val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); + val Fsets = map2 (fn setb => fn setT => + Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; + val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); + val Fwits = map2 (fn witb => fn witT => + Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; + val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = + prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) + user_mapb user_relb user_predb user_setbs + (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE) + lthy; + + fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); + + val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result + (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy; + + fun mk_wit_thms set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) + (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) + |> Thm.close_derivation + |> Conjunction.elim_balanced (length wit_goals) + |> map2 (Conjunction.elim_balanced o length) wit_goalss + |> (map o map) (Thm.forall_elim_vars 0); + val phi = Local_Theory.target_morphism lthy; + val thms = unflat all_goalss (Morphism.fact phi raw_thms); + + val (bnf, lthy') = after_qed mk_wit_thms thms lthy + in + (bnf, register_bnf plugins key bnf lthy') + end; + +val bnf_axiomatization = prepare_decl (K I) (K I) (K I); + +fun read_constraint _ NONE = @{sort type} + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; + +val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ; + +val parse_witTs = + @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ + >> (fn ("wits", Ts) => Ts + | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| + @{keyword "]"} || Scan.succeed []; + +val parse_bnf_axiomatization_options = + Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true)); + +val parse_bnf_axiomatization = + parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- + parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings; + +val _ = + Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration" + (parse_bnf_axiomatization >> + (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) => + bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd)); + +end; diff -r c4fad0569a24 -r 9bfcbab7cd99 src/HOL/Tools/BNF/bnf_lfp_countable.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Mar 22 12:39:37 2016 +0100 @@ -0,0 +1,195 @@ +(* Title: HOL/Tools/BNF/bnf_lfp_countable.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2014 + +Countability tactic for BNF datatypes. +*) + +signature BNF_LFP_COUNTABLE = +sig + val derive_encode_injectives_thms: Proof.context -> string list -> thm list + val countable_datatype_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 + +val countableS = @{sort countable}; + +fun nchotomy_tac ctxt nchotomy = + HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN' + REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE])); + +fun meta_spec_mp_tac ctxt 0 = K all_tac + | meta_spec_mp_tac ctxt depth = + dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' + dtac ctxt meta_mp THEN' assume_tac ctxt; + +fun use_induction_hypothesis_tac ctxt = + DEEPEN (1, 64 (* large number *)) + (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN' + assume_tac ctxt THEN' assume_tac ctxt) 0; + +val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split + id_apply snd_conv simp_thms}; +val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; + +fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = + HEADGOAL (asm_full_simp_tac + (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' + TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW + REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW + (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt)); + +fun distinct_ctrs_tac ctxt recs = + HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) 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 ctxt 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 ctxt induct) THEN + EVERY (@{map 4} (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 ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt 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_encode_funs ctxt fpTs ns ctrss0 recs0 = + let + val thy = Proof_Context.theory_of ctxt; + + fun check_countable T = + Sign.of_sort thy (T, countableS) orelse + raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []); + + fun mk_to_nat_checked T = + Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT); + + val nn = length ns; + val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (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_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j)) + end + else + SOME (mk_to_nat_checked 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 derive_encode_injectives_thms _ [] = [] + | derive_encode_injectives_thms ctxt fpT_names0 = + let + fun not_datatype s = error (quote s ^ " is not a datatype"); + fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive 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) :: _ = + map (#T o lfp_sugar_of o fst o dest_Type) (#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 =) countableS 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, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = + map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; + val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; + + val ctrss0 = map #ctrs ctr_sugars; + val ns = map length ctrss0; + val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars; + val nchotomys = map #nchotomy ctr_sugars; + val injectss = map #injects ctr_sugars; + val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) 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 = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts); + in + Goal.prove (*no 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 ctxt + |> Proof_Context.export names_ctxt ctxt + |> map Thm.close_derivation + end; + +fun get_countable_goal_type_name (@{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_type_name _ = error "Wrong goal format for datatype countability tactic"; + +fun core_countable_datatype_tac ctxt st = + let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in + endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st + end; + +fun countable_datatype_tac ctxt = + TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt; + +end;