author | Christian Urban <urbanc@in.tum.de> |
Fri, 13 Mar 2009 16:57:16 +0100 | |
changeset 176 | 3da5f3f07d8b |
parent 173 | d820cb5873ea |
child 177 | 4e2341f6599d |
permissions | -rw-r--r-- |
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Ind_Code |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
2 |
imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims |
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
5 |
section {* Code *} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
6 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
7 |
subsection {* Definitions *} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
8 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
9 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
10 |
If we give it a term and a constant name, it will define the |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
11 |
constant as the term. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
12 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
13 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
14 |
ML{*fun make_defs ((binding, syn), trm) lthy = |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
15 |
let |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
16 |
val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
17 |
val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
18 |
in |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
19 |
(thm, lthy') |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
20 |
end*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
21 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
22 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
23 |
Returns the definition and the local theory in which this definition has |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
24 |
been made. The @{ML internalK in Thm} is just a flag attached to the |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
25 |
theorem (others flags are @{ML definitionK in Thm} or @{ML axiomK in Thm}). |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
26 |
These flags just classify theorems and have no significant meaning, except |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
27 |
for tools such as finding theorems in the theorem database. |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
28 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
29 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
30 |
local_setup {* |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
31 |
fn lthy => |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
32 |
let |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
33 |
val (def, lthy') = make_defs ((Binding.name "MyTrue", NoSyn), @{term True}) lthy |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
34 |
val _ = warning (str_of_thm lthy' def) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
35 |
in |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
36 |
lthy' |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
37 |
end |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
38 |
*} |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
39 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
40 |
text {* |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
41 |
Prints out the theorem @{prop "MyTrue \<equiv> True"}. |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
42 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
43 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
44 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
45 |
Constructs the term for the definition: the main arguments are a predicate |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
46 |
and the types of the arguments, it also expects orules which are the |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
47 |
intro rules in the object logic; preds which are all predicates. returns the |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
48 |
term. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
49 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
50 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
51 |
ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) = |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
52 |
let |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
53 |
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
54 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
55 |
val fresh_args = |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
56 |
arg_tys |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
57 |
|> map (pair "z") |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
58 |
|> Variable.variant_frees lthy orules |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
59 |
|> map Free |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
60 |
in |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
61 |
list_comb (pred, fresh_args) |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
62 |
|> fold_rev (curry HOLogic.mk_imp) orules |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
63 |
|> fold_rev mk_all preds |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
64 |
|> fold_rev lambda fresh_args |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
65 |
end*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
66 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
67 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
68 |
The lines 5-9 produce fresh arguments with which the predicate can be applied. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
69 |
For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
70 |
generates variants for all these strings (names) so that they are unique w.r.t.~to |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
71 |
the intro rules; in Line 9 it generates the corresponding variable terms for these |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
72 |
unique names. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
73 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
74 |
The unique free variables are applied to the predicate (Line 11); then |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
75 |
the intro rules are attached as preconditions (Line 12); in Line 13 we |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
76 |
quantify over all predicates; and in line 14 we just abstract over all |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
77 |
the (fresh) arguments of the predicate. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
78 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
79 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
80 |
|
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
81 |
local_setup {* |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
82 |
fn lthy => |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
83 |
let |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
84 |
val orules = [@{prop "even 0"}, |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
85 |
@{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"}, |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
86 |
@{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] |
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
87 |
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
88 |
val pred = @{term "even::nat\<Rightarrow>bool"} |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
89 |
val arg_tys = [@{typ "nat"}] |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
90 |
val def = defs_aux lthy orules preds (pred, arg_tys) |
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
91 |
in |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
92 |
warning (Syntax.string_of_term lthy def); |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
93 |
lthy |
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
94 |
end*} |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
95 |
|
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
text {* |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
97 |
The arguments of the main function for the definitions are |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
98 |
the intro rules; the predicates and their names, their syntax |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
99 |
annotations and the argument types of each predicate. It |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
100 |
returns a theorem list (the definitions) and a local |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
101 |
theory where the definitions are made |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
102 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
103 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
104 |
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
105 |
let |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
106 |
val thy = ProofContext.theory_of lthy |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
107 |
val orules = map (ObjectLogic.atomize_term thy) rules |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
108 |
val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
109 |
in |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
110 |
fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
111 |
end*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
112 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
113 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
114 |
In line 4 we generate the intro rules in the object logic; for this we have to |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
115 |
obtain the theory behind the local theory (Line 3); with this we can |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
116 |
call @{ML defs_aux} to generate the terms for the left-hand sides. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
117 |
The actual definitions are made in Line 7. |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
118 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
119 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
120 |
subsection {* Induction Principles *} |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
121 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
122 |
text {* Recall the proof for the induction principle for @{term "even"}: *} |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
123 |
|
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
124 |
lemma |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
125 |
assumes prems: "even n" |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
126 |
shows "P 0 \<Longrightarrow> |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
127 |
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
128 |
apply(atomize (full)) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
129 |
apply(cut_tac prems) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
130 |
apply(unfold even_def) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
131 |
apply(drule spec[where x=P]) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
132 |
apply(drule spec[where x=Q]) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
133 |
apply(assumption) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
134 |
done |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
135 |
|
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
136 |
|
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
137 |
text {* We need to be able to instantiate universal quantifiers. *} |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
138 |
|
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
139 |
ML{*fun inst_spec ct = |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
140 |
Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
141 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
142 |
text {* |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
143 |
Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}. |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
144 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
145 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
146 |
text {* |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
147 |
Instantiates universal qantifications in the premises |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
148 |
*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
149 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
150 |
lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True" |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
151 |
apply (tactic {* |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
152 |
let |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
153 |
val ctrms = [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}] |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
154 |
in |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
155 |
EVERY1 (map (dtac o inst_spec) ctrms) |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
156 |
end *}) |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
157 |
txt {* \begin{minipage}{\textwidth} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
158 |
@{subgoals} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
159 |
\end{minipage}*} |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
160 |
(*<*)oops(*>*) |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
161 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
162 |
text {* |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
163 |
Now the tactic for proving the induction rules: |
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
124
diff
changeset
|
164 |
*} |
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
124
diff
changeset
|
165 |
|
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
166 |
ML{*fun induction_tac defs prems insts = |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
167 |
EVERY1 [ObjectLogic.full_atomize_tac, |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
168 |
cut_facts_tac prems, |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
169 |
K (rewrite_goals_tac defs), |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
170 |
EVERY' (map (dtac o inst_spec) insts), |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
171 |
assume_tac]*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
172 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
173 |
lemma |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
174 |
assumes prems: "even n" |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
175 |
shows "P 0 \<Longrightarrow> |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
176 |
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
177 |
apply(tactic {* |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
178 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
179 |
val defs = [@{thm even_def}, @{thm odd_def}] |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
180 |
val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
181 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
182 |
induction_tac defs @{thms prems} insts |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
183 |
end *}) |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
184 |
done |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
185 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
186 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
187 |
text {* |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
188 |
While the generic proof is relatively simple, it is a bit harder to |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
189 |
set up the goals for the induction principles. |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
190 |
*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
191 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
192 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
193 |
ML %linenosgray{*fun inductions rules defs preds tyss lthy1 = |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
194 |
let |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
195 |
val Ps = replicate (length preds) "P" |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
196 |
val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
197 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
198 |
val thy = ProofContext.theory_of lthy2 |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
199 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
200 |
val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
201 |
val newpreds = map Free (newprednames ~~ tyss') |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
202 |
val cnewpreds = map (cterm_of thy) newpreds |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
203 |
val rules' = map (subst_free (preds ~~ newpreds)) rules |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
204 |
|
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
205 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
206 |
fun prove_induction ((pred, newpred), tys) = |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
207 |
let |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
208 |
val zs = replicate (length tys) "z" |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
209 |
val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
210 |
val newargs = map Free (newargnames ~~ tys) |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
211 |
|
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
212 |
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
213 |
val goal = Logic.list_implies |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
214 |
(rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
215 |
in |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
216 |
Goal.prove lthy3 [] [prem] goal |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
217 |
(fn {prems, ...} => induction_tac defs prems cnewpreds) |
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
218 |
|> singleton (ProofContext.export lthy3 lthy1) |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
219 |
end |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
220 |
in |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
221 |
map prove_induction (preds ~~ newpreds ~~ tyss) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
222 |
end*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
223 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
224 |
ML {* |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
225 |
let |
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
226 |
val rules = [@{prop "even (0::nat)"}, |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
227 |
@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
228 |
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
229 |
val defs = [@{thm even_def}, @{thm odd_def}] |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
230 |
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
231 |
val tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
232 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
233 |
inductions rules defs preds tyss @{context} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
234 |
end |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
235 |
*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
236 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
237 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
238 |
subsection {* Introduction Rules *} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
239 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
240 |
ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
241 |
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
242 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
243 |
ML{*fun subproof2 prem params2 prems2 = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
244 |
SUBPROOF (fn {prems, ...} => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
245 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
246 |
val prem' = prems MRS prem; |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
247 |
val prem'' = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
248 |
case prop_of prem' of |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
249 |
_ $ (Const (@{const_name All}, _) $ _) => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
250 |
prem' |> all_elims params2 |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
251 |
|> imp_elims prems2 |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
252 |
| _ => prem'; |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
253 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
254 |
rtac prem'' 1 |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
255 |
end)*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
256 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
257 |
ML{*fun subproof1 rules preds i = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
258 |
SUBPROOF (fn {params, prems, context = ctxt', ...} => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
259 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
260 |
val (prems1, prems2) = chop (length prems - length rules) prems; |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
261 |
val (params1, params2) = chop (length params - length preds) params; |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
262 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
263 |
rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
264 |
THEN |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
265 |
EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
266 |
end)*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
267 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
268 |
ML{* |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
269 |
fun introductions_tac defs rules preds i ctxt = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
270 |
EVERY1 [ObjectLogic.rulify_tac, |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
271 |
K (rewrite_goals_tac defs), |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
272 |
REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
273 |
subproof1 rules preds i ctxt]*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
274 |
|
173
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
275 |
lemma evenS: |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
276 |
shows "odd m \<Longrightarrow> even (Suc m)" |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
277 |
apply(tactic {* |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
278 |
let |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
279 |
val rules = [@{prop "even (0::nat)"}, |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
280 |
@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"}, |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
281 |
@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
282 |
val defs = [@{thm even_def}, @{thm odd_def}] |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
283 |
val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
284 |
in |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
285 |
introductions_tac defs rules preds 1 @{context} |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
286 |
end *}) |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
287 |
done |
d820cb5873ea
used latex package boxedminipage
Christian Urban <urbanc@in.tum.de>
parents:
165
diff
changeset
|
288 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
289 |
ML{*fun introductions rules preds defs lthy = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
290 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
291 |
fun prove_intro (i, goal) = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
292 |
Goal.prove lthy [] [] goal |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
293 |
(fn {context, ...} => introductions_tac defs rules preds i context) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
294 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
295 |
map_index prove_intro rules |
164
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
296 |
end*} |
3f617d7a2691
more work on simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
163
diff
changeset
|
297 |
|
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
298 |
text {* main internal function *} |
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
299 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
300 |
ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
301 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
302 |
val syns = map snd pred_specs |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
303 |
val pred_specs' = map fst pred_specs |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
304 |
val prednames = map fst pred_specs' |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
305 |
val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs' |
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
parents:
124
diff
changeset
|
306 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
307 |
val tyss = map (binder_types o fastype_of) preds |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
308 |
val (attrs, rules) = split_list rule_specs |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
309 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
310 |
val (defs, lthy') = definitions rules preds prednames syns tyss lthy |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
311 |
val ind_rules = inductions rules defs preds tyss lthy' |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
312 |
val intro_rules = introductions rules preds defs lthy' |
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
313 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
314 |
val mut_name = space_implode "_" (map Binding.name_of prednames) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
315 |
val case_names = map (Binding.name_of o fst) attrs |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
316 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
317 |
lthy' |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
318 |
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
319 |
((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
320 |
|-> (fn intross => LocalTheory.note Thm.theoremK |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
321 |
((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
322 |
|>> snd |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
323 |
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
324 |
((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
325 |
[Attrib.internal (K (RuleCases.case_names case_names)), |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
326 |
Attrib.internal (K (RuleCases.consumes 1)), |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
327 |
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
328 |
(pred_specs ~~ ind_rules)) #>> maps snd) |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
329 |
|> snd |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
330 |
end*} |
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
331 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
332 |
ML{*fun read_specification' vars specs lthy = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
333 |
let |
176
3da5f3f07d8b
updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents:
173
diff
changeset
|
334 |
val specs' = map (fn (a, s) => (a, [s])) specs |
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
335 |
val ((varst, specst), _) = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
336 |
Specification.read_specification vars specs' lthy |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
337 |
val specst' = map (apsnd the_single) specst |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
338 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
339 |
(varst, specst') |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
340 |
end*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
341 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
342 |
ML{*fun add_inductive pred_specs rule_specs lthy = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
343 |
let |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
344 |
val (pred_specs', rule_specs') = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
345 |
read_specification' pred_specs rule_specs lthy |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
346 |
in |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
347 |
add_inductive_i pred_specs' rule_specs' lthy |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
348 |
end*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
349 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
350 |
ML{*val spec_parser = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
351 |
OuterParse.opt_target -- |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
352 |
OuterParse.fixes -- |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
353 |
Scan.optional |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
354 |
(OuterParse.$$$ "where" |-- |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
355 |
OuterParse.!!! |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
356 |
(OuterParse.enum1 "|" |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
357 |
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
358 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
359 |
ML{*val specification = |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
360 |
spec_parser >> |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
361 |
(fn ((loc, pred_specs), rule_specs) => |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
362 |
Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*} |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
363 |
|
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
364 |
ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
365 |
OuterKeyword.thy_decl specification*} |
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
366 |
|
124
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
367 |
text {* |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
368 |
Things to include at the end: |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
369 |
|
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
370 |
\begin{itemize} |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
371 |
\item say something about add-inductive-i to return |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
372 |
the rules |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
373 |
\item say that the induction principle is weaker (weaker than |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
374 |
what the standard inductive package generates) |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
375 |
\end{itemize} |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
376 |
|
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
377 |
*} |
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
378 |
|
165
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
379 |
simple_inductive |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
380 |
Even and Odd |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
381 |
where |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
382 |
Even0: "Even 0" |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
383 |
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)" |
890fbfef6d6b
partially adapted to new antiquotation infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
164
diff
changeset
|
384 |
| OddS: "Even n \<Longrightarrow> Odd (Suc n)" |
124
0b9fa606a746
added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents:
118
diff
changeset
|
385 |
|
91
667a0943c40b
added a section that will eventually describe the code
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
386 |
end |