# HG changeset patch
# User paulson
# Date 973243473 -3600
# Node ID 99bd3e902979bb5426d69c127ed93295811ddaff
# Parent  5f5c1c0aba1c3e4b444845607f9b60ad4a5d2c64
advanced induction examples

diff -r 5f5c1c0aba1c -r 99bd3e902979 doc-src/TutorialI/Inductive/Advanced.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Fri Nov 03 10:24:33 2000 +0100
@@ -0,0 +1,48 @@
+(* ID:         $Id$ *)
+theory Advanced = Main:
+
+datatype 'f "term" = Apply 'f "'f term list"
+
+consts terms :: "'f set \<Rightarrow> 'f term set"
+inductive "terms F"
+intros
+step[intro]: "\<lbrakk>\<forall>t \<in> set term_list. t \<in> terms F;  f \<in> F\<rbrakk>
+              \<Longrightarrow> (Apply f term_list) \<in> terms F"
+
+
+lemma "F\<subseteq>G \<Longrightarrow> terms F \<subseteq> terms G"
+apply clarify
+apply (erule terms.induct)
+apply blast
+done
+
+consts term_type :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
+inductive "term_type sig"
+intros
+step[intro]: "\<lbrakk>\<forall>et \<in> set term_type_list. et \<in> term_type sig; 
+               sig f = (map snd term_type_list, rtype)\<rbrakk>
+              \<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type sig"
+
+consts term_type' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f term * 't)set"
+inductive "term_type' sig"
+intros
+step[intro]: "\<lbrakk>term_type_list \<in> lists(term_type' sig); 
+                 sig f = (map snd term_type_list, rtype)\<rbrakk>
+              \<Longrightarrow> (Apply f (map fst term_type_list), rtype) \<in> term_type' sig"
+monos lists_mono
+
+
+lemma "term_type sig \<subseteq> term_type' sig"
+apply clarify
+apply (erule term_type.induct)
+apply auto
+done
+
+lemma "term_type' sig \<subseteq> term_type sig"
+apply clarify
+apply (erule term_type'.induct)
+apply auto
+done
+
+end
+