author | blanchet |
Mon, 20 Jan 2014 18:24:56 +0100 | |
changeset 55058 | 4e700eb471d4 |
parent 55025 | src/HOL/BNF/Tools/bnf_decl.ML@1ac0a0194428 |
permissions | -rw-r--r-- |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_decl.ML |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
3 |
Copyright 2013 |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
4 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
5 |
Axiomatic declaration of bounded natural functors. |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
6 |
*) |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
7 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
8 |
signature BNF_DECL = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
9 |
sig |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
10 |
val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding -> |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
11 |
typ list -> local_theory -> BNF_Def.bnf * local_theory |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
12 |
end |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
13 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
14 |
structure BNF_Decl : BNF_DECL = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
15 |
struct |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
16 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
17 |
open BNF_Util |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
18 |
open BNF_Def |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
19 |
|
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
20 |
fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy = |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
21 |
let |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
22 |
fun prepare_type_arg (set_opt, (ty, c)) = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
23 |
let val s = fst (dest_TFree (prepare_typ lthy ty)) in |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
24 |
(set_opt, (s, prepare_constraint lthy c)) |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
25 |
end; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
26 |
val ((user_setbs, vars), raw_vars') = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
27 |
map prepare_type_arg raw_vars |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
28 |
|> `split_list |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
29 |
|>> apfst (map_filter I); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
30 |
val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
31 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
32 |
fun mk_b name user_b = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
33 |
(if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
34 |
|> Binding.qualify false (Binding.name_of b); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
35 |
val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
36 |
val (bd_type_Tname, lthy) = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
37 |
Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
38 |
val T = Type (Tname, map TFree vars); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
39 |
val bd_type_T = Type (bd_type_Tname, map TFree deads); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
40 |
val lives = map TFree (filter_out (member (op =) deads) vars); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
41 |
val live = length lives; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
42 |
val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
43 |
val (lives', _) = BNF_Util.mk_TFrees (length lives) |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
44 |
(fold Variable.declare_typ (map TFree vars) lthy); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
45 |
val T' = Term.typ_subst_atomic (lives ~~ lives') T; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
46 |
val mapT = map2 (curry op -->) lives lives' ---> T --> T'; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
47 |
val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
48 |
val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
49 |
val mapb = mk_b BNF_Def.mapN user_mapb; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
50 |
val bdb = mk_b "bd" Binding.empty; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
51 |
val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
52 |
(if live = 1 then [0] else 1 upto live); |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
53 |
|
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
54 |
val witTs = map (prepare_typ lthy) user_witTs; |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
55 |
val nwits = length witTs; |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
56 |
val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
57 |
(if nwits = 1 then [0] else 1 upto nwits); |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
58 |
|
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
59 |
val lthy = Local_Theory.background_theory |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
60 |
(Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
61 |
map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
62 |
map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
63 |
lthy; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
64 |
val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
65 |
val Fsets = map2 (fn setb => fn setT => |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
66 |
Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
67 |
val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
68 |
val Fwits = map2 (fn witb => fn witT => |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
69 |
Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
70 |
val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
71 |
prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads)) |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
72 |
user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
73 |
lthy; |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
74 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
75 |
fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
76 |
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
77 |
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
78 |
|
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
79 |
val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
80 |
(Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
81 |
||> `Local_Theory.restore; |
54960 | 82 |
|
83 |
fun mk_wit_thms set_maps = |
|
84 |
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) |
|
85 |
|> Conjunction.elim_balanced (length wit_goals) |
|
86 |
|> map2 (Conjunction.elim_balanced o length) wit_goalss |
|
87 |
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); |
|
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
88 |
val phi = Proof_Context.export_morphism lthy_old lthy; |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
89 |
val thms = unflat all_goalss (Morphism.fact phi raw_thms); |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
90 |
in |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
91 |
BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy) |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
92 |
end; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
93 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
94 |
val bnf_decl = prepare_decl (K I) (K I); |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
95 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
96 |
fun read_constraint _ NONE = HOLogic.typeS |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
97 |
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
98 |
|
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
99 |
val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ; |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
100 |
|
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
101 |
val parse_witTs = |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
102 |
@{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
103 |
>> (fn ("wits", Ts) => Ts |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
104 |
| (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
105 |
@{keyword "]"} || Scan.succeed []; |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
106 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
107 |
val parse_bnf_decl = |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
108 |
parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
109 |
parse_witTs -- Parse.opt_mixfix; |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
110 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
111 |
val _ = |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
112 |
Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration" |
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
113 |
(parse_bnf_decl >> |
55025
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
114 |
(fn ((((bsTs, b), (mapb, relb)), witTs), mx) => |
1ac0a0194428
support declaration of nonemptiness witnesses in bnf_decl
traytel
parents:
54960
diff
changeset
|
115 |
bnf_decl_cmd bsTs b mx mapb relb witTs #> snd)); |
54601
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
116 |
|
91a1e4aa7c80
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
traytel
parents:
diff
changeset
|
117 |
end; |