# HG changeset patch # User wenzelm # Date 1516093086 -3600 # Node ID 100247708f314de8544582a265cb2c516ab34432 # Parent 3abf6a7225181076b9a462eb7d345892e8e158d8 clarified comments; diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Tue Jan 16 09:30:00 2018 +0100 +++ b/src/HOL/Hoare/Pointer_Examples.thy Tue Jan 16 09:58:06 2018 +0100 @@ -24,20 +24,15 @@ {List tl q (rev Ps @ Qs)}" apply vcg_simp apply fastforce - apply(fastforce intro:notin_List_update[THEN iffD2]) -(* explicit: - apply clarify - apply(rename_tac ps b qs) - apply clarsimp - apply(rename_tac ps') - apply(fastforce intro:notin_List_update[THEN iffD2]) - apply(rule_tac x = ps' in exI) - apply simp - apply(rule_tac x = "b#qs" in exI) - apply simp -*) -apply fastforce -done + apply(fastforce intro:notin_List_update[THEN iffD2]) + \ \explicit:\ + \<^cancel>\apply clarify\ + \<^cancel>\apply(rename_tac ps b qs)\ + \<^cancel>\apply clarsimp\ + \<^cancel>\apply(rename_tac ps')\ + \<^cancel>\apply(fastforce intro:notin_List_update[THEN iffD2])\ + apply fastforce + done text\And now with ghost variables @{term ps} and @{term qs}. Even ``more automatic''.\ diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Pointers0.thy --- a/src/HOL/Hoare/Pointers0.thy Tue Jan 16 09:30:00 2018 +0100 +++ b/src/HOL/Hoare/Pointers0.thy Tue Jan 16 09:58:06 2018 +0100 @@ -188,19 +188,18 @@ {List tl q (rev Ps @ Qs)}" apply vcg_simp apply fastforce - apply(fastforce intro:notin_List_update[THEN iffD2]) -(* explicily: - apply clarify - apply(rename_tac ps qs) - apply clarsimp - apply(rename_tac ps') - apply(rule_tac x = ps' in exI) - apply simp - apply(rule_tac x = "p#qs" in exI) - apply simp -*) -apply fastforce -done + apply(fastforce intro:notin_List_update[THEN iffD2]) + \ \explicit:\ + \<^cancel>\apply clarify\ + \<^cancel>\apply(rename_tac ps qs)\ + \<^cancel>\apply clarsimp\ + \<^cancel>\apply(rename_tac ps')\ + \<^cancel>\apply(rule_tac x = ps' in exI)\ + \<^cancel>\apply simp\ + \<^cancel>\apply(rule_tac x = "p#qs" in exI)\ + \<^cancel>\apply simp\ + apply fastforce + done text "A longer readable version:" diff -r 3abf6a722518 -r 100247708f31 src/HOL/Hoare/Separation.thy --- a/src/HOL/Hoare/Separation.thy Tue Jan 16 09:30:00 2018 +0100 +++ b/src/HOL/Hoare/Separation.thy Tue Jan 16 09:58:06 2018 +0100 @@ -54,13 +54,11 @@ "_wand" :: "bool \ bool \ bool" (infixl "-*" 60) (* FIXME does not handle "_idtdummy" *) -ML\ -(* free_tr takes care of free vars in the scope of sep. logic connectives: - they are implicitly applied to the heap *) +ML \ +\ \\free_tr\ takes care of free vars in the scope of separation logic connectives: + they are implicitly applied to the heap\ fun free_tr(t as Free _) = t $ Syntax.free "H" -(* - | free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps -*) +\<^cancel>\| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\ | free_tr t = t fun emp_tr [] = Syntax.const @{const_syntax is_empty} $ Syntax.free "H" @@ -109,9 +107,7 @@ fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t -(* - | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps -*) +\<^cancel>\| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\ | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t | strip (Abs(_,_,P)) = P | strip (Const(@{const_syntax is_empty},_)) = Syntax.const @{syntax_const "_emp"}