equal
deleted
inserted
replaced
40 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
40 (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp) |
41 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
41 intrs' (list_comb (pred, zs)))))) #>> snd #>> snd |
42 end) (preds_syn ~~ preds ~~ Tss) lthy; |
42 end) (preds_syn ~~ preds ~~ Tss) lthy; |
43 |
43 |
44 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
44 val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1; |
45 |
45 |
46 |
46 |
47 (* proving the induction rules *) |
47 (* proving the induction rules *) |
48 |
48 (* @chunk induction_rules *) |
49 val (Pnames, lthy3) = |
49 val (Pnames, lthy3) = |
50 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
50 Variable.variant_fixes (replicate (length preds) "P") lthy2; |
51 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
51 val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) |
52 (Pnames ~~ Tss); |
52 (Pnames ~~ Tss); |
53 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
53 val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; |
74 [assume_tac 1])) |> |
74 [assume_tac 1])) |> |
75 singleton (ProofContext.export lthy4 lthy1) |
75 singleton (ProofContext.export lthy4 lthy1) |
76 end; |
76 end; |
77 |
77 |
78 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
78 val indrules = map prove_indrule (preds ~~ Ps ~~ Tss); |
79 |
79 (* @end *) |
80 |
80 |
81 (* proving the introduction rules *) |
81 (* proving the introduction rules *) |
82 |
82 (* @chunk intro_rules *) |
83 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
83 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
84 val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); |
84 val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); |
85 |
85 |
86 fun prove_intr (i, (_, r)) = |
86 fun prove_intr (i, (_, r)) = |
87 Goal.prove lthy2 [] [] r |
87 Goal.prove lthy2 [] [] r |
110 in rtac prem'' 1 end) ctxt' 1) prems1) |
110 in rtac prem'' 1 end) ctxt' 1) prems1) |
111 end) ctxt 1]) |> |
111 end) ctxt 1]) |> |
112 singleton (ProofContext.export lthy2 lthy1); |
112 singleton (ProofContext.export lthy2 lthy1); |
113 |
113 |
114 val intr_ths = map_index prove_intr intrs; |
114 val intr_ths = map_index prove_intr intrs; |
115 |
115 (* @end *) |
116 |
116 |
117 (* storing the theorems *) |
117 (* storing the theorems *) |
118 |
118 (* @chunk storing *) |
119 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn); |
119 val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn); |
120 val case_names = map (Binding.base_name o fst o fst) intrs |
120 val case_names = map (Binding.base_name o fst o fst) intrs |
|
121 (* @end *) |
121 in |
122 in |
122 lthy1 |> |
123 lthy1 |> |
123 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
124 LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
124 ((Binding.qualify mut_name a, atts), [([th], [])])) |
125 ((Binding.qualify mut_name a, atts), [([th], [])])) |
125 (intrs ~~ intr_ths)) |-> |
126 (intrs ~~ intr_ths)) |-> |
131 [Attrib.internal (K (RuleCases.case_names case_names)), |
132 [Attrib.internal (K (RuleCases.case_names case_names)), |
132 Attrib.internal (K (RuleCases.consumes 1)), |
133 Attrib.internal (K (RuleCases.consumes 1)), |
133 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
134 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
134 (preds_syn ~~ indrules)) #>> maps snd) |
135 (preds_syn ~~ indrules)) #>> maps snd) |
135 end; |
136 end; |
136 |
137 |
137 (* @chunk add_inductive *) |
138 (* @chunk add_inductive *) |
138 fun add_inductive preds_syn params_syn intro_srcs lthy = |
139 fun add_inductive preds_syn params_syn intro_srcs lthy = |
139 let |
140 let |
140 val ((vars, specs), _) = Specification.read_specification |
141 val ((vars, specs), _) = Specification.read_specification |
141 (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) |
142 (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) |