21 val print_cases: context -> unit |
22 val print_cases: context -> unit |
22 val pretty_prems: context -> Pretty.T list |
23 val pretty_prems: context -> Pretty.T list |
23 val pretty_context: context -> Pretty.T list |
24 val pretty_context: context -> Pretty.T list |
24 val print_proof_data: theory -> unit |
25 val print_proof_data: theory -> unit |
25 val init: theory -> context |
26 val init: theory -> context |
26 val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list |
27 val assumptions: context -> (cterm list * exporter) list |
27 val fixed_names: context -> string list |
28 val fixed_names: context -> string list |
28 val read_typ: context -> string -> typ |
29 val read_typ: context -> string -> typ |
29 val cert_typ: context -> typ -> typ |
30 val cert_typ: context -> typ -> typ |
30 val intern_skolem: context -> term -> term |
31 val intern_skolem: context -> term -> term |
31 val extern_skolem: context -> term -> term |
32 val extern_skolem: context -> term -> term |
42 val declare_term: term -> context -> context |
43 val declare_term: term -> context -> context |
43 val declare_terms: term list -> context -> context |
44 val declare_terms: term list -> context -> context |
44 val warn_extra_tfrees: context -> context -> context |
45 val warn_extra_tfrees: context -> context -> context |
45 val generalizeT: context -> context -> typ -> typ |
46 val generalizeT: context -> context -> typ -> typ |
46 val generalize: context -> context -> term -> term |
47 val generalize: context -> context -> term -> term |
47 val find_free: term -> string -> term option |
48 val find_free: term -> string -> term option |
48 val export_wrt: context -> context option |
49 val export_wrt: bool -> context -> context option -> (thm -> thm Seq.seq) * (int -> tactic) list |
49 -> (thm -> thm) * ((int -> tactic) * (int -> tactic)) list |
|
50 val auto_bind_goal: term -> context -> context |
50 val auto_bind_goal: term -> context -> context |
51 val auto_bind_facts: string -> term list -> context -> context |
51 val auto_bind_facts: string -> term list -> context -> context |
52 val match_bind: bool -> (string list * string) list -> context -> context |
52 val match_bind: bool -> (string list * string) list -> context -> context |
53 val match_bind_i: bool -> (term list * term) list -> context -> context |
53 val match_bind_i: bool -> (term list * term) list -> context -> context |
54 val read_propp: context * (string * (string list * string list)) |
54 val read_propp: context * (string * (string list * string list)) |
67 val put_thmss: (string * thm list) list -> context -> context |
67 val put_thmss: (string * thm list) list -> context -> context |
68 val reset_thms: string -> context -> context |
68 val reset_thms: string -> context -> context |
69 val have_thmss: |
69 val have_thmss: |
70 ((string * context attribute list) * (thm list * context attribute list) list) list -> |
70 ((string * context attribute list) * (thm list * context attribute list) list) list -> |
71 context -> context * (string * thm list) list |
71 context -> context * (string * thm list) list |
72 val assume: ((int -> tactic) * (int -> tactic)) |
72 val assume: exporter |
73 -> (string * context attribute list * (string * (string list * string list)) list) list |
73 -> (string * context attribute list * (string * (string list * string list)) list) list |
74 -> context -> context * ((string * thm list) list * thm list) |
74 -> context -> context * ((string * thm list) list * thm list) |
75 val assume_i: ((int -> tactic) * (int -> tactic)) |
75 val assume_i: exporter |
76 -> (string * context attribute list * (term * (term list * term list)) list) list |
76 -> (string * context attribute list * (term * (term list * term list)) list) list |
77 -> context -> context * ((string * thm list) list * thm list) |
77 -> context -> context * ((string * thm list) list * thm list) |
78 val read_vars: context * (string list * string option) -> context * (string list * typ option) |
78 val read_vars: context * (string list * string option) -> context * (string list * typ option) |
79 val cert_vars: context * (string list * typ option) -> context * (string list * typ option) |
79 val cert_vars: context * (string list * typ option) -> context * (string list * typ option) |
80 val fix: (string list * string option) list -> context -> context |
80 val fix: (string list * string option) list -> context -> context |
99 struct |
99 struct |
100 |
100 |
101 |
101 |
102 (** datatype context **) |
102 (** datatype context **) |
103 |
103 |
|
104 type exporter = |
|
105 (cterm list -> thm -> thm Seq.seq) * (bool -> int -> (int -> tactic) list); |
|
106 |
104 datatype context = |
107 datatype context = |
105 Context of |
108 Context of |
106 {thy: theory, (*current theory*) |
109 {thy: theory, (*current theory*) |
107 data: Object.T Symtab.table, (*user data*) |
110 data: Object.T Symtab.table, (*user data*) |
108 asms: |
111 asms: |
109 ((cterm * ((int -> tactic) * (int -> tactic))) list * (*assumes: A ==> _*) |
112 ((cterm list * exporter) list * (*assumes: A ==> _*) |
110 (string * thm list) list) * |
113 (string * thm list) list) * |
111 ((string * string) list * string list), (*fixes: !!x. _*) |
114 ((string * string) list * string list), (*fixes: !!x. _*) |
112 binds: (term * typ) option Vartab.table, (*term bindings*) |
115 binds: (term * typ) option Vartab.table, (*term bindings*) |
113 thms: thm list option Symtab.table, (*local thms*) |
116 thms: thm list option Symtab.table, (*local thms*) |
114 cases: (string * RuleCases.T) list, (*local contexts*) |
117 cases: (string * RuleCases.T) list, (*local contexts*) |
653 fun find_free t x = foldl_aterms (get_free x) (None, t); |
656 fun find_free t x = foldl_aterms (get_free x) (None, t); |
654 |
657 |
655 |
658 |
656 local |
659 local |
657 |
660 |
658 fun export tfrees fixes casms thm = |
661 fun export tfrees fixes goal_asms thm = |
659 let |
662 thm |
660 val rule = |
663 |> Drule.forall_elim_vars 0 |
661 thm |
664 |> Seq.EVERY (rev (map op |> goal_asms)) |
|
665 |> Seq.map (fn rule => |
|
666 let |
|
667 val {sign, prop, maxidx, ...} = Thm.rep_thm rule; |
|
668 val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes); |
|
669 in |
|
670 rule |
|
671 |> Drule.forall_intr_list frees |
662 |> Drule.forall_elim_vars 0 |
672 |> Drule.forall_elim_vars 0 |
663 |> Drule.implies_intr_list casms; |
673 |> Drule.tvars_intr_list tfrees |
664 val {sign, prop, ...} = Thm.rep_thm rule; |
674 end); |
665 val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes); |
|
666 in |
|
667 rule |
|
668 |> Drule.forall_intr_list frees |
|
669 |> Drule.forall_elim_vars 0 |
|
670 |> Drule.tvars_intr_list tfrees |
|
671 end; |
|
672 |
675 |
673 fun diff_context inner None = (gen_tfrees inner None, fixed_names inner, assumptions inner) |
676 fun diff_context inner None = (gen_tfrees inner None, fixed_names inner, assumptions inner) |
674 | diff_context inner (Some outer) = |
677 | diff_context inner (Some outer) = |
675 (gen_tfrees inner (Some outer), |
678 (gen_tfrees inner (Some outer), |
676 fixed_names inner \\ fixed_names outer, |
679 fixed_names inner \\ fixed_names outer, |
677 Library.drop (length (assumptions outer), assumptions inner)); |
680 Library.drop (length (assumptions outer), assumptions inner)); |
678 |
681 |
679 in |
682 in |
680 |
683 |
681 fun export_wrt inner opt_outer = |
684 fun export_wrt is_goal inner opt_outer = |
682 let |
685 let |
683 val (tfrees, fixes, asms) = diff_context inner opt_outer; |
686 val (tfrees, fixes, asms) = diff_context inner opt_outer; |
684 val casms = map (Drule.mk_cgoal o #1) asms; |
687 val goal_asms = map (fn (cprops, (exp, _)) => (map Drule.mk_cgoal cprops, exp)) asms; |
685 val tacs = map #2 asms; |
688 val tacs = flat (map (fn (cprops, (_, f)) => f is_goal (length cprops)) asms); |
686 in (export tfrees fixes casms, tacs) end; |
689 in (export tfrees fixes goal_asms, tacs) end; |
687 |
690 |
688 end; |
691 end; |
689 |
692 |
690 |
693 |
691 |
694 |
878 |
881 |
879 (* assume *) |
882 (* assume *) |
880 |
883 |
881 local |
884 local |
882 |
885 |
883 fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) = |
886 fun gen_assm prepp (ctxt, (name, attrs, raw_prop_pats)) = |
884 let |
887 let |
885 val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); |
888 val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); |
886 |
889 |
887 val cprops = map (Thm.cterm_of (sign_of ctxt')) props; |
890 val cprops = map (Thm.cterm_of (sign_of ctxt')) props; |
888 val cprops_tac = map (rpair tac) cprops; |
|
889 val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops; |
891 val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops; |
890 |
892 |
891 val ths = map (fn th => ([th], [])) asms; |
893 val ths = map (fn th => ([th], [])) asms; |
892 val (ctxt'', [(_, thms)]) = |
894 val (ctxt'', [(_, thms)]) = |
893 ctxt' |
895 ctxt' |
894 |> auto_bind_facts name props |
896 |> auto_bind_facts name props |
895 |> have_thmss [((name, attrs @ [Drule.tag_assumption]), ths)]; |
897 |> have_thmss [((name, attrs @ [Drule.tag_assumption]), ths)]; |
896 |
898 in (ctxt'', (cprops, (name, asms), (name, thms))) end; |
897 val ctxt''' = |
899 |
898 ctxt'' |
900 fun gen_assms prepp exp args ctxt = |
|
901 let |
|
902 val (ctxt', results) = foldl_map (gen_assm prepp) (ctxt, args); |
|
903 val cprops = flat (map #1 results); |
|
904 val asmss = map #2 results; |
|
905 val thmss = map #3 results; |
|
906 val ctxt'' = |
|
907 ctxt' |
899 |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => |
908 |> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => |
900 (thy, data, ((asms_ct @ cprops_tac, asms_th @ [(name, asms)]), fixes), |
909 (thy, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, |
901 binds, thms, cases, defs)); |
910 cases, defs)); |
902 in (ctxt''', (name, thms)) end; |
911 in (warn_extra_tfrees ctxt ctxt'', (thmss, prems_of ctxt'')) end; |
903 |
|
904 fun gen_assms prepp tac args ctxt = |
|
905 let val (ctxt', thmss) = foldl_map (gen_assm prepp tac) (ctxt, args) |
|
906 in (warn_extra_tfrees ctxt ctxt', (thmss, prems_of ctxt')) end; |
|
907 |
912 |
908 in |
913 in |
909 |
914 |
910 val assume = gen_assms (apsnd #1 o bind_propp); |
915 val assume = gen_assms (apsnd #1 o bind_propp); |
911 val assume_i = gen_assms (apsnd #1 o bind_propp_i); |
916 val assume_i = gen_assms (apsnd #1 o bind_propp_i); |