27 * Element.context_i list) * ((string * typ) list * Proof.context) |
27 * Element.context_i list) * ((string * typ) list * Proof.context) |
28 (*FIXME*) |
28 (*FIXME*) |
29 val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> |
29 val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> |
30 Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list |
30 Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list |
31 * Element.context_i list) * ((string * typ) list * Proof.context) |
31 * Element.context_i list) * ((string * typ) list * Proof.context) |
32 val add_locale: bstring -> bstring -> expression_i -> Element.context_i list -> |
32 val add_locale: binding -> binding -> expression_i -> Element.context_i list -> |
33 theory -> string * local_theory |
33 theory -> string * local_theory |
34 val add_locale_cmd: bstring -> bstring -> expression -> Element.context list -> |
34 val add_locale_cmd: binding -> binding -> expression -> Element.context list -> |
35 theory -> string * local_theory |
35 theory -> string * local_theory |
36 |
36 |
37 (* Interpretation *) |
37 (* Interpretation *) |
38 val cert_goal_expression: expression_i -> Proof.context -> |
38 val cert_goal_expression: expression_i -> Proof.context -> |
39 (term list list * (string * morphism) list * morphism) * Proof.context |
39 (term list list * (string * morphism) list * morphism) * Proof.context |
40 val read_goal_expression: expression -> Proof.context -> |
40 val read_goal_expression: expression -> Proof.context -> |
41 (term list list * (string * morphism) list * morphism) * Proof.context |
41 (term list list * (string * morphism) list * morphism) * Proof.context |
42 val sublocale: string -> expression_i -> theory -> Proof.state |
42 val sublocale: string -> expression_i -> theory -> Proof.state |
43 val sublocale_cmd: string -> expression -> theory -> Proof.state |
43 val sublocale_cmd: string -> expression -> theory -> Proof.state |
44 val interpretation: expression_i -> (Attrib.binding * term) list -> |
44 val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state |
45 theory -> Proof.state |
45 val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state |
46 val interpretation_cmd: expression -> (Attrib.binding * string) list -> |
|
47 theory -> Proof.state |
|
48 val interpret: expression_i -> bool -> Proof.state -> Proof.state |
46 val interpret: expression_i -> bool -> Proof.state -> Proof.state |
49 val interpret_cmd: expression -> bool -> Proof.state -> Proof.state |
47 val interpret_cmd: expression -> bool -> Proof.state -> Proof.state |
50 end; |
48 end; |
51 |
|
52 |
49 |
53 structure Expression : EXPRESSION = |
50 structure Expression : EXPRESSION = |
54 struct |
51 struct |
55 |
52 |
56 datatype ctxt = datatype Element.ctxt; |
53 datatype ctxt = datatype Element.ctxt; |
88 if null dups then () else error (message ^ commas dups) |
85 if null dups then () else error (message ^ commas dups) |
89 end; |
86 end; |
90 |
87 |
91 fun match_bind (n, b) = (n = Binding.name_of b); |
88 fun match_bind (n, b) = (n = Binding.name_of b); |
92 fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) = |
89 fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) = |
93 (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) |
90 Binding.eq_name (b1, b2) andalso |
94 Binding.name_of b1 = Binding.name_of b2 andalso |
|
95 (mx1 = mx2 orelse |
91 (mx1 = mx2 orelse |
96 error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression")); |
92 error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression")); |
97 |
93 |
98 fun params_loc loc = |
94 fun params_loc loc = |
99 (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc); |
95 (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc); |
100 fun params_inst (expr as (loc, (prfx, Positional insts))) = |
96 fun params_inst (expr as (loc, (prfx, Positional insts))) = |
101 let |
97 let |
102 val (ps, loc') = params_loc loc; |
98 val (ps, loc') = params_loc loc; |
130 val (implicit, expr') = params_expr expr; |
126 val (implicit, expr') = params_expr expr; |
131 |
127 |
132 val implicit' = map (#1 #> Binding.name_of) implicit; |
128 val implicit' = map (#1 #> Binding.name_of) implicit; |
133 val fixed' = map (#1 #> Binding.name_of) fixed; |
129 val fixed' = map (#1 #> Binding.name_of) fixed; |
134 val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; |
130 val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; |
135 val implicit'' = if strict then [] |
131 val implicit'' = |
136 else let val _ = reject_dups |
132 if strict then [] |
|
133 else |
|
134 let val _ = reject_dups |
137 "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed') |
135 "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed') |
138 in map (fn (b, mx) => (b, NONE, mx)) implicit end; |
136 in map (fn (b, mx) => (b, NONE, mx)) implicit end; |
139 |
137 |
140 in (expr', implicit'' @ fixed) end; |
138 in (expr', implicit'' @ fixed) end; |
141 |
139 |
174 val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; |
172 val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; |
175 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); |
173 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); |
176 val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; |
174 val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; |
177 val res = Syntax.check_terms ctxt arg; |
175 val res = Syntax.check_terms ctxt arg; |
178 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
176 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
179 |
177 |
180 (* instantiation *) |
178 (* instantiation *) |
181 val (type_parms'', res') = chop (length type_parms) res; |
179 val (type_parms'', res') = chop (length type_parms) res; |
182 val insts'' = (parm_names ~~ res') |> map_filter |
180 val insts'' = (parm_names ~~ res') |> map_filter |
183 (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | |
181 (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | |
184 inst => SOME inst); |
182 inst => SOME inst); |
364 val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt; |
362 val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt; |
365 val inst''' = insts'' |> List.last |> snd |> snd; |
363 val inst''' = insts'' |> List.last |> snd |> snd; |
366 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; |
364 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; |
367 val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt; |
365 val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt; |
368 in (i+1, insts', ctxt'') end; |
366 in (i+1, insts', ctxt'') end; |
369 |
367 |
370 fun prep_elem insts raw_elem (elems, ctxt) = |
368 fun prep_elem insts raw_elem (elems, ctxt) = |
371 let |
369 let |
372 val ctxt' = declare_elem prep_vars_elem raw_elem ctxt; |
370 val ctxt' = declare_elem prep_vars_elem raw_elem ctxt; |
373 val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; |
371 val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; |
374 val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt'; |
372 val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt'; |
388 prep_concl raw_concl (insts', elems, ctxt5); |
386 prep_concl raw_concl (insts', elems, ctxt5); |
389 |
387 |
390 (* Retrieve parameter types *) |
388 (* Retrieve parameter types *) |
391 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes) |
389 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes) |
392 | _ => fn ps => ps) (Fixes fors :: elems') []; |
390 | _ => fn ps => ps) (Fixes fors :: elems') []; |
393 val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; |
391 val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; |
394 val parms = xs ~~ Ts; (* params from expression and elements *) |
392 val parms = xs ~~ Ts; (* params from expression and elements *) |
395 |
393 |
396 val Fixes fors' = finish_primitive parms I (Fixes fors); |
394 val Fixes fors' = finish_primitive parms I (Fixes fors); |
397 val (deps, elems'') = finish ctxt6 parms do_close insts elems'; |
395 val (deps, elems'') = finish ctxt6 parms do_close insts elems'; |
398 |
396 |
488 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
486 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
489 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
487 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
490 val exp_typ = Logic.type_map exp_term; |
488 val exp_typ = Logic.type_map exp_term; |
491 val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
489 val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
492 in ((propss, deps, export'), goal_ctxt) end; |
490 in ((propss, deps, export'), goal_ctxt) end; |
493 |
491 |
494 in |
492 in |
495 |
493 |
496 fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; |
494 fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; |
497 fun read_goal_expression x = prep_goal_expression read_full_context_statement x; |
495 fun read_goal_expression x = prep_goal_expression read_full_context_statement x; |
498 |
496 |
633 val statement = ObjectLogic.ensure_propT thy head; |
631 val statement = ObjectLogic.ensure_propT thy head; |
634 |
632 |
635 val ([pred_def], defs_thy) = |
633 val ([pred_def], defs_thy) = |
636 thy |
634 thy |
637 |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |
635 |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |
638 |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd |
636 |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd |
639 |> PureThy.add_defs false |
637 |> PureThy.add_defs false |
640 [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])]; |
638 [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; |
641 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; |
639 val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; |
642 |
640 |
643 val cert = Thm.cterm_of defs_thy; |
641 val cert = Thm.cterm_of defs_thy; |
644 |
642 |
645 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
643 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
658 Tactic.compose_tac (false, ax, 0) 1)); |
656 Tactic.compose_tac (false, ax, 0) 1)); |
659 in ((statement, intro, axioms), defs_thy) end; |
657 in ((statement, intro, axioms), defs_thy) end; |
660 |
658 |
661 in |
659 in |
662 |
660 |
663 (* CB: main predicate definition function *) |
661 (* main predicate definition function *) |
664 |
662 |
665 fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy = |
663 fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy = |
666 let |
664 let |
667 val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs; |
665 val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs; |
668 |
666 |
669 val (a_pred, a_intro, a_axioms, thy'') = |
667 val (a_pred, a_intro, a_axioms, thy'') = |
670 if null exts then (NONE, NONE, [], thy) |
668 if null exts then (NONE, NONE, [], thy) |
671 else |
669 else |
672 let |
670 let |
673 val aname = if null ints then pname else pname ^ "_" ^ axiomsN; |
671 val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname |
674 val ((statement, intro, axioms), thy') = |
672 val ((statement, intro, axioms), thy') = |
675 thy |
673 thy |
676 |> def_pred aname parms defs' exts exts'; |
674 |> def_pred aname parms defs' exts exts'; |
677 val (_, thy'') = |
675 val (_, thy'') = |
678 thy' |
676 thy' |
679 |> Sign.add_path aname |
677 |> Sign.add_path (Binding.name_of aname) |
680 |> Sign.no_base_names |
678 |> Sign.no_base_names |
681 |> PureThy.note_thmss Thm.internalK |
679 |> PureThy.note_thmss Thm.internalK |
682 [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])] |
680 [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])] |
683 ||> Sign.restore_naming thy'; |
681 ||> Sign.restore_naming thy'; |
684 in (SOME statement, SOME intro, axioms, thy'') end; |
682 in (SOME statement, SOME intro, axioms, thy'') end; |
689 val ((statement, intro, axioms), thy''') = |
687 val ((statement, intro, axioms), thy''') = |
690 thy'' |
688 thy'' |
691 |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); |
689 |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); |
692 val (_, thy'''') = |
690 val (_, thy'''') = |
693 thy''' |
691 thy''' |
694 |> Sign.add_path pname |
692 |> Sign.add_path (Binding.name_of pname) |
695 |> Sign.no_base_names |
693 |> Sign.no_base_names |
696 |> PureThy.note_thmss Thm.internalK |
694 |> PureThy.note_thmss Thm.internalK |
697 [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]), |
695 [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]), |
698 ((Binding.name axiomsN, []), |
696 ((Binding.name axiomsN, []), |
699 [(map (Drule.standard o Element.conclude_witness) axioms, [])])] |
697 [(map (Drule.standard o Element.conclude_witness) axioms, [])])] |
720 | defines_to_notes _ e = e; |
718 | defines_to_notes _ e = e; |
721 |
719 |
722 fun gen_add_locale prep_decl |
720 fun gen_add_locale prep_decl |
723 bname raw_predicate_bname raw_import raw_body thy = |
721 bname raw_predicate_bname raw_import raw_body thy = |
724 let |
722 let |
725 val name = Sign.full_bname thy bname; |
723 val name = Sign.full_name thy bname; |
726 val _ = Locale.defined thy name andalso |
724 val _ = Locale.defined thy name andalso |
727 error ("Duplicate definition of locale " ^ quote name); |
725 error ("Duplicate definition of locale " ^ quote name); |
728 |
726 |
729 val ((fixed, deps, body_elems), (parms, ctxt')) = |
727 val ((fixed, deps, body_elems), (parms, ctxt')) = |
730 prep_decl raw_import I raw_body (ProofContext.init thy); |
728 prep_decl raw_import I raw_body (ProofContext.init thy); |
731 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
729 val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; |
732 |
730 |
733 val predicate_bname = if raw_predicate_bname = "" then bname |
731 val predicate_bname = |
|
732 if Binding.is_empty raw_predicate_bname then bname |
734 else raw_predicate_bname; |
733 else raw_predicate_bname; |
735 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = |
734 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = |
736 define_preds predicate_bname parms text thy; |
735 define_preds predicate_bname parms text thy; |
737 |
736 |
738 val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; |
737 val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; |
739 val _ = if null extraTs then () |
738 val _ = |
740 else warning ("Additional type variable(s) in locale specification " ^ quote bname); |
739 if null extraTs then () |
|
740 else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname)); |
741 |
741 |
742 val a_satisfy = Element.satisfy_morphism a_axioms; |
742 val a_satisfy = Element.satisfy_morphism a_axioms; |
743 val b_satisfy = Element.satisfy_morphism b_axioms; |
743 val b_satisfy = Element.satisfy_morphism b_axioms; |
744 |
744 |
745 val params = fixed @ |
745 val params = fixed @ |
746 (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat); |
746 (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat); |
747 val asm = if is_some b_statement then b_statement else a_statement; |
747 val asm = if is_some b_statement then b_statement else a_statement; |
748 |
748 |
749 val notes = |
749 val notes = |
750 if is_some asm |
750 if is_some asm |
751 then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []), |
751 then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []), |
752 [([Assumption.assume (cterm_of thy' (the asm))], |
752 [([Assumption.assume (cterm_of thy' (the asm))], |
753 [(Attrib.internal o K) Locale.witness_attrib])])])] |
753 [(Attrib.internal o K) Locale.witness_attrib])])])] |
754 else []; |
754 else []; |
755 |
755 |
756 val notes' = body_elems |> |
756 val notes' = body_elems |> |
764 val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; |
764 val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; |
765 val axioms = map Element.conclude_witness b_axioms; |
765 val axioms = map Element.conclude_witness b_axioms; |
766 |
766 |
767 val loc_ctxt = thy' |
767 val loc_ctxt = thy' |
768 |> Locale.register_locale bname (extraTs, params) |
768 |> Locale.register_locale bname (extraTs, params) |
769 (asm, rev defs) (a_intro, b_intro) axioms ([], []) |
769 (asm, rev defs) (a_intro, b_intro) axioms ([], []) |
770 (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |
770 (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |
771 |> TheoryTarget.init (SOME name) |
771 |> TheoryTarget.init (SOME name) |
772 |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes'; |
772 |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes'; |
773 |
773 |
774 in (name, loc_ctxt) end; |
774 in (name, loc_ctxt) end; |
791 let |
791 let |
792 val target = intern thy raw_target; |
792 val target = intern thy raw_target; |
793 val target_ctxt = Locale.init target thy; |
793 val target_ctxt = Locale.init target thy; |
794 |
794 |
795 val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; |
795 val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt; |
796 |
796 |
797 fun after_qed witss = ProofContext.theory ( |
797 fun after_qed witss = ProofContext.theory ( |
798 fold2 (fn (name, morph) => fn wits => Locale.add_dependency target |
798 fold2 (fn (name, morph) => fn wits => Locale.add_dependency target |
799 (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #> |
799 (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #> |
800 (fn thy => fold_rev Locale.activate_global_facts |
800 (fn thy => fold_rev Locale.activate_global_facts |
801 (Locale.get_registrations thy) thy)); |
801 (Locale.get_registrations thy) thy)); |
877 let |
877 let |
878 val _ = Proof.assert_forward_or_chain state; |
878 val _ = Proof.assert_forward_or_chain state; |
879 val ctxt = Proof.context_of state; |
879 val ctxt = Proof.context_of state; |
880 |
880 |
881 val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; |
881 val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt; |
882 |
882 |
883 fun store_reg (name, morph) thms = |
883 fun store_reg (name, morph) thms = |
884 let |
884 let |
885 val morph' = morph $> Element.satisfy_morphism thms $> export; |
885 val morph' = morph $> Element.satisfy_morphism thms $> export; |
886 in Locale.activate_local_facts (name, morph') end; |
886 in Locale.activate_local_facts (name, morph') end; |
887 |
887 |