578 \begin{minipage}{\textwidth} |
578 \begin{minipage}{\textwidth} |
579 \begin{isabelle} |
579 \begin{isabelle} |
580 \<close> |
580 \<close> |
581 ML %grayML\<open>fun chop_print params1 params2 prems1 prems2 ctxt = |
581 ML %grayML\<open>fun chop_print params1 params2 prems1 prems2 ctxt = |
582 let |
582 let |
583 val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), |
583 val pps = [Pretty.big_list "Params1 from the rule:" |
584 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
584 (map (pretty_cterm ctxt) params1), |
585 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
585 Pretty.big_list "Params2 from the predicate:" |
586 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
586 (map (pretty_cterm ctxt) params2), |
|
587 Pretty.big_list "Prems1 from the rule:" |
|
588 (map (pretty_thm ctxt) prems1), |
|
589 Pretty.big_list "Prems2 from the predicate:" |
|
590 (map (pretty_thm ctxt) prems2)] |
587 in |
591 in |
588 pps |> Pretty.chunks |
592 pps |> Pretty.chunks |
589 |> Pretty.string_of |
593 |> Pretty.string_of |
590 |> tracing |
594 |> tracing |
591 end\<close> |
595 end\<close> |
648 \<open>a, b, t\<close>\\ |
652 \<open>a, b, t\<close>\\ |
649 \<open>Params2 from the predicate:\<close>\\ |
653 \<open>Params2 from the predicate:\<close>\\ |
650 \<open>fresh\<close>\\ |
654 \<open>fresh\<close>\\ |
651 \<open>Prems1 from the rule:\<close>\\ |
655 \<open>Prems1 from the rule:\<close>\\ |
652 @{term "a \<noteq> b"}\\ |
656 @{term "a \<noteq> b"}\\ |
653 @{text [break] |
657 @{text "\<forall>fresh."}\\ |
654 "\<forall>fresh. |
658 @{text "(\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>"}\\ |
655 (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow> |
659 @{text "(\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>"}\\ |
656 (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow> |
660 @{text "(\<forall>a t. fresh a (Lam a t)) \<longrightarrow> "}\\ |
657 (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> |
661 @{text "(\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\ |
658 (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\ |
|
659 \<open>Prems2 from the predicate:\<close>\\ |
662 \<open>Prems2 from the predicate:\<close>\\ |
660 @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\ |
663 @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\ |
661 @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\ |
664 @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\ |
662 @{term "\<forall>a t. fresh a (Lam a t)"}\\ |
665 @{term "\<forall>a t. fresh a (Lam a t)"}\\ |
663 @{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"} |
666 @{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"} |
680 let |
683 let |
681 val cparams = map snd params |
684 val cparams = map snd params |
682 val (params1, params2) = chop (length cparams - length preds) cparams |
685 val (params1, params2) = chop (length cparams - length preds) cparams |
683 val (prems1, prems2) = chop (length prems - length rules) prems |
686 val (prems1, prems2) = chop (length prems - length rules) prems |
684 in |
687 in |
685 resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
688 resolve_tac context |
|
689 [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
686 end)\<close> |
690 end)\<close> |
687 |
691 |
688 text \<open> |
692 text \<open> |
689 The argument \<open>i\<close> corresponds to the number of the |
693 The argument \<open>i\<close> corresponds to the number of the |
690 introduction we want to prove. We will later on let it range |
694 introduction we want to prove. We will later on let it range |
753 let |
757 let |
754 val cparams = map snd params |
758 val cparams = map snd params |
755 val (params1, params2) = chop (length cparams - length preds) cparams |
759 val (params1, params2) = chop (length cparams - length preds) cparams |
756 val (prems1, prems2) = chop (length prems - length rules) prems |
760 val (prems1, prems2) = chop (length prems - length rules) prems |
757 in |
761 in |
758 resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
762 resolve_tac context |
|
763 [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
759 THEN EVERY1 (map (prepare_prem context params2 prems2) prems1) |
764 THEN EVERY1 (map (prepare_prem context params2 prems2) prems1) |
760 end)\<close> |
765 end)\<close> |
761 |
766 |
762 text \<open> |
767 text \<open> |
763 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. |
768 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore. |
852 let |
857 let |
853 val cparams = map snd params |
858 val cparams = map snd params |
854 val (params1, params2) = chop (length cparams - length preds) cparams |
859 val (params1, params2) = chop (length cparams - length preds) cparams |
855 val (prems1, prems2) = chop (length prems - length rules) prems |
860 val (prems1, prems2) = chop (length prems - length rules) prems |
856 in |
861 in |
857 resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
862 resolve_tac context |
|
863 [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 |
858 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
864 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) |
859 end)\<close> |
865 end)\<close> |
860 |
866 |
861 text \<open> |
867 text \<open> |
862 With these two functions we can now also prove the introduction |
868 With these two functions we can now also prove the introduction |