doc-src/TutorialI/Inductive/Advanced.thy

tuned;

(* ID:         $Id$ *)
theory Advanced = Even:

text{* We completely forgot about "rule inversion", or whatever we may want
to call it. Just as a demo I include the two forms that Markus has made available. First the one for binding the result to a name *}

inductive_cases even_cases [elim!]:
  "Suc(Suc n) \<in> even"

thm even_cases;

text{*and now the one for local usage:*}

lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even";
by(ind_cases "Suc(Suc n) \<in> even");

text{*Both forms accept lists of strings.

Hope you can find some more exciting examples, although these may do
*}


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