src/HOL/Hoare/Pointer_Examples.thy
changeset 24499 5a3ee202e0b0
parent 19399 fd2ba98056a2
child 35316 870dfea4f9c0
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 16:17:53 2007 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 18:46:33 2007 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  theory Pointer_Examples imports HeapSyntax begin
     1.6  
     1.7 +axiomatization where unproven: "PROP A"
     1.8 +
     1.9  section "Verifications"
    1.10  
    1.11  subsection "List reversal"
    1.12 @@ -340,38 +342,35 @@
    1.13  consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
    1.14         path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    1.15  
    1.16 -ML"set quick_and_dirty"
    1.17 -
    1.18  text"First some basic lemmas:"
    1.19  
    1.20  lemma [simp]: "ispath f p p"
    1.21 -sorry
    1.22 +by (rule unproven)
    1.23  lemma [simp]: "path f p p = []"
    1.24 -sorry
    1.25 +by (rule unproven)
    1.26  lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
    1.27 -sorry
    1.28 +by (rule unproven)
    1.29  lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
    1.30   path (f(a := r)) p q = path f p q"
    1.31 -sorry
    1.32 +by (rule unproven)
    1.33  
    1.34  text"Some more specific lemmas needed by the example:"
    1.35  
    1.36  lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
    1.37 -sorry
    1.38 +by (rule unproven)
    1.39  lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
    1.40   path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
    1.41 -sorry
    1.42 +by (rule unproven)
    1.43  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
    1.44   b \<notin> set (path f p (Ref a))"
    1.45 -sorry
    1.46 +by (rule unproven)
    1.47  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
    1.48 -sorry
    1.49 +by (rule unproven)
    1.50  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
    1.51 -sorry
    1.52 +by (rule unproven)
    1.53  
    1.54  lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
    1.55 -sorry
    1.56 -ML"reset quick_and_dirty"
    1.57 +by (rule unproven)
    1.58  
    1.59  lemma "VARS hd tl p q r s
    1.60   {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>