src/HOL/Induct/Term.thy
 author wenzelm Sat, 07 Apr 2012 16:41:59 +0200 changeset 47389 e8552cba702d parent 46914 c2ca2c3d23a6 child 58249 180f1b3508ed permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
```
(*  Title:      HOL/Induct/Term.thy
Author:     Stefan Berghofer,  TU Muenchen
*)

header {* Terms over a given alphabet *}

theory Term
imports Main
begin

datatype ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"

text {* \medskip Substitution function on terms *}

primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
where
"subst_term f (Var a) = f a"
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
| "subst_term_list f [] = []"
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"

text {* \medskip A simple theorem about composition of substitutions *}

lemma subst_comp:
"subst_term (subst_term f1 \<circ> f2) t =
subst_term f1 (subst_term f2 t)"
and "subst_term_list (subst_term f1 \<circ> f2) ts =
subst_term_list f1 (subst_term_list f2 ts)"
by (induct t and ts) simp_all

text {* \medskip Alternative induction rule *}

lemma
assumes var: "!!v. P (Var v)"
and app: "!!f ts. (\<forall>t \<in> set ts. P t) ==> P (App f ts)"
shows term_induct2: "P t"
and "\<forall>t \<in> set ts. P t"
apply (induct t and ts)
apply (rule var)
apply (rule app)
apply assumption
apply simp_all
done

end
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.5025562,"math_prob":0.6707681,"size":1337,"snap":"2020-45-2020-50","text_gpt3_token_len":426,"char_repetition_ratio":0.20705177,"word_repetition_ratio":0.05357143,"special_character_ratio":0.35302916,"punctuation_ratio":0.13043478,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9802363,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-11-25T17:40:41Z\",\"WARC-Record-ID\":\"<urn:uuid:16ead88c-70ca-4920-b0ac-1459f883dfe3>\",\"Content-Length\":\"7818\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:a634c570-86a0-4c9f-a141-ff2a7471dc5d>\",\"WARC-Concurrent-To\":\"<urn:uuid:b39b83a8-c06b-4c5c-83ed-8a3ee7a4ba8f>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"https://isabelle.in.tum.de/repos/isabelle/file/e8552cba702d/src/HOL/Induct/Term.thy\",\"WARC-Payload-Digest\":\"sha1:UGDJM766CPYVDRMM6PGTO2R2RPD72BAQ\",\"WARC-Block-Digest\":\"sha1:B3D3GNUPTW7KGAMW3NU6OIMYAAFRTTCH\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-50/CC-MAIN-2020-50_segments_1606141183514.25_warc_CC-MAIN-20201125154647-20201125184647-00552.warc.gz\"}"}