86 val add_binds_i: (indexname * term option) list -> context -> context |
86 val add_binds_i: (indexname * term option) list -> context -> context |
87 val auto_bind_goal: term list -> context -> context |
87 val auto_bind_goal: term list -> context -> context |
88 val auto_bind_facts: term list -> context -> context |
88 val auto_bind_facts: term list -> context -> context |
89 val match_bind: bool -> (string list * string) list -> context -> term list * context |
89 val match_bind: bool -> (string list * string) list -> context -> term list * context |
90 val match_bind_i: bool -> (term list * term) list -> context -> term list * context |
90 val match_bind_i: bool -> (term list * term) list -> context -> term list * context |
91 val read_propp: context * (string * (string list * string list)) list list |
91 val read_propp: context * (string * string list) list list |
92 -> context * (term * (term list * term list)) list list |
92 -> context * (term * term list) list list |
93 val cert_propp: context * (term * (term list * term list)) list list |
93 val cert_propp: context * (term * term list) list list |
94 -> context * (term * (term list * term list)) list list |
94 -> context * (term * term list) list list |
95 val read_propp_schematic: context * (string * (string list * string list)) list list |
95 val read_propp_schematic: context * (string * string list) list list |
96 -> context * (term * (term list * term list)) list list |
96 -> context * (term * term list) list list |
97 val cert_propp_schematic: context * (term * (term list * term list)) list list |
97 val cert_propp_schematic: context * (term * term list) list list |
98 -> context * (term * (term list * term list)) list list |
98 -> context * (term * term list) list list |
99 val bind_propp: context * (string * (string list * string list)) list list |
99 val bind_propp: context * (string * string list) list list |
100 -> context * (term list list * (context -> context)) |
100 -> context * (term list list * (context -> context)) |
101 val bind_propp_i: context * (term * (term list * term list)) list list |
101 val bind_propp_i: context * (term * term list) list list |
102 -> context * (term list list * (context -> context)) |
102 -> context * (term list list * (context -> context)) |
103 val bind_propp_schematic: context * (string * (string list * string list)) list list |
103 val bind_propp_schematic: context * (string * string list) list list |
104 -> context * (term list list * (context -> context)) |
104 -> context * (term list list * (context -> context)) |
105 val bind_propp_schematic_i: context * (term * (term list * term list)) list list |
105 val bind_propp_schematic_i: context * (term * term list) list list |
106 -> context * (term list list * (context -> context)) |
106 -> context * (term list list * (context -> context)) |
107 val fact_tac: thm list -> int -> tactic |
107 val fact_tac: thm list -> int -> tactic |
108 val some_fact_tac: context -> int -> tactic |
108 val some_fact_tac: context -> int -> tactic |
109 val get_thm: context -> thmref -> thm |
109 val get_thm: context -> thmref -> thm |
110 val get_thm_closure: context -> thmref -> thm |
110 val get_thm_closure: context -> thmref -> thm |
140 val invent_fixes: string list -> context -> string list * context |
140 val invent_fixes: string list -> context -> string list * context |
141 val fix_frees: term -> context -> context |
141 val fix_frees: term -> context -> context |
142 val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) |
142 val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) |
143 val bind_fixes: string list -> context -> (term -> term) * context |
143 val bind_fixes: string list -> context -> (term -> term) * context |
144 val add_assms: export -> |
144 val add_assms: export -> |
145 ((string * attribute list) * (string * (string list * string list)) list) list -> |
145 ((string * attribute list) * (string * string list) list) list -> |
146 context -> (bstring * thm list) list * context |
146 context -> (bstring * thm list) list * context |
147 val add_assms_i: export -> |
147 val add_assms_i: export -> |
148 ((string * attribute list) * (term * (term list * term list)) list) list -> |
148 ((string * attribute list) * (term * term list) list) list -> |
149 context -> (bstring * thm list) list * context |
149 context -> (bstring * thm list) list * context |
150 val assume_export: export |
150 val assume_export: export |
151 val presume_export: export |
151 val presume_export: export |
152 val add_view: context -> cterm list -> context -> context |
152 val add_view: context -> cterm list -> context -> context |
153 val export_view: cterm list -> context -> context -> thm -> thm |
153 val export_view: cterm list -> context -> context -> thm -> thm |
831 end; |
831 end; |
832 |
832 |
833 |
833 |
834 (* simult_matches *) |
834 (* simult_matches *) |
835 |
835 |
836 fun simult_matches ctxt [] = [] |
836 fun simult_matches _ (_, []) = [] |
837 | simult_matches ctxt pairs = |
837 | simult_matches ctxt (t, pats) = |
838 let |
838 let |
839 fun fail () = error "Pattern match failed!"; |
839 fun fail () = error "Pattern match failed!"; |
840 |
840 |
|
841 val pairs = map (rpair t) pats; |
841 val maxidx = fold (fn (t1, t2) => fn i => |
842 val maxidx = fold (fn (t1, t2) => fn i => |
842 Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1; |
843 Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1; |
843 val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx, |
844 val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx, |
844 map swap pairs); (*prefer assignment of variables from patterns*) |
845 map swap pairs); (*prefer assignment of variables from patterns*) |
845 val env = |
846 val env = |
883 local |
884 local |
884 |
885 |
885 fun prep_bind prep_pats (raw_pats, t) ctxt = |
886 fun prep_bind prep_pats (raw_pats, t) ctxt = |
886 let |
887 let |
887 val ctxt' = declare_term t ctxt; |
888 val ctxt' = declare_term t ctxt; |
888 val pats = prep_pats (fastype_of t) ctxt' raw_pats; |
889 val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats; |
889 val binds = simult_matches ctxt' (map (rpair t) pats); |
890 val binds = simult_matches ctxt' (t, pats); |
890 in (binds, ctxt') end; |
891 in (binds, ctxt') end; |
891 |
892 |
892 fun gen_binds prep_terms prep_pats gen raw_binds ctxt = |
893 fun gen_binds prep_terms prep_pats gen raw_binds ctxt = |
893 let |
894 let |
894 val ts = prep_terms ctxt (map snd raw_binds); |
895 val ts = prep_terms ctxt (map snd raw_binds); |
917 |
918 |
918 local |
919 local |
919 |
920 |
920 fun prep_propp schematic prep_props prep_pats (context, args) = |
921 fun prep_propp schematic prep_props prep_pats (context, args) = |
921 let |
922 let |
922 fun prep (_, (raw_pats1, raw_pats2)) (ctxt, prop :: props) = |
923 fun prep (_, raw_pats) (ctxt, prop :: props) = |
923 let |
924 let val ctxt' = declare_term prop ctxt |
924 val ctxt' = declare_term prop ctxt; |
925 in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end |
925 val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2); (*simultaneous type inference!*) |
|
926 in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end |
|
927 | prep _ _ = sys_error "prep_propp"; |
926 | prep _ _ = sys_error "prep_propp"; |
928 val (propp, (context', _)) = (fold_map o fold_map) prep args |
927 val (propp, (context', _)) = (fold_map o fold_map) prep args |
929 (context, prep_props schematic context (maps (map fst) args)); |
928 (context, prep_props schematic context (maps (map fst) args)); |
930 in (context', propp) end; |
929 in (context', propp) end; |
931 |
930 |
932 fun matches ctxt (prop, (pats1, pats2)) = |
|
933 simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2); |
|
934 |
|
935 fun gen_bind_propp prepp (ctxt, raw_args) = |
931 fun gen_bind_propp prepp (ctxt, raw_args) = |
936 let |
932 let |
937 val (ctxt', args) = prepp (ctxt, raw_args); |
933 val (ctxt', args) = prepp (ctxt, raw_args); |
938 val binds = flat (flat (map (map (matches ctxt')) args)); |
934 val binds = flat (flat (map (map (simult_matches ctxt')) args)); |
939 val propss = map (map #1) args; |
935 val propss = map (map #1) args; |
940 |
936 |
941 (*generalize result: context evaluated now, binds added later*) |
937 (*generalize result: context evaluated now, binds added later*) |
942 val gen = generalize ctxt' ctxt; |
938 val gen = generalize ctxt' ctxt; |
943 fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds))); |
939 fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds))); |