equal
deleted
inserted
replaced
4 The nominal induct proof method. |
4 The nominal induct proof method. |
5 *) |
5 *) |
6 |
6 |
7 structure NominalInduct: |
7 structure NominalInduct: |
8 sig |
8 sig |
9 val nominal_induct_tac: Proof.context -> (string option * term) option list list -> |
9 val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list -> |
10 (string * typ) list -> (string * typ) list list -> thm list -> |
10 (string * typ) list -> (string * typ) list list -> thm list -> |
11 thm list -> int -> RuleCases.cases_tactic |
11 thm list -> int -> RuleCases.cases_tactic |
12 val nominal_induct_method: Method.src -> Proof.context -> Method.method |
12 val nominal_induct_method: Method.src -> Proof.context -> Method.method |
13 end = |
13 end = |
14 struct |
14 struct |
29 |
29 |
30 (* prepare rule *) |
30 (* prepare rule *) |
31 |
31 |
32 fun inst_mutual_rule ctxt insts avoiding rules = |
32 fun inst_mutual_rule ctxt insts avoiding rules = |
33 let |
33 let |
34 |
|
35 val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules; |
34 val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules; |
36 val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule); |
35 val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule); |
37 val (cases, consumes) = RuleCases.get joined_rule; |
36 val (cases, consumes) = RuleCases.get joined_rule; |
38 |
37 |
39 val l = length rules; |
38 val l = length rules; |
130 val ruleN = "rule"; |
129 val ruleN = "rule"; |
131 |
130 |
132 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
131 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
133 |
132 |
134 val def_inst = |
133 val def_inst = |
135 ((Scan.lift (Args.name --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME) |
134 ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME) |
136 -- Args.term) >> SOME || |
135 -- Args.term) >> SOME || |
137 inst >> Option.map (pair NONE); |
136 inst >> Option.map (pair NONE); |
138 |
137 |
139 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
138 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => |
140 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); |
139 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); |