equal
deleted
inserted
replaced
28 fun declare name f = IndCasesData.map (Symtab.update (name, f)); |
28 fun declare name f = IndCasesData.map (Symtab.update (name, f)); |
29 |
29 |
30 fun smart_cases ctxt s = |
30 fun smart_cases ctxt s = |
31 let |
31 let |
32 val thy = Proof_Context.theory_of ctxt; |
32 val thy = Proof_Context.theory_of ctxt; |
|
33 |
33 fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); |
34 fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); |
34 val A = Syntax.read_prop ctxt s handle ERROR msg => err msg; |
35 val A = Syntax.read_prop ctxt s handle ERROR msg => err msg; |
35 val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop |
36 val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop |
36 (Logic.strip_imp_concl A)))))) handle TERM _ => err ""; |
37 (Logic.strip_imp_concl A)))))) handle TERM _ => err ""; |
37 in |
38 in |
38 (case Symtab.lookup (IndCasesData.get thy) c of |
39 (case Symtab.lookup (IndCasesData.get thy) c of |
39 NONE => error ("Unknown inductive cases rule for set " ^ quote c) |
40 NONE => error ("Unknown inductive cases rule for set " ^ quote c) |
40 | SOME f => f ctxt (Thm.global_cterm_of thy A)) |
41 | SOME f => f ctxt (Thm.cterm_of ctxt A)) |
41 end; |
42 end; |
42 |
43 |
43 |
44 |
44 (* inductive_cases command *) |
45 (* inductive_cases command *) |
45 |
46 |