Guten Abend, bin Studenten an der Goethe-Uni in Frankfurt und beschäftige mich sehr stark mit dem Isabelle Beweis-System.
Zur Zeit sitze ich an folgendem Problem in Isabelle. In dem Lemma "subst_no_occ" komme ich nicht weiter, ich vermute stark, dass ich in den Funktionen "apply_subst" und "occ" etwas wichtiges übersehen habe und im Beweis etwas verloren geht. primrec apply_subst_list :: "('a trm) list \Rightarrow 'a subst \Rightarrow ('a trm) list" and apply_subst :: "'a trm \Rightarrow 'a subst \Rightarrow 'a trm" (infixl "\triangleleft" 60) where "apply_subst_list [] s = []" | "apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)" | "(Var v) \triangleleft s = assoc v (Var v) s" | "(Fn f xs) \triangleleft s = (Fn f (apply_subst_list xs s))" primrec occ :: "'a trm \Rightarrow 'a trm \Rightarrow bool" and occ_list :: "'a trm \Rightarrow 'a trm list \Rightarrow bool" where "occ u (Var v) = False" | "occ u (Fn f xs) = (if (list_ex (eq u) xs) then True else (occ_list u xs))" | "occ_list u [] = False" | "occ_list u (x#xs) = (if occ u x then True else occ_list u xs)" lemma subst_no_occ: "\neg occ (Var v) t \Longrightarrow Var v \neq t \Longrightarrow t \triangleleft [(v,s)] = t" apply(induct t) apply(simp) apply(simp) apply(simp) apply(simp) done Liebe Grüße Anja Gerbes Good evening, I am student at Goethe University in Frankfurt and I am working with the Isabelle proof system. Currently I am sitting at the following problem in Isabelle. In the lemma "subst_no_occ" I get no further, I strongly suspect that I am in the functions"apply_subst" and "occ" have overlooked something important and something gets lost in the proof. primrec apply_subst_list :: "('a trm) list \Rightarrow 'a subst \Rightarrow ('a trm) list" and apply_subst :: "'a trm \Rightarrow 'a subst \Rightarrow 'a trm" (infixl "\triangleleft" 60) where "apply_subst_list [] s = []" | "apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)" | "(Var v) \triangleleft s = assoc v (Var v) s" | "(Fn f xs) \triangleleft s = (Fn f (apply_subst_list xs s))" primrec occ :: "'a trm \Rightarrow 'a trm \Rightarrow bool" and occ_list :: "'a trm \Rightarrow 'a trm list \Rightarrow bool" where "occ u (Var v) = False" | "occ u (Fn f xs) = (if (list_ex (eq u) xs) then True else (occ_list u xs))" | "occ_list u [] = False" | "occ_list u (x#xs) = (if occ u x then True else occ_list u xs)" lemma subst_no_occ: "\neg occ (Var v) t \Longrightarrow Var v \neq t \Longrightarrow t \triangleleft [(v,s)] = t" apply(induct t) apply(simp) apply(simp) apply(simp) apply(simp) done Greetings Anja Gerbes
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev