1 theory Ind_Code |
1 theory Ind_Code |
2 imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims |
2 imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims |
3 begin |
3 begin |
4 |
4 |
|
5 datatype trm = |
|
6 Var "string" |
|
7 | App "trm" "trm" |
|
8 | Lam "string" "trm" |
|
9 |
|
10 simple_inductive |
|
11 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100) |
|
12 where |
|
13 "a\<noteq>b \<Longrightarrow> a\<sharp>Var b" |
|
14 | "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s" |
|
15 | "a\<sharp>Lam a t" |
|
16 | "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t" |
|
17 |
|
18 |
5 section {* Code *} |
19 section {* Code *} |
6 |
20 |
7 text {* |
21 text {* |
|
22 |
8 @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
23 @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"} |
9 |
24 |
10 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
25 @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"} |
11 |
26 |
12 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
27 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"} |
531 ML {* prems_of *} |
546 ML {* prems_of *} |
532 ML {* Logic.strip_params *} |
547 ML {* Logic.strip_params *} |
533 ML {* Logic.strip_assums_hyp *} |
548 ML {* Logic.strip_assums_hyp *} |
534 |
549 |
535 ML {* |
550 ML {* |
536 fun chop_print_tac ctxt thm = |
551 fun chop_print_tac m n ctxt thm = |
537 let |
552 let |
538 val [trm] = prems_of thm |
553 val [trm] = prems_of thm |
539 val params = map fst (Logic.strip_params trm) |
554 val params = map fst (Logic.strip_params trm) |
540 val prems = Logic.strip_assums_hyp trm |
555 val prems = Logic.strip_assums_hyp trm |
541 val (prems1, prems2) = chop (length prems - 3) prems; |
556 val (prems1, prems2) = chop (length prems - m) prems; |
542 val (params1, params2) = chop (length params - 2) params; |
557 val (params1, params2) = chop (length params - n) params; |
543 val _ = warning (Syntax.string_of_term ctxt trm) |
558 val _ = warning (Syntax.string_of_term ctxt trm) |
544 val _ = warning (commas params) |
559 val _ = warning (commas params) |
545 val _ = warning (commas (map (Syntax.string_of_term ctxt) prems)) |
560 val _ = warning (commas (map (Syntax.string_of_term ctxt) prems)) |
546 val _ = warning ((commas params1) ^ " | " ^ (commas params2)) |
561 val _ = warning ((commas params1) ^ " | " ^ (commas params2)) |
547 val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^ |
562 val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^ |
549 in |
564 in |
550 Seq.single thm |
565 Seq.single thm |
551 end |
566 end |
552 *} |
567 *} |
553 |
568 |
|
569 ML {* METAHYPS *} |
|
570 |
|
571 ML {* |
|
572 fun chop_print_tac2 ctxt prems = |
|
573 let |
|
574 val _ = warning (commas (map (str_of_thm ctxt) prems)) |
|
575 in |
|
576 all_tac |
|
577 end |
|
578 *} |
554 |
579 |
555 lemma intro1: |
580 lemma intro1: |
556 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)" |
581 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)" |
557 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
582 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
558 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *}) |
583 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *}) |
559 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
584 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
560 apply(tactic {* chop_print_tac @{context} *}) |
585 apply(tactic {* chop_print_tac 3 2 @{context} *}) |
561 oops |
586 oops |
|
587 |
|
588 ML {* |
|
589 fun SUBPROOF_test tac ctxt = |
|
590 SUBPROOF (fn {params, prems, context,...} => |
|
591 let |
|
592 val thy = ProofContext.theory_of context |
|
593 in |
|
594 tac (params, prems, context) |
|
595 THEN Method.insert_tac prems 1 |
|
596 THEN print_tac "SUBPROOF Test" |
|
597 THEN SkipProof.cheat_tac thy |
|
598 end) ctxt 1 |
|
599 *} |
|
600 |
|
601 |
|
602 |
|
603 |
|
604 lemma fresh_App: |
|
605 shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s" |
|
606 apply(tactic {* ObjectLogic.rulify_tac 1 *}) |
|
607 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *}) |
|
608 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *}) |
|
609 oops |
|
610 (* |
|
611 apply(tactic {* SUBPROOF_test |
|
612 (fn (params, prems, ctxt) => |
|
613 let |
|
614 val (prems1, prems2) = chop (length prems - 4) prems; |
|
615 val (params1, params2) = chop (length params - 1) params; |
|
616 in |
|
617 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1 |
|
618 end) @{context} *}) |
|
619 *) |
562 |
620 |
563 ML{*fun subproof2 prem params2 prems2 = |
621 ML{*fun subproof2 prem params2 prems2 = |
564 SUBPROOF (fn {prems, ...} => |
622 SUBPROOF (fn {prems, ...} => |
565 let |
623 let |
566 val prem' = prems MRS prem; |
624 val prem' = prems MRS prem; |