equal
deleted
inserted
replaced
47 (* @end *) |
47 (* @end *) |
48 |
48 |
49 (* @chunk definitions *) |
49 (* @chunk definitions *) |
50 fun definitions rules params preds prednames syns arg_typess lthy = |
50 fun definitions rules params preds prednames syns arg_typess lthy = |
51 let |
51 let |
52 val thy = ProofContext.theory_of lthy |
52 val thy = Proof_Context.theory_of lthy |
53 val orules = map (Object_Logic.atomize_term thy) rules |
53 val orules = map (Object_Logic.atomize_term thy) rules |
54 val defs = |
54 val defs = |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
56 in |
56 in |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
76 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
76 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
77 |
77 |
78 val Ps = replicate (length preds) "P" |
78 val Ps = replicate (length preds) "P" |
79 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
79 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
80 |
80 |
81 val thy = ProofContext.theory_of lthy3 |
81 val thy = Proof_Context.theory_of lthy3 |
82 |
82 |
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
84 val newpreds = map Free (newprednames ~~ Tss') |
84 val newpreds = map Free (newprednames ~~ Tss') |
85 val cnewpreds = map (cterm_of thy) newpreds |
85 val cnewpreds = map (cterm_of thy) newpreds |
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
95 val goal = Logic.list_implies |
95 val goal = Logic.list_implies |
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
97 in |
97 in |
98 Goal.prove lthy4 [] [prem] goal |
98 Goal.prove lthy4 [] [prem] goal |
99 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
99 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
100 |> singleton (ProofContext.export lthy4 lthy1) |
100 |> singleton (Proof_Context.export lthy4 lthy1) |
101 end |
101 end |
102 in |
102 in |
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
104 end |
104 end |
105 (* @end *) |
105 (* @end *) |
150 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
150 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
151 |
151 |
152 fun prove_intro (i, goal) = |
152 fun prove_intro (i, goal) = |
153 Goal.prove lthy2 [] [] goal |
153 Goal.prove lthy2 [] [] goal |
154 (fn {context, ...} => introductions_tac defs rules preds i context) |
154 (fn {context, ...} => introductions_tac defs rules preds i context) |
155 |> singleton (ProofContext.export lthy2 lthy1) |
155 |> singleton (Proof_Context.export lthy2 lthy1) |
156 in |
156 in |
157 map_index prove_intro rules |
157 map_index prove_intro rules |
158 end |
158 end |
159 (* @end *) |
159 (* @end *) |
160 |
160 |