Commit f67070d5 authored by lsf37's avatar lsf37
Browse files

re-reverted the accidental revert that happend when devel was

accidentally auto-synced back to Isabelle2007.
parent 1093abc06c16
#!/usr/bin/env bash
#
# $Id: regression,v 1.28 2008-06-11 14:22:50 lsf37 Exp $
# $Id: regression,v 1.29 2008-06-12 06:57:14 lsf37 Exp $
# Author: Gerwin Klein, NICTA
#
# Automated regression test to be run from cron.
......@@ -122,7 +122,7 @@ DIFF=`$WORKING_COPY/admin/report.pl $LOG $REPORT`
# send mail on status changes
if [ -n "$DIFF" ]; then
cat > $TMP <<EOF
The status of the following AFP entries changed:
The status of the following AFP entries changed or remains FAIL:
$DIFF
Tested version: $AFP_VER
......@@ -133,7 +133,7 @@ Have a nice day,
EOF
for R in $MAIN_NOTIFY; do
$MAIL 'status changed (AFP)' "$R" $TMP $REPORT $LOG
$MAIL 'status (AFP)' "$R" $TMP $REPORT $LOG
done
fi
......
#!/usr/bin/perl
#
# $Id: report.pl,v 1.5 2008-06-11 14:22:50 lsf37 Exp $
# $Id: report.pl,v 1.6 2008-06-12 06:57:14 lsf37 Exp $
# Author: Gerwin Klein, NICTA
#
# Parses log file and generates report of entry status.
......@@ -67,6 +67,9 @@ foreach $t (keys old_tests) {
elsif ($old_fail{$t} != $fail{$t}) {
print "[$t] changed from $old_status to $new_status.\n";
}
elsif ($fail{$t}) {
print "[$t] is still on $new_status.\n";
}
}
foreach $t (keys tests) {
......
(* Title: AVL Trees
ID: $Id: AVL.thy,v 1.12 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: AVL.thy,v 1.13 2008-06-12 06:57:14 lsf37 Exp $
Author: Tobias Nipkow and Cornelia Pusch,
converted to Isar by Gerwin Klein
contributions by Achim Brucker, Burkhart Wolff and Jan Smaus
......@@ -73,11 +73,7 @@ definition
mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
consts
l_bal :: "'a * 'a tree * 'a tree \<Rightarrow> 'a tree"
r_bal :: "'a * 'a tree * 'a tree \<Rightarrow> 'a tree"
recdef l_bal "{}"
fun l_bal where
"l_bal(n, MKT ln ll lr h, r) =
(if ht ll < ht lr
then case lr of ET \<Rightarrow> ET (* impossible *)
......@@ -85,7 +81,7 @@ recdef l_bal "{}"
mkt lrn (mkt ln ll lrl) (mkt n lrr r)
else mkt ln ll (mkt n lr r))"
recdef r_bal "{}"
fun r_bal where
"r_bal(n, l, MKT rn rl rr h) =
(if ht rl > ht rr
then case rl of ET \<Rightarrow> ET (* impossible *)
......
(* Title: AVL Trees
ID: $Id: AVL2.thy,v 1.6 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: AVL2.thy,v 1.7 2008-06-12 06:57:14 lsf37 Exp $
Author: Tobias Nipkow and Cornelia Pusch,
converted to Isar by Gerwin Klein
contributions by Achim Brucker, Burkhart Wolff and Jan Smaus
......@@ -73,18 +73,14 @@ primrec
if k<n then (is_in\<^isub>0 k l)
else (is_in\<^isub>0 k r))"
consts
l_bal\<^isub>0 :: "'a * 'a tree\<^isub>0 * 'a tree\<^isub>0 \<Rightarrow> 'a tree\<^isub>0"
r_bal\<^isub>0 :: "'a * 'a tree\<^isub>0 * 'a tree\<^isub>0 \<Rightarrow> 'a tree\<^isub>0"
recdef l_bal\<^isub>0 "{}"
fun l_bal\<^isub>0 where
"l_bal\<^isub>0(n, MKT\<^isub>0 ln ll lr, r) =
(if height ll < height lr
then case lr of ET\<^isub>0 \<Rightarrow> ET\<^isub>0 (* impossible *)
| MKT\<^isub>0 lrn lrl lrr \<Rightarrow> MKT\<^isub>0 lrn (MKT\<^isub>0 ln ll lrl) (MKT\<^isub>0 n lrr r)
else MKT\<^isub>0 ln ll (MKT\<^isub>0 n lr r))"
recdef r_bal\<^isub>0 "{}"
fun r_bal\<^isub>0 where
"r_bal\<^isub>0(n, l, MKT\<^isub>0 rn rl rr) =
(if height rl > height rr
then case rl of ET\<^isub>0 \<Rightarrow> ET\<^isub>0 (* impossible *)
......@@ -284,11 +280,7 @@ definition
mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
consts
l_bal :: "'a * 'a tree * 'a tree \<Rightarrow> 'a tree"
r_bal :: "'a * 'a tree * 'a tree \<Rightarrow> 'a tree"
recdef l_bal "{}"
fun l_bal where
"l_bal(n, MKT ln ll lr h, r) =
(if ht ll < ht lr
then case lr of ET \<Rightarrow> ET (* impossible *)
......@@ -296,7 +288,7 @@ recdef l_bal "{}"
mkt lrn (mkt ln ll lrl) (mkt n lrr r)
else mkt ln ll (mkt n lr r))"
recdef r_bal "{}"
fun r_bal where
"r_bal(n, l, MKT rn rl rr h) =
(if ht rl > ht rr
then case rl of ET \<Rightarrow> ET (* impossible *)
......
(* Title: Inductive definition of Hoare logic for total correctness
ID: $Id: PHoareTotal.thy,v 1.5 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: PHoareTotal.thy,v 1.6 2008-06-12 06:57:15 lsf37 Exp $
Author: Tobias Nipkow, 2001/2006
Maintainer: Tobias Nipkow
*)
......@@ -323,7 +323,7 @@ apply(blast intro:trancl_trans)
done
lemma renumber:
lemma renumber_aux:
"\<lbrakk>\<forall>i. (a,f i) : r^* \<and> (f i,f(Suc i)) : r; (a,b) : r^* \<rbrakk> \<Longrightarrow> b = f 0 \<longrightarrow> (\<exists>f. f 0 = a & (\<forall>i. (f i, f(Suc i)) : r))"
apply(erule converse_rtrancl_induct)
apply blast
......@@ -337,7 +337,7 @@ done
lemma renumber:
"\<forall>i. (a,f i) : r^* \<and> (f i,f(Suc i)) : r \<Longrightarrow> \<exists>f. f 0 = a & (\<forall>i. (f i, f(Suc i)) : r)"
by(blast dest:renumber)
by(blast dest:renumber_aux)
constdefs inf :: "com list \<Rightarrow> state \<Rightarrow> bool"
......@@ -444,7 +444,7 @@ apply(rule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> ((LOCAL f;c;g)#cs,s) |
apply(simp add: exec1.intros split:nat.split)
done
lemma exec1_only1: "(ccs,s) \<rightarrow> (cs',t) \<Longrightarrow>
lemma exec1_only1_aux: "(ccs,s) \<rightarrow> (cs',t) \<Longrightarrow>
\<forall>c cs. ccs = c#cs \<longrightarrow> (\<exists>cs1. cs' = cs1 @ cs)"
apply(erule exec1.induct)
apply blast
......@@ -452,9 +452,9 @@ apply force+
done
lemma exec1_only1: "(c#cs,s) \<rightarrow> (cs',t) \<Longrightarrow> \<exists>cs1. cs' = cs1 @ cs"
by(blast dest:exec1_only1)
by(blast dest:exec1_only1_aux)
lemma exec1_drop_suffix:
lemma exec1_drop_suffix_aux:
"(cs12,s) \<rightarrow> (cs1'2,s') \<Longrightarrow> !cs1 cs2 cs1'.
cs12 = cs1@cs2 & cs1'2 = cs1'@cs2 & cs1 \<noteq> [] \<longrightarrow> (cs1,s) \<rightarrow> (cs1',s')"
apply(erule exec1.induct)
......@@ -463,7 +463,7 @@ done
lemma exec1_drop_suffix:
"(cs1@cs2,s) \<rightarrow> (cs1'@cs2,s') \<Longrightarrow> cs1 \<noteq> [] \<Longrightarrow> (cs1,s) \<rightarrow> (cs1',s')"
by(blast dest:exec1_drop_suffix)
by(blast dest:exec1_drop_suffix_aux)
lemma execs_drop_suffix[rule_format(no_asm)]:
"\<lbrakk> f 0 = (c#cs,s);!i. f(i) \<rightarrow> f(Suc i) \<rbrakk> \<Longrightarrow>
......@@ -489,7 +489,7 @@ apply(drule execs_drop_suffix,assumption,assumption)
apply simp
done
lemma skolemize: "\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f.\<forall>x. P x \<longrightarrow> Q x (f x)"
lemma skolemize1: "\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f.\<forall>x. P x \<longrightarrow> Q x (f x)"
apply(rule_tac x = "\<lambda>x. SOME y. Q x y" in exI)
apply(fast intro:someI2)
done
......@@ -532,7 +532,7 @@ apply(rule conjI)
apply(fast intro: LeastI)
apply(subgoal_tac
"!i<=LEAST i. fst (f i) = cs. EX p. ((p \<noteq> []) = (i<(LEAST i. fst (f i) = cs))) & fst(f i) = p@cs")
apply(drule skolemize)
apply(drule skolemize1)
apply clarify
apply(rename_tac p)
apply(erule_tac p=p in execs_drop_suffix0, assumption)
......@@ -548,7 +548,7 @@ apply(drule not_less_Least)
apply blast
done
lemma skolemize: "\<forall>x.\<exists>y. P x y \<Longrightarrow> \<exists>f.\<forall>x. P x (f x)"
lemma skolemize2: "\<forall>x.\<exists>y. P x y \<Longrightarrow> \<exists>f.\<forall>x. P x (f x)"
apply(rule_tac x = "\<lambda>x. SOME y. P x y" in exI)
apply(fast intro:someI2)
done
......@@ -569,7 +569,7 @@ apply(case_tac "EX i. fst(f i) = cs")
apply(rule disjI1)
apply simp
apply(subgoal_tac "\<forall>i. \<exists>p. p \<noteq> [] \<and> fst(f i) = p@cs")
apply(drule skolemize)
apply(drule skolemize2)
apply clarify
apply(rename_tac p)
apply(rule_tac x = "\<lambda>i. (p i, snd(f i))" in exI)
......
(* Title: Inductive definition of Hoare logic for total correctness
ID: $Id: PsHoareTotal.thy,v 1.5 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: PsHoareTotal.thy,v 1.6 2008-06-12 06:57:15 lsf37 Exp $
Author: Tobias Nipkow, 2001/2006
Maintainer: Tobias Nipkow
*)
......@@ -339,7 +339,7 @@ apply(blast intro:trancl_trans)
done
lemma renumber:
lemma renumber_aux:
"\<lbrakk>\<forall>i. (a,f i) : r^* \<and> (f i,f(Suc i)) : r; (a,b) : r^* \<rbrakk> \<Longrightarrow> b = f 0 \<longrightarrow> (\<exists>f. f 0 = a & (\<forall>i. (f i, f(Suc i)) : r))"
apply(erule converse_rtrancl_induct)
apply blast
......@@ -353,7 +353,7 @@ done
lemma renumber:
"\<forall>i. (a,f i) : r^* \<and> (f i,f(Suc i)) : r \<Longrightarrow> \<exists>f. f 0 = a & (\<forall>i. (f i, f(Suc i)) : r)"
by(blast dest:renumber)
by(blast dest:renumber_aux)
constdefs inf :: "com list \<Rightarrow> state \<Rightarrow> bool"
......@@ -460,16 +460,16 @@ apply(rule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> ((LOCAL f;c;g)#cs,s) |
apply(simp add: exec1.intros split:nat.split)
done
lemma exec1_only1: "(ccs,s) \<rightarrow> (cs',t) \<Longrightarrow>
lemma exec1_only1_aux: "(ccs,s) \<rightarrow> (cs',t) \<Longrightarrow>
\<forall>c cs. ccs = c#cs \<longrightarrow> (\<exists>cs1. cs' = cs1 @ cs)"
apply(erule exec1.induct)
apply force+
done
lemma exec1_only1: "(c#cs,s) \<rightarrow> (cs',t) \<Longrightarrow> \<exists>cs1. cs' = cs1 @ cs"
by(blast dest:exec1_only1)
by(blast dest:exec1_only1_aux)
lemma exec1_drop_suffix:
lemma exec1_drop_suffix_aux:
"(cs12,s) \<rightarrow> (cs1'2,s') \<Longrightarrow> !cs1 cs2 cs1'.
cs12 = cs1@cs2 & cs1'2 = cs1'@cs2 & cs1 \<noteq> [] \<longrightarrow> (cs1,s) \<rightarrow> (cs1',s')"
apply(erule exec1.induct)
......@@ -478,7 +478,7 @@ done
lemma exec1_drop_suffix:
"(cs1@cs2,s) \<rightarrow> (cs1'@cs2,s') \<Longrightarrow> cs1 \<noteq> [] \<Longrightarrow> (cs1,s) \<rightarrow> (cs1',s')"
by(blast dest:exec1_drop_suffix)
by(blast dest:exec1_drop_suffix_aux)
lemma execs_drop_suffix[rule_format(no_asm)]:
"\<lbrakk> f 0 = (c#cs,s);!i. f(i) \<rightarrow> f(Suc i) \<rbrakk> \<Longrightarrow>
......@@ -504,7 +504,7 @@ apply(drule execs_drop_suffix,assumption,assumption)
apply simp
done
lemma skolemize: "\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f.\<forall>x. P x \<longrightarrow> Q x (f x)"
lemma skolemize1: "\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f.\<forall>x. P x \<longrightarrow> Q x (f x)"
apply(rule_tac x = "\<lambda>x. SOME y. Q x y" in exI)
apply(fast intro:someI2)
done
......@@ -547,7 +547,7 @@ apply(rule conjI)
apply(fast intro: LeastI)
apply(subgoal_tac
"!i<=LEAST i. fst (f i) = cs. EX p. ((p \<noteq> []) = (i<(LEAST i. fst (f i) = cs))) & fst(f i) = p@cs")
apply(drule skolemize)
apply(drule skolemize1)
apply clarify
apply(rename_tac p)
apply(erule_tac p=p in execs_drop_suffix0, assumption)
......@@ -563,7 +563,7 @@ apply(drule not_less_Least)
apply blast
done
lemma skolemize: "\<forall>x.\<exists>y. P x y \<Longrightarrow> \<exists>f.\<forall>x. P x (f x)"
lemma skolemize2: "\<forall>x.\<exists>y. P x y \<Longrightarrow> \<exists>f.\<forall>x. P x (f x)"
apply(rule_tac x = "\<lambda>x. SOME y. P x y" in exI)
apply(fast intro:someI2)
done
......@@ -584,7 +584,7 @@ apply(case_tac "EX i. fst(f i) = cs")
apply(rule disjI1)
apply simp
apply(subgoal_tac "\<forall>i. \<exists>p. p \<noteq> [] \<and> fst(f i) = p@cs")
apply(drule skolemize)
apply(drule skolemize2)
apply clarify
apply(rename_tac p)
apply(rule_tac x = "\<lambda>i. (p i, snd(f i))" in exI)
......
(* Title: BDD
ID: $Id: BinDag.thy,v 1.4 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: BinDag.thy,v 1.5 2008-06-12 06:57:15 lsf37 Exp $
Author: Veronika Ortner and Norbert Schirmer, 2004
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
......@@ -29,7 +29,9 @@ USA
header {* BDD Abstractions *}
theory BinDag imports "../Heap" begin
theory BinDag
imports "../Simpl/Heap"
begin
datatype dag = Tip | Node dag ref dag
......@@ -77,12 +79,14 @@ lemma subdag_NodeD:
lemma subdag_not_sym: "\<And>t. \<lbrakk>subdag s t; subdag t s\<rbrakk> \<Longrightarrow> P"
by (induct s) (auto dest: subdag_NodeD)
instantiation dag:: order
begin
instance dag:: ord ..
definition
less_dag_def: "s < (t::dag) \<longleftrightarrow> subdag t s"
defs (overloaded)
less_dag_def: "s < (t::dag) \<equiv> subdag t s"
le_dag_def: "s \<le> (t::dag) \<equiv> s=t \<or> s < t"
definition
le_dag_def: "s \<le> (t::dag) \<longleftrightarrow> s=t \<or> s < t"
lemma le_dag_refl: "(x::dag) \<le> x"
by (simp add: le_dag_def)
......@@ -111,7 +115,6 @@ lemma le_dag_trans:
qed
qed
lemma le_dag_antisym:
fixes x::dag and y
assumes x_y: "x \<le> y" and y_x: "y \<le> x"
......@@ -129,10 +132,10 @@ lemma dag_less_le:
shows "(x < y) = (x \<le> y \<and> x \<noteq> y)"
by (auto simp add: less_dag_def le_dag_def dest: subdag_neq)
instance dag:: order
by (intro_classes,
(assumption
| rule le_dag_refl le_dag_trans le_dag_antisym dag_less_le)+)
instance by default
(assumption | rule le_dag_refl le_dag_trans le_dag_antisym dag_less_le)+
end
lemma less_dag_Tip [simp]: "\<not> (x < Tip)"
by (simp add: less_dag_def)
......
(* Title: BDD
ID: $Id: EvalProof.thy,v 1.4 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: EvalProof.thy,v 1.5 2008-06-12 06:57:15 lsf37 Exp $
Author: Veronika Ortner and Norbert Schirmer, 2004
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LPGL
......@@ -33,7 +33,7 @@ theory EvalProof imports ProcedureSpecs begin
lemma (in Eval_impl) Eval_modifies:
shows "\<forall>\<sigma>. \<Gamma>\<turnstile>{\<sigma>} PROC Eval (\<acute>p, \<acute>varval, \<acute>R)
{t. t may_not_modify_globals \<sigma>}"
apply (hoare_rule ProcRec1)
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
......@@ -43,7 +43,7 @@ lemma (in Eval_impl) Eval_spec:
\<lbrace>\<sigma>. Dag \<acute>p \<acute>low \<acute>high t \<and> bdt t \<acute>var = Some bdt1\<rbrace>
\<acute>R :== PROC Eval(\<acute>p, \<acute>varval)
\<lbrace>\<acute>R = eval bdt1 \<^bsup>\<sigma>\<^esup>varval \<rbrace>"
apply (hoare_rule ProcRec1)
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply clarsimp
apply safe
......
(* Title: BDD
ID: $Id: General.thy,v 1.6 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: General.thy,v 1.7 2008-06-12 06:57:15 lsf37 Exp $
Author: Veronika Ortner and Norbert Schirmer, 2004
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
......@@ -42,39 +42,37 @@ primrec
"root Tip = Null"
"root (Node l a r) = a"
consts isLeaf :: "dag \<Rightarrow> bool"
recdef isLeaf "measure size"
fun isLeaf :: "dag \<Rightarrow> bool" where
"isLeaf Tip = False"
"isLeaf (Node Tip v Tip) = True"
"isLeaf (Node (Node l v\<^isub>1 r) v\<^isub>2 Tip) = False"
"isLeaf (Node Tip v\<^isub>1 (Node l v\<^isub>2 r)) = False"
| "isLeaf (Node Tip v Tip) = True"
| "isLeaf (Node (Node l v\<^isub>1 r) v\<^isub>2 Tip) = False"
| "isLeaf (Node Tip v\<^isub>1 (Node l v\<^isub>2 r)) = False"
datatype bdt = Zero | One | Bdt_Node bdt nat bdt
consts bdt :: "dag \<Rightarrow> (ref \<Rightarrow> nat) \<Rightarrow> bdt option"
recdef bdt "measure size"
"bdt Tip = (\<lambda>bdtvar . None)"
"bdt (Node Tip vref Tip) =
fun bdt_fn :: "dag \<Rightarrow> (ref \<Rightarrow> nat) \<Rightarrow> bdt option" where
"bdt_fn Tip = (\<lambda>bdtvar . None)"
| "bdt_fn (Node Tip vref Tip) =
(\<lambda>bdtvar .
(if (bdtvar vref = 0)
then Some Zero
else (if (bdtvar vref = 1)
then Some One
else None)))"
"bdt (Node Tip vref (Node l vref1 r)) = (\<lambda>bdtvar . None)"
"bdt (Node (Node l vref1 r) vref Tip) = (\<lambda>bdtvar . None)"
"bdt (Node (Node l1 vref1 r1) vref (Node l2 vref2 r2)) =
| "bdt_fn (Node Tip vref (Node l vref1 r)) = (\<lambda>bdtvar . None)"
| "bdt_fn (Node (Node l vref1 r) vref Tip) = (\<lambda>bdtvar . None)"
| "bdt_fn (Node (Node l1 vref1 r1) vref (Node l2 vref2 r2)) =
(\<lambda>bdtvar .
(if (bdtvar vref = 0 \<or> bdtvar vref = 1)
then None
else
(case (bdt (Node l1 vref1 r1) bdtvar) of
(case (bdt_fn (Node l1 vref1 r1) bdtvar) of
None \<Rightarrow> None
|(Some b1) \<Rightarrow>
(case (bdt (Node l2 vref2 r2) bdtvar) of
(case (bdt_fn (Node l2 vref2 r2) bdtvar) of
None \<Rightarrow> None
|(Some b2) \<Rightarrow> Some (Bdt_Node b1 (bdtvar vref) b2)))))"
(hints cong add: option.case_cong if_cong)
(*
Kongruenzregeln sind das Feintuning fr den Simplifier (siehe Kapitel 9 im Isabelle
Tutorial). Im Fall von case wird standardmig nur die case bedingung nicht
......@@ -83,7 +81,7 @@ Auswertungsstrategie einer Programmiersprache, da wird auch zun
Bedingung vereinfacht. Will man mehr so kann man die entsprechenden Kongruenz
regeln dazunehmen.
*)
abbreviation "bdt == bdt_fn"
consts eval :: "bdt \<Rightarrow> bool list \<Rightarrow> bool"
primrec
......@@ -93,30 +91,28 @@ primrec
(*A given bdt is ordered if it is a One or Zero or its value is smaller than
its parents value*)
consts ordered_bdt:: "bdt \<Rightarrow> bool"
recdef ordered_bdt "measure size"
fun ordered_bdt:: "bdt \<Rightarrow> bool" where
"ordered_bdt Zero = True"
"ordered_bdt One = True"
"ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v (Bdt_Node l2 v2 r2)) =
| "ordered_bdt One = True"
| "ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v (Bdt_Node l2 v2 r2)) =
((v1 < v) \<and> (v2 < v) \<and>
(ordered_bdt (Bdt_Node l1 v1 r1)) \<and> (ordered_bdt (Bdt_Node l2 v2 r2)))"
"ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v r) =
| "ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v r) =
((v1 < v) \<and> (ordered_bdt (Bdt_Node l1 v1 r1)))"
"ordered_bdt (Bdt_Node l v (Bdt_Node l2 v2 r2)) =
| "ordered_bdt (Bdt_Node l v (Bdt_Node l2 v2 r2)) =
((v2 < v) \<and> (ordered_bdt (Bdt_Node l2 v2 r2)))"
"ordered_bdt (Bdt_Node l v r) = True"
| "ordered_bdt (Bdt_Node l v r) = True"
(*In case t = (Node Tip v Tip) v should have the values 0 or 1. This is not checked by this function*)
consts ordered:: "dag \<Rightarrow> (ref\<Rightarrow>nat) \<Rightarrow> bool"
recdef ordered "measure size"
fun ordered:: "dag \<Rightarrow> (ref\<Rightarrow>nat) \<Rightarrow> bool" where
"ordered Tip = (\<lambda> var. True)"
"ordered (Node (Node l\<^isub>1 v\<^isub>1 r\<^isub>1) v (Node l\<^isub>2 v\<^isub>2 r\<^isub>2)) =
| "ordered (Node (Node l\<^isub>1 v\<^isub>1 r\<^isub>1) v (Node l\<^isub>2 v\<^isub>2 r\<^isub>2)) =
(\<lambda> var. (var v\<^isub>1 < var v \<and> var v\<^isub>2 < var v) \<and>
(ordered (Node l\<^isub>1 v\<^isub>1 r\<^isub>1) var) \<and> (ordered (Node l\<^isub>2 v\<^isub>2 r\<^isub>2) var))"
"ordered (Node Tip v Tip) = (\<lambda> var. (True))"
"ordered (Node Tip v r) =
| "ordered (Node Tip v Tip) = (\<lambda> var. (True))"
| "ordered (Node Tip v r) =
(\<lambda> var. (var (root r) < var v) \<and> (ordered r var))"
"ordered (Node l v Tip) =
| "ordered (Node l v Tip) =
(\<lambda> var. (var (root l) < var v) \<and> (ordered l var))"
......@@ -141,13 +137,13 @@ done
lemma bdt_Some_One_iff [simp]:
"(bdt t var = Some One) = (\<exists> p. t = Node Tip p Tip \<and> var p = 1)"
apply (induct_tac t rule: bdt.induct) (*bdt is a recdef*)
apply (induct_tac t rule: bdt_fn.induct)
apply (auto split: option.splits) (*in order to split the cases Zero and One*)
done
lemma bdt_Some_Zero_iff [simp]:
"(bdt t var = Some Zero) = (\<exists> p. t = Node Tip p Tip \<and> var p = 0)"
apply (induct_tac t rule: bdt.induct)
apply (induct_tac t rule: bdt_fn.induct)
apply (auto split: option.splits)
done
......@@ -156,7 +152,7 @@ lemma bdt_Some_Node_iff [simp]:
"(bdt t var = Some (Bdt_Node bdt1 v bdt2)) =
(\<exists> p l r. t = Node l p r \<and> bdt l var = Some bdt1 \<and> bdt r var = Some bdt2 \<and>
1 < v \<and> var p = v )"
apply (induct_tac t rule: bdt.induct)
apply (induct_tac t rule: bdt_fn.induct)
prefer 5
apply (fastsimp split: if_splits option.splits)
apply auto
......@@ -171,9 +167,9 @@ proof (induct t)
next
case (Node lt a rt)
note NN= this
have bdt1: "bdt (Node lt a rt) var = Some bdt1" .
have no_in_t: " no \<in> set_of (Node lt a rt)" .
have p_tree: "Dag p low high (Node lt a rt)" .
have bdt1: "bdt (Node lt a rt) var = Some bdt1" by fact
have no_in_t: " no \<in> set_of (Node lt a rt)" by fact
have p_tree: "Dag p low high (Node lt a rt)" by fact
from Node.prems obtain
lt: "Dag (low p) low high lt" and
rt: "Dag (high p) low high rt"
......@@ -473,7 +469,7 @@ lemma subdag_ordered:
no \<in> set_of t\<rbrakk> \<Longrightarrow> ordered not var"
proof (induct t)
case Tip
with Tip.prems show ?case by simp
from Tip.prems show ?case by simp
next
case (Node lt po rt)
note nN=this
......@@ -489,9 +485,7 @@ next
from Tip ltTip Node.prems have "no=p"
by simp
with ppo Node.prems have "not=(Node lt po rt)"
apply -
apply (simp del: Dag_Ref add: Dag_unique)
done
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
next
case (Node lrnot rn rrnot)
......@@ -501,20 +495,21 @@ next
by simp
from Node.prems have ponN: "po \<noteq> Null"
by auto
with ppo ponN ltTip Node.prems Node have "Dag (high po) low high rt"
with ppo ponN ltTip Node.prems have *: "Dag (high po) low high rt"
by auto
with Node.hyps Node.prems ord_rt show ?thesis
show ?thesis
proof (cases "no=po")
case True
with ppo Node.prems have "not = (Node lt po rt)"
with ppo Node.prems have "not = Node lt po rt"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
with Node.prems show ?thesis
by simp
next
assume "no\<noteq> po"
case False
with Node.prems ltTip have "no \<in> set_of rt"
by simp
with ord_rt Node.prems show ?thesis
by auto
with ord_rt * `Dag no low high not` show ?thesis
by (rule Node.hyps)
qed
qed
next
......@@ -529,20 +524,20 @@ next
by simp
from Node.prems have ponN: "po \<noteq> Null"
by auto
with ppo ponN Tip Node.prems ltNode have "Dag (low po) low high lt"
with ppo ponN Tip Node.prems ltNode have *: "Dag (low po) low high lt"
by auto
with Node.hyps Node.prems ord_lt show ?thesis
show ?thesis
proof (cases "no=po")
case True
with ppo Node.prems have "not = (Node lt po rt)"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
next
assume "no\<noteq> po"
case False
with Node.prems Tip have "no \<in> set_of lt"
by simp
with ord_lt Node.prems show ?thesis
by auto
with ord_lt * `Dag no low high not` show ?thesis
by (rule Node.hyps)
qed
next
case (Node lrt r rrt)
......@@ -708,11 +703,10 @@ defs shared_lower_levels_def : "shared_lower_levels t i bdtvar == \<forall> st1
*)
consts reduced :: "dag \<Rightarrow> bool"
recdef reduced "measure size"
fun reduced :: "dag \<Rightarrow> bool" where
"reduced Tip = True"
"reduced (Node Tip v Tip) = True"
"reduced (Node l v r) = (l \<noteq> r \<and> reduced l \<and> reduced r)"
| "reduced (Node Tip v Tip) = True"
| "reduced (Node l v r) = (l \<noteq> r \<and> reduced l \<and> reduced r)"
consts reduced_bdt :: "bdt \<Rightarrow> bool"
primrec
......@@ -1222,9 +1216,12 @@ proof (rule ballI)
done
from x_in_pret ord_pret highnN True have children_var_smaller: "var (low x) < var x \<and> var (high x) < var x"
apply -
thm var_ordered_children
apply (rule var_ordered_children)
apply assumption+
apply (rule pret_dag)
apply (rule ord_pret)
apply (rule x_in_pret)
apply (rule True)
apply (rule highnN)
done
with xsnb have lowxsnb: "var (low x) < nb"
by arith
......
......@@ -31,9 +31,9 @@ MAXTIME = 3600
## dependencies
$(SESSION-NAME): $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(SESSION-NAME): Simpl $(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz
$(IMAGE):
Simpl:
cd ../Simpl; $(ISATOOL) make Simpl
$(LOG)/$(BASE-IMAGE)-$(SESSION-NAME).gz: $(IMAGE) ROOT.ML *.thy document/*.tex document/*.bib
......
(* Title: BDD
ID: $Id: LevellistProof.thy,v 1.6 2008-06-11 14:22:50 lsf37 Exp $
ID: $Id: LevellistProof.thy,v 1.7 2008-06-12 06:57:15 lsf37 Exp $
Author: Veronika Ortner and Norbert Schirmer, 2004
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
......@@ -30,10 +30,12 @@ USA
header {* Proof of Procedure Levellist *}
theory LevellistProof imports ProcedureSpecs "../HeapList" begin
hide (open) const DistinctTreeProver.set_of tree.Node tree.Tip
lemma (in Levellist_impl) Levellist_modifies:
shows "\<forall>\<sigma>. \<Gamma>\<turnstile>{\<sigma>} \<acute>levellist :== PROC Levellist (\<acute>p, \<acute>m, \<acute>levellist)
{t. t may_only_modify_globals \<sigma> in [mark,next]}"