author  wenzelm 
Fri, 19 Jan 2007 22:08:08 +0100  
changeset 22101  6d13239d5f52 
parent 21879  a3efbae45735 
child 22846  fb79144af9a3 
permissions  rwrr 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

1 
(* Title: ZF/Tools/ind_cases.ML 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, LMU Muenchen 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

4 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

5 
Generic inductive cases facility for (co)inductive definitions. 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

6 
*) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

7 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

8 
signature IND_CASES = 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

9 
sig 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

10 
val declare: string > (simpset > cterm > thm) > theory > theory 
15703  11 
val inductive_cases: ((bstring * Attrib.src list) * string list) list > theory > theory 
18708  12 
val setup: theory > theory 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

13 
end; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

14 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

15 
structure IndCases: IND_CASES = 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

16 
struct 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

17 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

18 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

19 
(* theory data *) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

20 

16424  21 
structure IndCasesData = TheoryDataFun 
22 
(struct 

12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

23 
val name = "ZF/ind_cases"; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

24 
type T = (simpset > cterm > thm) Symtab.table; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

25 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

26 
val empty = Symtab.empty; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

27 
val copy = I; 
16424  28 
val extend = I; 
29 
fun merge _ tabs : T = Symtab.merge (K true) tabs; 

12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

30 
fun print _ _ = (); 
16424  31 
end); 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

32 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

33 

17412  34 
fun declare name f = IndCasesData.map (Symtab.update (name, f)); 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

35 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

36 
fun smart_cases thy ss read_prop s = 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

37 
let 
18678  38 
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); 
39 
val A = read_prop s handle ERROR msg => err msg; 

12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

40 
val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop 
18678  41 
(Logic.strip_imp_concl A)))))) handle TERM _ => err ""; 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

42 
in 
17412  43 
(case Symtab.lookup (IndCasesData.get thy) c of 
15531  44 
NONE => error ("Unknown inductive cases rule for set " ^ quote c) 
20342  45 
 SOME f => f ss (Thm.cterm_of thy A)) 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

46 
end; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

47 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

48 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

49 
(* inductive_cases command *) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

50 

12609  51 
fun inductive_cases args thy = 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

52 
let 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

53 
val read_prop = ProofContext.read_prop (ProofContext.init thy); 
12609  54 
val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop; 
55 
val facts = args > map (fn ((name, srcs), props) => 

18728  56 
((name, map (Attrib.attribute thy) srcs), 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12716
diff
changeset

57 
map (Thm.no_attributes o single o mk_cases) props)); 
20916  58 
in thy > PureThy.note_thmss_i "" facts > snd end; 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

59 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

60 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

61 
(* ind_cases method *) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

62 

21879  63 
fun mk_cases_meth (props, ctxt) = 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

64 
props 
15032  65 
> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

66 
(ProofContext.read_prop ctxt)) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

67 
> Method.erule 0; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

68 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

69 
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

70 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

71 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

72 
(* package setup *) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

73 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

74 
val setup = 
18708  75 
(IndCasesData.init #> 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

76 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
18708  77 
"dynamic case analysis on sets")]); 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

78 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

79 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

80 
(* outer syntax *) 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

81 

17057  82 
local structure P = OuterParse and K = OuterKeyword in 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

83 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

84 
val ind_cases = 
22101  85 
P.and_list1 (SpecParse.opt_thm_name ":"  Scan.repeat1 P.prop) 
12174
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

86 
>> (Toplevel.theory o inductive_cases); 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

87 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

88 
val inductive_casesP = 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

89 
OuterSyntax.command "inductive_cases" 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

90 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

91 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

92 
val _ = OuterSyntax.add_parsers [inductive_casesP]; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

93 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

94 
end; 
a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

95 

a0aab0b9f2e9
Generic inductive cases facility for (co)inductive definitions.
wenzelm
parents:
diff
changeset

96 
end; 
15705  97 