64 val fix_i: (string list * typ option) list -> state -> state |
64 val fix_i: (string list * typ option) list -> state -> state |
65 val norm_hhf_tac: int -> tactic |
65 val norm_hhf_tac: int -> tactic |
66 val hard_asm_tac: int -> tactic |
66 val hard_asm_tac: int -> tactic |
67 val soft_asm_tac: int -> tactic |
67 val soft_asm_tac: int -> tactic |
68 val assm: ProofContext.exporter |
68 val assm: ProofContext.exporter |
69 -> (string * context attribute list * (string * (string list * string list)) list) list |
69 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
70 -> state -> state |
70 -> state -> state |
71 val assm_i: ProofContext.exporter |
71 val assm_i: ProofContext.exporter |
72 -> (string * context attribute list * (term * (term list * term list)) list) list |
72 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
73 -> state -> state |
73 -> state -> state |
74 val assume: (string * context attribute list * (string * (string list * string list)) list) list |
74 val assume: |
|
75 ((string * context attribute list) * (string * (string list * string list)) list) list |
75 -> state -> state |
76 -> state -> state |
76 val assume_i: (string * context attribute list * (term * (term list * term list)) list) list |
77 val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list |
77 -> state -> state |
78 -> state -> state |
78 val presume: (string * context attribute list * (string * (string list * string list)) list) list |
79 val presume: |
|
80 ((string * context attribute list) * (string * (string list * string list)) list) list |
79 -> state -> state |
81 -> state -> state |
80 val presume_i: (string * context attribute list * (term * (term list * term list)) list) list |
82 val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list |
81 -> state -> state |
83 -> state -> state |
82 val invoke_case: string * context attribute list -> state -> state |
84 val invoke_case: string * context attribute list -> state -> state |
83 val theorem: bstring -> theory attribute list -> string * (string list * string list) |
85 val theorem: bstring -> theory attribute list -> string * (string list * string list) |
84 -> theory -> state |
86 -> theory -> state |
85 val theorem_i: bstring -> theory attribute list -> term * (term list * term list) |
87 val theorem_i: bstring -> theory attribute list -> term * (term list * term list) |
553 val (vars, props) = get_case state name; |
555 val (vars, props) = get_case state name; |
554 val bind_skolem = ProofContext.bind_skolem (context_of state) (map #1 vars); |
556 val bind_skolem = ProofContext.bind_skolem (context_of state) (map #1 vars); |
555 in |
557 in |
556 state |
558 state |
557 |> fix_i (map (fn (x, T) => ([x], Some T)) vars) |
559 |> fix_i (map (fn (x, T) => ([x], Some T)) vars) |
558 |> assume_i [(name, atts, map (fn t => (t, ([], []))) (map bind_skolem props))] |
560 |> assume_i [((name, atts), map (fn t => (t, ([], []))) (map bind_skolem props))] |
559 end; |
561 end; |
560 |
562 |
561 |
563 |
562 |
564 |
563 (** goals **) |
565 (** goals **) |
580 |
582 |
581 val antN = "antecedent"; |
583 val antN = "antecedent"; |
582 |
584 |
583 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state = |
585 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state = |
584 let |
586 let |
585 val (state', (prop, gen_binds)) = |
587 val (state', ([[prop]], gen_binds)) = |
586 state |
588 state |
587 |> assert_forward_or_chain |
589 |> assert_forward_or_chain |
588 |> enter_forward |
590 |> enter_forward |
589 |> opt_block |
591 |> opt_block |
590 |> map_context_result (fn ct => prepp (ct, raw_propp)); |
592 |> map_context_result (fn ct => prepp (ct, [[raw_propp]])); |
591 val cprop = Thm.cterm_of (sign_of state') prop; |
593 val cprop = Thm.cterm_of (sign_of state') prop; |
592 val goal = Drule.mk_triv_goal cprop; |
594 val goal = Drule.mk_triv_goal cprop; |
593 in |
595 in |
594 state' |
596 state' |
595 |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds)) |
597 |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds)) |