1(* Title: HOL/Tools/BNF/bnf_axiomatization.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2013 4 5Axiomatic declaration of bounded natural functors. 6*) 7 8signature BNF_AXIOMATIZATION = 9sig 10 val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> 11 mixfix -> binding -> binding -> binding -> typ list -> local_theory -> 12 BNF_Def.bnf * local_theory 13end 14 15structure BNF_Axiomatization : BNF_AXIOMATIZATION = 16struct 17 18open BNF_Util 19open BNF_Def 20 21fun prepare_decl prepare_plugins prepare_constraint prepare_typ 22 raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy = 23 let 24 val plugins = prepare_plugins lthy raw_plugins; 25 26 fun prepare_type_arg (set_opt, (ty, c)) = 27 let val s = fst (dest_TFree (prepare_typ lthy ty)) in 28 (set_opt, (s, prepare_constraint lthy c)) 29 end; 30 val ((user_setbs, vars), raw_vars') = 31 map prepare_type_arg raw_vars 32 |> `split_list 33 |>> apfst (map_filter I); 34 val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; 35 36 fun mk_b name user_b = 37 (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) 38 |> Binding.qualify false (Binding.name_of b); 39 val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy; 40 val (bd_type_Tname, lthy) = lthy 41 |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn); 42 val T = Type (Tname, map TFree vars); 43 val bd_type_T = Type (bd_type_Tname, map TFree deads); 44 val lives = map TFree (filter_out (member (op =) deads) vars); 45 val live = length lives; 46 val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; 47 val (lives', _) = BNF_Util.mk_TFrees (length lives) 48 (fold Variable.declare_typ (map TFree vars) lthy); 49 val T' = Term.typ_subst_atomic (lives ~~ lives') T; 50 val mapT = map2 (curry op -->) lives lives' ---> T --> T'; 51 val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; 52 val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); 53 val mapb = mk_b mapN user_mapb; 54 val bdb = mk_b "bd" Binding.empty; 55 val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs 56 (if live = 1 then [0] else 1 upto live); 57 58 val witTs = map (prepare_typ lthy) user_witTs; 59 val nwits = length witTs; 60 val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) 61 (if nwits = 1 then [0] else 1 upto nwits); 62 63 val lthy = Local_Theory.background_theory 64 (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: 65 map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ 66 map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) 67 lthy; 68 val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); 69 val Fsets = map2 (fn setb => fn setT => 70 Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; 71 val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); 72 val Fwits = map2 (fn witb => fn witT => 73 Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; 74 val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = 75 prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) 76 user_mapb user_relb user_predb user_setbs 77 (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE) 78 lthy; 79 80 fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; 81 val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; 82 val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); 83 84 val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result 85 (Specification.axiomatization [] [] [] 86 (map_index (fn (i, ax) => 87 ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy; 88 89 fun mk_wit_thms set_maps = 90 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) 91 (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) 92 |> Thm.close_derivation \<^here> 93 |> Conjunction.elim_balanced (length wit_goals) 94 |> map2 (Conjunction.elim_balanced o length) wit_goalss 95 |> (map o map) (Thm.forall_elim_vars 0); 96 val phi = Local_Theory.target_morphism lthy; 97 val thms = unflat all_goalss (Morphism.fact phi raw_thms); 98 99 val (bnf, lthy') = after_qed mk_wit_thms thms lthy 100 in 101 (bnf, register_bnf plugins key bnf lthy') 102 end; 103 104val bnf_axiomatization = prepare_decl (K I) (K I) (K I); 105 106fun read_constraint _ NONE = \<^sort>\<open>type\<close> 107 | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; 108 109val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ; 110 111val parse_witTs = 112 \<^keyword>\<open>[\<close> |-- (Parse.name --| \<^keyword>\<open>:\<close> -- Scan.repeat Parse.typ 113 >> (fn ("wits", Ts) => Ts 114 | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| 115 \<^keyword>\<open>]\<close> || Scan.succeed []; 116 117val parse_bnf_axiomatization_options = 118 Scan.optional (\<^keyword>\<open>(\<close> |-- Plugin_Name.parse_filter --| \<^keyword>\<open>)\<close>) (K (K true)); 119 120val parse_bnf_axiomatization = 121 parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- 122 parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings; 123 124val _ = 125 Outer_Syntax.local_theory \<^command_keyword>\<open>bnf_axiomatization\<close> "bnf declaration" 126 (parse_bnf_axiomatization >> 127 (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) => 128 bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd)); 129 130end; 131