135 *} |
135 *} |
136 |
136 |
137 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy = |
137 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy = |
138 let |
138 let |
139 val thy = ProofContext.theory_of lthy |
139 val thy = ProofContext.theory_of lthy |
140 val orules = map (ObjectLogic.atomize_term thy) rules |
140 val orules = map (Object_Logic.atomize_term thy) rules |
141 val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) |
141 val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) |
142 in |
142 in |
143 fold_map make_defn (prednames ~~ mxs ~~ defs) lthy |
143 fold_map make_defn (prednames ~~ mxs ~~ defs) lthy |
144 end*} |
144 end*} |
145 |
145 |
148 meta-quanti\-fications. In Line 4, we transform these introduction rules |
148 meta-quanti\-fications. In Line 4, we transform these introduction rules |
149 into the object logic (since definitions cannot be stated with |
149 into the object logic (since definitions cannot be stated with |
150 meta-connectives). To do this transformation we have to obtain the theory |
150 meta-connectives). To do this transformation we have to obtain the theory |
151 behind the local theory using the function @{ML_ind theory_of in ProofContext} |
151 behind the local theory using the function @{ML_ind theory_of in ProofContext} |
152 (Line 3); with this theory we can use the function |
152 (Line 3); with this theory we can use the function |
153 @{ML_ind atomize_term in ObjectLogic} to make the transformation (Line 4). The call |
153 @{ML_ind atomize_term in Object_Logic} to make the transformation (Line 4). The call |
154 to @{ML defn_aux} in Line 5 produces all right-hand sides of the |
154 to @{ML defn_aux} in Line 5 produces all right-hand sides of the |
155 definitions. The actual definitions are then made in Line 7. The result of |
155 definitions. The actual definitions are then made in Line 7. The result of |
156 the function is a list of theorems and a local theory (the theorems are |
156 the function is a list of theorems and a local theory (the theorems are |
157 registered with the local theory). A testcase for this function is |
157 registered with the local theory). A testcase for this function is |
158 *} |
158 *} |
252 The complete tactic for proving the induction principles can now |
252 The complete tactic for proving the induction principles can now |
253 be implemented as follows: |
253 be implemented as follows: |
254 *} |
254 *} |
255 |
255 |
256 ML %linenosgray{*fun ind_tac defs prem insts = |
256 ML %linenosgray{*fun ind_tac defs prem insts = |
257 EVERY1 [ObjectLogic.full_atomize_tac, |
257 EVERY1 [Object_Logic.full_atomize_tac, |
258 cut_facts_tac prem, |
258 cut_facts_tac prem, |
259 rewrite_goal_tac defs, |
259 rewrite_goal_tac defs, |
260 inst_spec_tac insts, |
260 inst_spec_tac insts, |
261 assume_tac]*} |
261 assume_tac]*} |
262 |
262 |
538 and then introduce quantifiers and implications. For this we |
538 and then introduce quantifiers and implications. For this we |
539 will use the tactic |
539 will use the tactic |
540 *} |
540 *} |
541 |
541 |
542 ML %linenosgray{*fun expand_tac defs = |
542 ML %linenosgray{*fun expand_tac defs = |
543 ObjectLogic.rulify_tac 1 |
543 Object_Logic.rulify_tac 1 |
544 THEN rewrite_goal_tac defs 1 |
544 THEN rewrite_goal_tac defs 1 |
545 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} |
545 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *} |
546 |
546 |
547 text {* |
547 text {* |
548 The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} |
548 The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better} |
677 |
677 |
678 @{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"} |
678 @{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"} |
679 |
679 |
680 To use this premise with @{ML rtac}, we need to instantiate its |
680 To use this premise with @{ML rtac}, we need to instantiate its |
681 quantifiers (with @{text params1}) and transform it into rule |
681 quantifiers (with @{text params1}) and transform it into rule |
682 format (using @{ML_ind rulify in ObjectLogic}). So we can modify the |
682 format (using @{ML_ind rulify in Object_Logic}). So we can modify the |
683 code as follows: |
683 code as follows: |
684 *} |
684 *} |
685 |
685 |
686 ML %linenosgray{*fun apply_prem_tac i preds rules = |
686 ML %linenosgray{*fun apply_prem_tac i preds rules = |
687 Subgoal.FOCUS (fn {params, prems, context, ...} => |
687 Subgoal.FOCUS (fn {params, prems, context, ...} => |
688 let |
688 let |
689 val cparams = map snd params |
689 val cparams = map snd params |
690 val (params1, params2) = chop (length cparams - length preds) cparams |
690 val (params1, params2) = chop (length cparams - length preds) cparams |
691 val (prems1, prems2) = chop (length prems - length rules) prems |
691 val (prems1, prems2) = chop (length prems - length rules) prems |
692 in |
692 in |
693 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
693 rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 |
694 end) *} |
694 end) *} |
695 |
695 |
696 text {* |
696 text {* |
697 The argument @{text i} corresponds to the number of the |
697 The argument @{text i} corresponds to the number of the |
698 introduction we want to prove. We will later on let it range |
698 introduction we want to prove. We will later on let it range |
761 let |
761 let |
762 val cparams = map snd params |
762 val cparams = map snd params |
763 val (params1, params2) = chop (length cparams - length preds) cparams |
763 val (params1, params2) = chop (length cparams - length preds) cparams |
764 val (prems1, prems2) = chop (length prems - length rules) prems |
764 val (prems1, prems2) = chop (length prems - length rules) prems |
765 in |
765 in |
766 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
766 rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 |
767 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
767 THEN EVERY1 (map (prepare_prem params2 prems2) prems1) |
768 end) *} |
768 end) *} |
769 |
769 |
770 text {* |
770 text {* |
771 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. |
771 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. |
859 let |
859 let |
860 val cparams = map snd params |
860 val cparams = map snd params |
861 val (params1, params2) = chop (length cparams - length preds) cparams |
861 val (params1, params2) = chop (length cparams - length preds) cparams |
862 val (prems1, prems2) = chop (length prems - length rules) prems |
862 val (prems1, prems2) = chop (length prems - length rules) prems |
863 in |
863 in |
864 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
864 rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 |
865 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
865 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
866 end) *} |
866 end) *} |
867 |
867 |
868 text {* |
868 text {* |
869 With these two functions we can now also prove the introduction |
869 With these two functions we can now also prove the introduction |
880 Finally we need two functions that string everything together. The first |
880 Finally we need two functions that string everything together. The first |
881 function is the tactic that performs the proofs. |
881 function is the tactic that performs the proofs. |
882 *} |
882 *} |
883 |
883 |
884 ML %linenosgray{*fun intro_tac defs rules preds i ctxt = |
884 ML %linenosgray{*fun intro_tac defs rules preds i ctxt = |
885 EVERY1 [ObjectLogic.rulify_tac, |
885 EVERY1 [Object_Logic.rulify_tac, |
886 rewrite_goal_tac defs, |
886 rewrite_goal_tac defs, |
887 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), |
887 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]), |
888 prove_intro_tac i preds rules ctxt]*} |
888 prove_intro_tac i preds rules ctxt]*} |
889 |
889 |
890 text {* |
890 text {* |