# HG changeset patch # User wenzelm # Date 921674183 -3600 # Node ID 8469852acbc04c263b2670f08f8ee4cdb4c0251e # Parent e71ac23a91118e6c4b7e5b0b43f66f86cba96699 added '_i' versions; add_constdefs; apply_theorems; fixed assume block nest; diff -r e71ac23a9111 -r 8469852acbc0 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Mar 17 13:34:49 1999 +0100 +++ b/src/Pure/Isar/isar_thy.ML Wed Mar 17 13:36:23 1999 +0100 @@ -2,10 +2,9 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Derived theory operations. +Pure/Isar derived theory operations. TODO: - - pure_thy.ML: add_constdefs (atomic!); - 'methods' section (proof macros, ML method defs) (!?); - next_block: ProofHistory open / close (!?); *) @@ -19,33 +18,61 @@ val add_subsection: string -> theory -> theory val add_subsubsection: string -> theory -> theory val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory + val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory + val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory + val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory + val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory + val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list + val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list -> theory -> theory + val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list + -> theory -> theory val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list -> theory -> theory + val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list + -> theory -> theory val have_facts: (string * Args.src list) * (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T + val have_facts_i: (string * Proof.context attribute list) * + (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T + val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T + val from_facts_i: (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T + val chain: ProofHistory.T -> ProofHistory.T val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T + val fix_i: (string * typ) list -> ProofHistory.T -> ProofHistory.T val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T + val match_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T + val theorem_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T + val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T val assume: string -> Args.src list -> (string * string list) list -> ProofHistory.T -> ProofHistory.T + val assume_i: string -> Proof.context attribute list -> (term * term list) list + -> ProofHistory.T -> ProofHistory.T val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T + val show_i: string -> Proof.context attribute list -> term * term list + -> ProofHistory.T -> ProofHistory.T val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T - val chain: ProofHistory.T -> ProofHistory.T - val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T + val have_i: string -> Proof.context attribute list -> term * term list + -> ProofHistory.T -> ProofHistory.T val begin_block: ProofHistory.T -> ProofHistory.T val next_block: ProofHistory.T -> ProofHistory.T val end_block: ProofHistory.T -> ProofHistory.T val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory + val qed_with_i: bstring option * theory attribute list option -> ProofHistory.T -> theory val qed: ProofHistory.T -> theory val kill_proof: ProofHistory.T -> theory val tac: Method.text -> ProofHistory.T -> ProofHistory.T + val tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T + val then_tac_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T val proof: Method.text option -> ProofHistory.T -> ProofHistory.T + val proof_i: (Proof.context -> Proof.method) option -> ProofHistory.T -> ProofHistory.T val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T + val terminal_proof_i: (Proof.context -> Proof.method) -> ProofHistory.T -> ProofHistory.T val immediate_proof: ProofHistory.T -> ProofHistory.T val default_proof: ProofHistory.T -> ProofHistory.T val use_mltext: string -> theory option -> theory option @@ -72,7 +99,7 @@ (** derived theory and proof operations **) -(* formal comments *) (* FIXME dummy *) +(* formal comments *) (* FIXME dummy *) fun add_text (txt:string) (thy:theory) = thy; fun add_title title author date thy = thy; @@ -88,7 +115,20 @@ f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; val add_axioms = add_axms PureThy.add_axioms; +val add_axioms_i = PureThy.add_axioms_i; val add_defs = add_axms PureThy.add_defs; +val add_defs_i = PureThy.add_defs_i; + + +(* constdefs *) + +fun gen_add_constdefs consts defs args thy = + thy + |> consts (map fst args) + |> defs (map (fn ((c, _, mx), s) => ((Thm.def_name (Syntax.const_name c mx), s), [])) args); + +val add_constdefs = gen_add_constdefs Theory.add_consts add_defs; +val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i; (* theorems *) @@ -97,63 +137,86 @@ f name (map (attrib x) more_srcs) (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x; - -val have_theorems = - #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute PureThy.have_thmss; +fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x; -val have_lemmas = - #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute - (fn name => fn more_atts => PureThy.have_thmss name (more_atts @ [Drule.tag_lemma])); +fun local_have_thmss x = + gen_have_thmss (ProofContext.get_thms o Proof.context_of) + (Attrib.local_attribute o Proof.theory_of) x; + +fun have_thmss_i f ((name, more_atts), th_atts) = + f name more_atts (map (apfst single) th_atts); + +fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); -val have_thmss = - gen_have_thmss (ProofContext.get_thms o Proof.context_of) - (Attrib.local_attribute o Proof.theory_of) Proof.have_thmss; +fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs); +fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs); +val have_theorems = #1 oo global_have_thmss (PureThy.have_thmss o Some); +val have_theorems_i = #1 oo have_thmss_i (PureThy.have_thmss o Some); +val have_lemmas = #1 oo global_have_thmss (have_lemss o Some); +val have_lemmas_i = #1 oo have_thmss_i (have_lemss o Some); +val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss; +val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss; + -val have_facts = ProofHistory.apply o have_thmss; -val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", [])); +(* forward chaining *) + +val from_facts = + ProofHistory.apply o (Proof.chain oo curry (local_have_thmss Proof.have_thmss) ("", [])); + +val from_facts_i = + ProofHistory.apply o (Proof.chain oo curry (have_thmss_i Proof.have_thmss) ("", [])); + +val chain = ProofHistory.apply Proof.chain; (* context *) val fix = ProofHistory.apply o Proof.fix; - +val fix_i = ProofHistory.apply o Proof.fix_i; val match_bind = ProofHistory.apply o Proof.match_bind; +val match_bind_i = ProofHistory.apply o Proof.match_bind_i; (* statements *) -fun global_statement f name tags s thy = - ProofHistory.init (f name (map (Attrib.global_attribute thy) tags) s thy); +fun global_statement f name src s thy = + ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy); -fun local_statement f name tags s = ProofHistory.apply_open (fn state => - f name (map (Attrib.local_attribute (Proof.theory_of state)) tags) s state); +fun local_statement do_open f name src s = ProofHistory.apply_cond_open do_open (fn state => + f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s state); + +fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy); +fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t); val theorem = global_statement Proof.theorem; +val theorem_i = global_statement_i Proof.theorem_i; val lemma = global_statement Proof.lemma; -val assume = local_statement Proof.assume; -val show = local_statement Proof.show; -val have = local_statement Proof.have; - - -(* forward chaining *) - -val chain = ProofHistory.apply Proof.chain; +val lemma_i = global_statement_i Proof.lemma_i; +val assume = local_statement false Proof.assume; +val assume_i = local_statement_i false Proof.assume_i; +val show = local_statement true Proof.show; +val show_i = local_statement_i true Proof.show_i; +val have = local_statement true Proof.have; +val have_i = local_statement_i true Proof.have_i; (* end proof *) -fun qed_with (alt_name, alt_tags) prf = +fun gen_qed_with prep_att (alt_name, raw_atts) prf = let val state = ProofHistory.current prf; val thy = Proof.theory_of state; - val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags; + val alt_atts = apsome (map (prep_att thy)) raw_atts; val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state; val prt_result = Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm]; in Pretty.writeln prt_result; thy end; +val qed_with = gen_qed_with Attrib.global_attribute; +val qed_with_i = gen_qed_with (K I); + val qed = qed_with (None, None); val kill_proof = Proof.theory_of o ProofHistory.current; @@ -168,10 +231,14 @@ (* backward steps *) val tac = ProofHistory.applys o Method.tac; +val tac_i = tac o Method.Basic; val then_tac = ProofHistory.applys o Method.then_tac; +val then_tac_i = then_tac o Method.Basic; val proof = ProofHistory.applys o Method.proof; +val proof_i = proof o apsome Method.Basic; val end_block = ProofHistory.applys_close Method.end_block; val terminal_proof = ProofHistory.applys_close o Method.terminal_proof; +val terminal_proof_i = terminal_proof o Method.Basic; val immediate_proof = ProofHistory.applys_close Method.immediate_proof; val default_proof = ProofHistory.applys_close Method.default_proof; @@ -226,7 +293,7 @@ ("(" ^ quote name ^ ", " ^ txt ^ ")"); -(* theory init and exit *) (* FIXME move? rearrange? *) +(* theory init and exit *) (* FIXME move? rearrange? *) fun begin_theory name parents files = let