do not touch quick_and_dirty;
authorwenzelm
Fri Aug 31 18:46:33 2007 +0200 (2007-08-31)
changeset 244995a3ee202e0b0
parent 24498 0a57b1b472b2
child 24500 5e135602f660
do not touch quick_and_dirty;
src/FOL/ex/LocaleTest.thy
src/HOL/Hoare/Pointer_Examples.thy
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Fri Aug 31 16:17:53 2007 +0200
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Fri Aug 31 18:46:33 2007 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4  imports FOL
     1.5  begin
     1.6  
     1.7 -ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
     1.8  ML {* set Toplevel.debug *}
     1.9  ML {* set show_hyps *}
    1.10  ML {* set show_sorts *}
     2.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 16:17:53 2007 +0200
     2.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 18:46:33 2007 +0200
     2.3 @@ -8,6 +8,8 @@
     2.4  
     2.5  theory Pointer_Examples imports HeapSyntax begin
     2.6  
     2.7 +axiomatization where unproven: "PROP A"
     2.8 +
     2.9  section "Verifications"
    2.10  
    2.11  subsection "List reversal"
    2.12 @@ -340,38 +342,35 @@
    2.13  consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
    2.14         path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    2.15  
    2.16 -ML"set quick_and_dirty"
    2.17 -
    2.18  text"First some basic lemmas:"
    2.19  
    2.20  lemma [simp]: "ispath f p p"
    2.21 -sorry
    2.22 +by (rule unproven)
    2.23  lemma [simp]: "path f p p = []"
    2.24 -sorry
    2.25 +by (rule unproven)
    2.26  lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
    2.27 -sorry
    2.28 +by (rule unproven)
    2.29  lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
    2.30   path (f(a := r)) p q = path f p q"
    2.31 -sorry
    2.32 +by (rule unproven)
    2.33  
    2.34  text"Some more specific lemmas needed by the example:"
    2.35  
    2.36  lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
    2.37 -sorry
    2.38 +by (rule unproven)
    2.39  lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
    2.40   path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
    2.41 -sorry
    2.42 +by (rule unproven)
    2.43  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
    2.44   b \<notin> set (path f p (Ref a))"
    2.45 -sorry
    2.46 +by (rule unproven)
    2.47  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
    2.48 -sorry
    2.49 +by (rule unproven)
    2.50  lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
    2.51 -sorry
    2.52 +by (rule unproven)
    2.53  
    2.54  lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
    2.55 -sorry
    2.56 -ML"reset quick_and_dirty"
    2.57 +by (rule unproven)
    2.58  
    2.59  lemma "VARS hd tl p q r s
    2.60   {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>