64 to prove a related statement about term lists simultaneously. For example, |
64 to prove a related statement about term lists simultaneously. For example, |
65 the fact that the identity substitution does not change a term needs to be |
65 the fact that the identity substitution does not change a term needs to be |
66 strengthened and proved as follows: |
66 strengthened and proved as follows: |
67 *} |
67 *} |
68 |
68 |
69 lemma "subst Var t = (t ::('v,'f)term) \<and> |
69 lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and> |
70 substs Var ts = (ts::('v,'f)term list)"; |
70 substs Var ts = (ts::('v,'f)term list)"; |
71 apply(induct_tac t and ts, simp_all); |
71 apply(induct_tac t and ts, simp_all); |
72 done |
72 done |
73 |
73 |
74 text{*\noindent |
74 text{*\noindent |
75 Note that @{term Var} is the identity substitution because by definition it |
75 Note that @{term Var} is the identity substitution because by definition it |
100 where @{term"map"} is the standard list function such that |
100 where @{term"map"} is the standard list function such that |
101 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
101 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
102 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
102 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
103 that the suggested equation holds: |
103 that the suggested equation holds: |
104 *} |
104 *} |
|
105 (*<*) |
|
106 (* Exercise 1: *) |
|
107 lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and> |
|
108 substs ((subst f) \<circ> g) ts = substs f (substs g ts)" |
|
109 apply (induct_tac t and ts) |
|
110 apply (simp_all) |
|
111 done |
|
112 |
|
113 (* Exercise 2: *) |
|
114 |
|
115 consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term" |
|
116 trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list" |
|
117 primrec |
|
118 "trev (Var v) = Var v" |
|
119 "trev (App f ts) = App f (trevs ts)" |
|
120 |
|
121 "trevs [] = []" |
|
122 "trevs (t#ts) = (trevs ts) @ [(trev t)]" |
|
123 |
|
124 lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" |
|
125 apply (induct_tac xs, auto) |
|
126 done |
|
127 |
|
128 lemma "trev (trev t) = (t::('v,'f)term) \<and> |
|
129 trevs (trevs ts) = (ts::('v,'f)term list)" |
|
130 apply (induct_tac t and ts, simp_all) |
|
131 done |
|
132 (*>*) |
105 |
133 |
106 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
134 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
107 apply(induct_tac ts, simp_all) |
135 apply(induct_tac ts, simp_all) |
108 done |
136 done |
109 |
137 |