# HG changeset patch # User wenzelm # Date 1003185274 -7200 # Node ID 5f0ab6f5c280f64995ddc03f9328e0359fb12cd4 # Parent 311eee3d63b64891a69f9815a394b707f5ac7c4d support impromptu terminology of cases parameters; diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 16 00:33:22 2001 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Oct 16 00:34:34 2001 +0200 @@ -363,9 +363,13 @@ (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment) >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind))); +val case_spec = + (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.underscore >> K None || P.name >> Some) + --| P.$$$ ")") || P.xname >> rpair []) -- P.opt_attribs >> P.triple1; + val caseP = OuterSyntax.command "case" "invoke local context" K.prf_asm - (P.xthm -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case))); + (case_spec -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case))); (* proof structure *) diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Tue Oct 16 00:33:22 2001 +0200 +++ b/src/Pure/Isar/isar_thy.ML Tue Oct 16 00:34:34 2001 +0200 @@ -87,8 +87,9 @@ val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T - val invoke_case_i: (string * Proof.context attribute list) * Comment.text + val invoke_case: (string * string option list * Args.src list) * Comment.text + -> ProofHistory.T -> ProofHistory.T + val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text -> ProofHistory.T -> ProofHistory.T val theorem: string -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text -> bool -> theory -> ProofHistory.T @@ -342,8 +343,8 @@ val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore; val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore; -fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state => - Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state); +fun invoke_case ((name, xs, src), comment_ignore) = ProofHistory.apply (fn state => + Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state); val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore; diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Oct 16 00:33:22 2001 +0200 +++ b/src/Pure/Isar/proof.ML Tue Oct 16 00:34:34 2001 +0200 @@ -80,7 +80,7 @@ -> state -> state val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list -> state -> state - val invoke_case: string * context attribute list -> state -> state + val invoke_case: string * string option list * context attribute list -> state -> state val theorem: string -> bstring -> theory attribute list -> string * (string list * string list) -> theory -> state val theorem_i: string -> bstring -> theory attribute list -> term * (term list * term list) @@ -549,10 +549,10 @@ (* invoke_case *) -fun invoke_case (name, atts) state = +fun invoke_case (name, xs, atts) state = let val (state', (lets, asms)) = - map_context_result (ProofContext.apply_case (get_case state name)) state; + map_context_result (ProofContext.apply_case (get_case state name xs)) state; in state' |> add_binds_i lets diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 16 00:33:22 2001 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Oct 16 00:34:34 2001 +0200 @@ -88,7 +88,7 @@ val fix: (string list * string option) list -> context -> context val fix_i: (string list * typ option) list -> context -> context val bind_skolem: context -> string list -> term -> term - val get_case: context -> string -> RuleCases.T + val get_case: context -> string -> string option list -> RuleCases.T val add_cases: (string * RuleCases.T) list -> context -> context val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list) val show_hyps: bool ref @@ -953,16 +953,22 @@ (** cases **) -fun check_case ctxt name {fixes, assumes, binds} = - if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso - null (foldr Term.add_term_vars (assumes, [])) then - {fixes = fixes, assumes = assumes, binds = map drop_schematic binds} - else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt); +fun prep_case ctxt name xs {fixes, assumes, binds} = + let + fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys + | replace [] ys = ys + | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); + in + if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso + null (foldr Term.add_term_vars (assumes, [])) then + {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds} + else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) + end; -fun get_case (ctxt as Context {cases, ...}) name = +fun get_case (ctxt as Context {cases, ...}) name xs = (case assoc (cases, name) of None => raise CONTEXT ("Unknown case: " ^ quote name, ctxt) - | Some c => check_case ctxt name c); + | Some c => prep_case ctxt name xs c); fun add_cases xs = map_context (fn (thy, data, asms, binds, thms, cases, defs) =>