# HG changeset patch # User traytel # Date 1382444232 -7200 # Node ID c0186a0d8cb3265a2f137ef7c74b41b14eabf078 # Parent 5288fa24c9db064f28a70e16288250757cd96b8e define a trivial nonemptiness witness if none is provided diff -r 5288fa24c9db -r c0186a0d8cb3 src/HOL/BNF/Basic_BNFs.thy --- a/src/HOL/BNF/Basic_BNFs.thy Mon Oct 21 23:45:27 2013 +0200 +++ b/src/HOL/BNF/Basic_BNFs.thy Tue Oct 22 14:17:12 2013 +0200 @@ -27,15 +27,14 @@ lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \ Grp B1 f1 OO (Grp B2 f2)\\ \ (Grp A p1)\\ OO Grp A p2" unfolding wpull_def Grp_def by auto -bnf ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" ["id :: 'a \ 'a"] +bnf ID: "id :: ('a \ 'b) \ 'a \ 'b" ["\x. {x}"] "\_:: 'a. natLeq" "id :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] done -bnf DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] - "op = :: 'a \ 'a \ bool" +bnf DEADID: "id :: 'a \ 'a" [] "\_:: 'a. natLeq +c |UNIV :: 'a set|" "op = :: 'a \ 'a \ bool" by (auto simp add: wpull_Grp_def Grp_def card_order_csum natLeq_card_order card_of_card_order_on cinfinite_csum natLeq_cinfinite) @@ -148,7 +147,7 @@ lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] -bnf map_pair [fsts, snds] "\_::'a \ 'b. natLeq" [Pair] prod_rel +bnf map_pair [fsts, snds] "\_::'a \ 'b. natLeq" prod_rel proof (unfold prod_set_defs) show "map_pair id id = id" by (rule map_pair.id) next @@ -193,7 +192,7 @@ Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_pair snd snd)" unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff by auto -qed simp+ +qed (* Categorical version of pullback: *) lemma wpull_cat: @@ -230,8 +229,8 @@ moreover have "?f ` ?LHS \ ?RHS" unfolding Func_def by fastforce ultimately show ?thesis using card_of_ordLeq by fast qed - -bnf "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] +declare [[bnf_note_all]] +bnf "op \" [range] "\_:: 'a \ 'b. natLeq +c |UNIV :: 'a set|" "fun_rel op =" proof fix f show "id \ f = id f" by simp @@ -278,6 +277,8 @@ Grp {x. range x \ Collect (split R)} (op \ snd)" unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps subset_iff image_iff by auto (force, metis pair_collapse) -qed auto - +qed +term fun_wit +print_bnfs +find_theorems fun_wit end diff -r 5288fa24c9db -r c0186a0d8cb3 src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Mon Oct 21 23:45:27 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Tue Oct 22 14:17:12 2013 +0200 @@ -164,10 +164,9 @@ fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN - REPEAT_DETERM ( - atac 1 ORELSE - REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN - (TRY o dresolve_tac Gwit_thms THEN' + REPEAT_DETERM ((atac ORELSE' + REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN' + etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN' (etac FalseE ORELSE' hyp_subst_tac ctxt THEN' dresolve_tac Fwit_thms THEN' diff -r 5288fa24c9db -r c0186a0d8cb3 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Mon Oct 21 23:45:27 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Tue Oct 22 14:17:12 2013 +0200 @@ -612,14 +612,12 @@ val fact_policy = mk_fact_policy no_defs_lthy; val bnf_b = qualify raw_bnf_b; val live = length raw_sets; - val nwits = length raw_wits; val map_rhs = prep_term no_defs_lthy raw_map; val set_rhss = map (prep_term no_defs_lthy) raw_sets; val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of Abs (_, T, t) => (T, t) | _ => error "Bad bound constant"); - val wit_rhss = map (prep_term no_defs_lthy) raw_wits; fun err T = error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ @@ -672,21 +670,14 @@ else map (fn i => set_name i (fn () => mk_suffix_binding (mk_setN i))) (1 upto live); in bs ~~ set_rhss end; val bd_bind_def = (fn () => def_qualify (mk_suffix_binding bdN), bd_rhs); - val wit_binds_defs = - let - val bs = if nwits = 1 then [fn () => def_qualify (mk_suffix_binding witN)] - else map (fn i => fn () => def_qualify (mk_suffix_binding (mk_witN i))) (1 upto nwits); - in bs ~~ wit_rhss end; - val (((((bnf_map_term, raw_map_def), + val ((((bnf_map_term, raw_map_def), (bnf_set_terms, raw_set_defs)), - (bnf_bd_term, raw_bd_def)), - (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = + (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) = no_defs_lthy |> maybe_define true map_bind_def ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs ||>> maybe_define true bd_bind_def - ||>> apfst split_list o fold_map (maybe_define true) wit_binds_defs ||> `(maybe_restore no_defs_lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -694,7 +685,6 @@ val bnf_map_def = Morphism.thm phi raw_map_def; val bnf_set_defs = map (Morphism.thm phi) raw_set_defs; val bnf_bd_def = Morphism.thm phi raw_bd_def; - val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; val bnf_map = Morphism.term phi bnf_map_term; @@ -713,7 +703,6 @@ val bdT = Morphism.typ phi bd_rhsT; val bnf_bd = Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term); - val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms; (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*) val deads = (case Ds_opt of @@ -770,7 +759,6 @@ val bnf_sets_As = map (mk_bnf_t As') bnf_sets; val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets; val bnf_bd_As = mk_bnf_t As' bnf_bd; - val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; val pre_names_lthy = lthy; val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As), @@ -827,9 +815,23 @@ (fn () => def_qualify (if Binding.is_empty rel_b then mk_suffix_binding relN else rel_b), rel_rhs); - val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) = + val wit_rhss = + if null raw_wits then + [fold_rev Term.absdummy As' (Term.list_comb (bnf_map_AsAs, + map2 (fn T => fn i => Term.absdummy T (Bound i)) As' (live downto 1)) $ + Const (@{const_name undefined}, CA'))] + else map (prep_term no_defs_lthy) raw_wits; + val nwits = length wit_rhss; + val wit_binds_defs = + let + val bs = if nwits = 1 then [fn () => def_qualify (mk_suffix_binding witN)] + else map (fn i => fn () => def_qualify (mk_suffix_binding (mk_witN i))) (1 upto nwits); + in bs ~~ wit_rhss end; + + val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) = lthy |> maybe_define (is_some raw_rel_opt) rel_bind_def + ||>> apfst split_list o fold_map (maybe_define (not (null raw_wits))) wit_binds_defs ||> `(maybe_restore lthy); val phi = Proof_Context.export_morphism lthy_old lthy; @@ -841,6 +843,10 @@ val rel = mk_bnf_rel pred2RTs CA' CB'; val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; + val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs; + val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms; + val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; + val map_id0_goal = let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA') @@ -939,11 +945,14 @@ map wit_goal (0 upto live - 1) end; - val wit_goalss = map mk_wit_goals bnf_wit_As; + val trivial_wit_tac = mk_trivial_wit_tac bnf_wit_defs; - fun after_qed thms lthy = + val wit_goalss = + (if null raw_wits then SOME trivial_wit_tac else NONE, map mk_wit_goals bnf_wit_As); + + fun after_qed mk_wit_thms thms lthy = let - val (axioms, wit_thms) = apfst (mk_axioms live) (chop (length goals) thms); + val (axioms, nontriv_wit_thms) = apfst (mk_axioms live) (chop (length goals) thms); val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]}; val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order]; @@ -1016,6 +1025,9 @@ val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms); + val wit_thms = + if null nontriv_wit_thms then mk_wit_thms (map Lazy.force set_map) else nontriv_wit_thms; + fun mk_in_bd () = let val bdT = fst (dest_relT (fastype_of bnf_bd_As)); @@ -1259,35 +1271,45 @@ (bnf, Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy); -(* TODO: Once the invariant "nwits > 0" holds, remove "mk_conjunction_balanced'" and "rtac TrueI" - below *) -fun mk_conjunction_balanced' [] = @{prop True} - | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts; - fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs = - (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) => + (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => let - val wits_tac = - K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN' - mk_unfold_thms_then_tac lthy one_step_defs wit_tac; - val wit_goals = map mk_conjunction_balanced' wit_goalss; - val wit_thms = - Goal.prove_sorry lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac - |> Conjunction.elim_balanced (length wit_goals) - |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + fun mk_wits_tac set_maps = + K (TRYALL Goal.conjunction_tac) THEN' + (case triv_tac_opt of + SOME tac => tac set_maps + | NONE => mk_unfold_thms_then_tac lthy one_step_defs wit_tac); + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + fun mk_wit_thms set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) + |> Conjunction.elim_balanced (length wit_goals) + |> map2 (Conjunction.elim_balanced o length) wit_goalss + |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); in map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] []) goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs) - |> (fn thms => after_qed (map single thms @ wit_thms) lthy) + |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs; -val bnf_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) => - Proof.unfolding ([[(defs, [])]]) - (Proof.theorem NONE (snd o register_bnf key oo after_qed) - (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo - prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty Binding.empty - []; +val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => + let + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + fun mk_triv_wit_thms tac set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) + (K (TRYALL Goal.conjunction_tac) THEN' tac set_maps) + |> Conjunction.elim_balanced (length wit_goals) + |> map2 (Conjunction.elim_balanced o length) wit_goalss + |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + val (mk_wit_thms, nontriv_wit_goals) = + (case triv_tac_opt of + NONE => (fn _ => [], map (map (rpair [])) wit_goalss) + | SOME tac => (mk_triv_wit_thms tac, [])); + in + Proof.unfolding ([[(defs, [])]]) + (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms) + (map (single o rpair []) goals @ nontriv_wit_goals) lthy) + end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE + Binding.empty Binding.empty []; fun print_bnfs ctxt = let @@ -1324,7 +1346,9 @@ "register a type as a bounded natural functor" ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- - (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term) + (Scan.option ((@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) + >> the_default []) -- + Scan.option Parse.term) >> bnf_cmd); end; diff -r 5288fa24c9db -r c0186a0d8cb3 src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Oct 21 23:45:27 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue Oct 22 14:17:12 2013 +0200 @@ -31,7 +31,10 @@ {prems: thm list, context: Proof.context} -> tactic val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> - thm -> {prems: 'a, context: Proof.context} -> tactic + thm -> {prems: thm list, context: Proof.context} -> tactic + + val mk_trivial_wit_tac: thm list -> thm list -> {prems: thm list, context: Proof.context} -> + tactic end; structure BNF_Def_Tactics : BNF_DEF_TACTICS = @@ -302,4 +305,8 @@ map_comp RS sym, map_id])] 1 end; +fun mk_trivial_wit_tac wit_defs set_maps {context = ctxt, prems = _} = + unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm => + dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac; + end;