[isabelle-dev] Occur-Check Problem in Isabelle

[Anja Gerbes]

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
-------------- n?chster Teil --------------
Ein Dateianhang mit HTML-Daten wurde abgetrennt...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110713/959de0b4/attachment.html>