--- a/src/HOL/IMP/Big_Step.thy Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/IMP/Big_Step.thy Mon Aug 08 16:19:57 2011 -0700
@@ -113,6 +113,10 @@
qed
qed
+(* Using rule inversion to prove simplification rules: *)
+lemma assign_simp:
+ "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
+ by auto
subsection "Command Equivalence"
--- a/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 16:19:57 2011 -0700
@@ -479,9 +479,7 @@
"ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
by (induct c) auto
-lemma assign [simp]:
- "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
- by auto
+declare assign_simp [simp]
lemma ccomp_exec_n:
"ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Fold.thy Mon Aug 08 16:19:57 2011 -0700
@@ -0,0 +1,413 @@
+header "Constant Folding"
+
+theory Fold imports Sem_Equiv begin
+
+section "Simple folding of arithmetic expressions"
+
+types
+ tab = "name \<Rightarrow> val option"
+
+(* maybe better as the composition of substitution and the existing simp_const(0) *)
+fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
+"simp_const (N n) _ = N n" |
+"simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
+"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
+ (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
+
+definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
+
+theorem aval_simp_const[simp]:
+assumes "approx t s"
+shows "aval (simp_const a t) s = aval a s"
+ using assms
+ by (induct a) (auto simp: approx_def split: aexp.split option.split)
+
+theorem aval_simp_const_N:
+assumes "approx t s"
+shows "simp_const a t = N n \<Longrightarrow> aval a s = n"
+ using assms
+ by (induct a arbitrary: n)
+ (auto simp: approx_def split: aexp.splits option.splits)
+
+definition
+ "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
+
+primrec lnames :: "com \<Rightarrow> name set" where
+"lnames SKIP = {}" |
+"lnames (x ::= a) = {x}" |
+"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
+"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
+"lnames (WHILE b DO c) = lnames c"
+
+primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"defs SKIP t = t" |
+"defs (x ::= a) t =
+ (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"defs (c1;c2) t = (defs c2 o defs c1) t" |
+"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
+"defs (WHILE b DO c) t = t |` (-lnames c)"
+
+primrec fold where
+"fold SKIP _ = SKIP" |
+"fold (x ::= a) t = (x ::= (simp_const a t))" |
+"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
+"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
+"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
+
+lemma approx_merge:
+ "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
+ by (fastsimp simp: merge_def approx_def)
+
+lemma approx_map_le:
+ "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
+ by (clarsimp simp: approx_def map_le_def dom_def)
+
+lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
+ by (clarsimp simp: restrict_map_def map_le_def)
+
+lemma merge_restrict:
+ assumes "t1 |` S = t |` S"
+ assumes "t2 |` S = t |` S"
+ shows "merge t1 t2 |` S = t |` S"
+proof -
+ from assms
+ have "\<forall>x. (t1 |` S) x = (t |` S) x"
+ and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
+ thus ?thesis
+ by (auto simp: merge_def restrict_map_def
+ split: if_splits intro: ext)
+qed
+
+
+lemma defs_restrict:
+ "defs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+ case (Semi c1 c2)
+ hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+ by simp
+ hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from Semi
+ have "defs c2 (defs c1 t) |` (- lnames c2) =
+ defs c1 t |` (- lnames c2)"
+ by simp
+ hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
+ defs c1 t |` (- lnames c2) |` (- lnames c1)"
+ by simp
+ ultimately
+ show ?case by (clarsimp simp: Int_commute)
+next
+ case (If b c1 c2)
+ hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+ hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from If
+ have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+ hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
+ t |` (- lnames c2) |` (-lnames c1)" by simp
+ ultimately
+ show ?case by (auto simp: Int_commute intro: merge_restrict)
+qed (auto split: aexp.split)
+
+
+lemma big_step_pres_approx:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Skip thus ?case by simp
+next
+ case Assign
+ thus ?case
+ by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+ hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s')
+ hence "approx (defs c1 t) s'" by simp
+ thus ?case by (simp add: approx_merge)
+next
+ case (IfFalse b s c2 s')
+ hence "approx (defs c2 t) s'" by simp
+ thus ?case by (simp add: approx_merge)
+next
+ case WhileFalse
+ thus ?case by (simp add: approx_def restrict_map_def)
+next
+ case (WhileTrue b s1 c s2 s3)
+ hence "approx (defs c t) s2" by simp
+ with WhileTrue
+ have "approx (defs c t |` (-lnames c)) s3" by simp
+ thus ?case by (simp add: defs_restrict)
+qed
+
+corollary approx_defs_inv [simp]:
+ "\<Turnstile> {approx t} c {approx (defs c t)}"
+ by (simp add: hoare_valid_def big_step_pres_approx)
+
+
+lemma big_step_pres_approx_restrict:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Assign
+ thus ?case by (clarsimp simp: approx_def)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
+ by (rule Semi)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
+ by (rule Semi)
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s' c2)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
+ by (simp add: Int_commute)
+ hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
+ by (rule IfTrue)
+ thus ?case by (simp add: Int_commute)
+next
+ case (IfFalse b s c2 s' c1)
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
+ by simp
+ hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
+ by (rule IfFalse)
+ thus ?case by simp
+qed auto
+
+
+lemma approx_restrict_inv:
+ "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
+ by (simp add: hoare_valid_def big_step_pres_approx_restrict)
+
+declare assign_simp [simp]
+
+lemma approx_eq:
+ "approx t \<Turnstile> c \<sim> fold c t"
+proof (induct c arbitrary: t)
+ case SKIP show ?case by simp
+next
+ case Assign
+ show ?case by (simp add: equiv_up_to_def)
+next
+ case Semi
+ thus ?case by (auto intro!: equiv_up_to_semi)
+next
+ case If
+ thus ?case by (auto intro!: equiv_up_to_if_weak)
+next
+ case (While b c)
+ hence "approx (t |` (- lnames c)) \<Turnstile>
+ WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
+ by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
+ thus ?case
+ by (auto intro: equiv_up_to_weaken approx_map_le)
+qed
+
+
+lemma approx_empty [simp]:
+ "approx empty = (\<lambda>_. True)"
+ by (auto intro!: ext simp: approx_def)
+
+lemma equiv_sym:
+ "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
+ by (auto simp add: equiv_def)
+
+theorem constant_folding_equiv:
+ "fold c empty \<sim> c"
+ using approx_eq [of empty c]
+ by (simp add: equiv_up_to_True equiv_sym)
+
+
+
+section {* More ambitious folding including boolean expressions *}
+
+
+fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
+"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
+"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
+"bsimp_const (Not b) t = not(bsimp_const b t)" |
+"bsimp_const (B bv) _ = B bv"
+
+theorem bvalsimp_const [simp]:
+ assumes "approx t s"
+ shows "bval (bsimp_const b t) s = bval b s"
+ using assms by (induct b) auto
+
+lemma not_B [simp]: "not (B v) = B (\<not>v)"
+ by (cases v) auto
+
+lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
+ by (cases b) auto
+
+lemma and_B_eq:
+ "(and a b = B v) = (a = B False \<and> \<not>v \<or>
+ b = B False \<and> \<not>v \<or>
+ (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
+ by (rule and.induct) auto
+
+lemma less_B_eq [simp]:
+ "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
+ by (rule less.induct) auto
+
+theorem bvalsimp_const_B:
+assumes "approx t s"
+shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
+ using assms
+ by (induct b arbitrary: v)
+ (auto simp: approx_def and_B_eq aval_simp_const_N
+ split: bexp.splits bool.splits)
+
+
+primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"bdefs SKIP t = t" |
+"bdefs (x ::= a) t =
+ (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
+"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+ B True \<Rightarrow> bdefs c1 t
+ | B False \<Rightarrow> bdefs c2 t
+ | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
+"bdefs (WHILE b DO c) t = t |` (-lnames c)"
+
+
+primrec bfold where
+"bfold SKIP _ = SKIP" |
+"bfold (x ::= a) t = (x ::= (simp_const a t))" |
+"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
+"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+ B True \<Rightarrow> bfold c1 t
+ | B False \<Rightarrow> bfold c2 t
+ | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
+"bfold (WHILE b DO c) t = (case bsimp_const b t of
+ B False \<Rightarrow> SKIP
+ | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
+
+
+lemma bdefs_restrict:
+ "bdefs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+ case (Semi c1 c2)
+ hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
+ by simp
+ hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from Semi
+ have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
+ bdefs c1 t |` (- lnames c2)"
+ by simp
+ hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
+ bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
+ by simp
+ ultimately
+ show ?case by (clarsimp simp: Int_commute)
+next
+ case (If b c1 c2)
+ hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+ hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
+ t |` (- lnames c1) |` (-lnames c2)" by simp
+ moreover
+ from If
+ have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+ hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
+ t |` (- lnames c2) |` (-lnames c1)" by simp
+ ultimately
+ show ?case
+ by (auto simp: Int_commute intro: merge_restrict
+ split: bexp.splits bool.splits)
+qed (auto split: aexp.split bexp.split bool.split)
+
+
+lemma big_step_pres_approx_b:
+ "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+ case Skip thus ?case by simp
+next
+ case Assign
+ thus ?case
+ by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+ case (Semi c1 s1 s2 c2 s3)
+ have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+ hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
+ thus ?case by simp
+next
+ case (IfTrue b s c1 s')
+ hence "approx (bdefs c1 t) s'" by simp
+ thus ?case using `bval b s` `approx t s`
+ by (clarsimp simp: approx_merge bvalsimp_const_B
+ split: bexp.splits bool.splits)
+next
+ case (IfFalse b s c2 s')
+ hence "approx (bdefs c2 t) s'" by simp
+ thus ?case using `\<not>bval b s` `approx t s`
+ by (clarsimp simp: approx_merge bvalsimp_const_B
+ split: bexp.splits bool.splits)
+next
+ case WhileFalse
+ thus ?case
+ by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
+ split: bexp.splits bool.splits)
+next
+ case (WhileTrue b s1 c s2 s3)
+ hence "approx (bdefs c t) s2" by simp
+ with WhileTrue
+ have "approx (bdefs c t |` (- lnames c)) s3"
+ by simp
+ thus ?case
+ by (simp add: bdefs_restrict)
+qed
+
+corollary approx_bdefs_inv [simp]:
+ "\<Turnstile> {approx t} c {approx (bdefs c t)}"
+ by (simp add: hoare_valid_def big_step_pres_approx_b)
+
+lemma bfold_equiv:
+ "approx t \<Turnstile> c \<sim> bfold c t"
+proof (induct c arbitrary: t)
+ case SKIP show ?case by simp
+next
+ case Assign
+ thus ?case by (simp add: equiv_up_to_def)
+next
+ case Semi
+ thus ?case by (auto intro!: equiv_up_to_semi)
+next
+ case (If b c1 c2)
+ hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
+ IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
+ by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
+ thus ?case using If
+ by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits
+ intro: equiv_up_to_trans)
+ next
+ case (While b c)
+ hence "approx (t |` (- lnames c)) \<Turnstile>
+ WHILE b DO c \<sim>
+ WHILE bsimp_const b (t |` (- lnames c))
+ DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
+ by (auto intro: equiv_up_to_while_weak approx_restrict_inv
+ simp: bequiv_up_to_def)
+ hence "approx t \<Turnstile> ?W \<sim> ?W'"
+ by (auto intro: equiv_up_to_weaken approx_map_le)
+ thus ?case
+ by (auto split: bexp.splits bool.splits
+ intro: equiv_up_to_while_False
+ simp: bvalsimp_const_B)
+qed
+
+
+theorem constant_bfolding_equiv:
+ "bfold c empty \<sim> c"
+ using bfold_equiv [of empty c]
+ by (simp add: equiv_up_to_True equiv_sym)
+
+
+end
--- a/src/HOL/IMP/ROOT.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/IMP/ROOT.ML Mon Aug 08 16:19:57 2011 -0700
@@ -17,5 +17,6 @@
"Procs_Stat_Vars_Dyn",
"Procs_Stat_Vars_Stat",
"C_like",
- "OO"
+ "OO",
+ "Fold"
];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sem_Equiv.thy Mon Aug 08 16:19:57 2011 -0700
@@ -0,0 +1,165 @@
+header "Semantic Equivalence up to a Condition"
+
+theory Sem_Equiv
+imports Hoare_Sound_Complete
+begin
+
+definition
+ equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
+where
+ "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
+
+definition
+ bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
+where
+ "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
+
+lemma equiv_up_to_True:
+ "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
+ by (simp add: equiv_def equiv_up_to_def)
+
+lemma equiv_up_to_weaken:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
+ by (simp add: equiv_up_to_def)
+
+lemma equiv_up_toI:
+ "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
+ by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD1:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
+ by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD2:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
+ by (unfold equiv_up_to_def) blast
+
+
+lemma equiv_up_to_refl [simp, intro!]:
+ "P \<Turnstile> c \<sim> c"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_sym:
+ "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_trans [trans]:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
+ by (auto simp: equiv_up_to_def)
+
+
+lemma bequiv_up_to_refl [simp, intro!]:
+ "P \<Turnstile> b <\<sim>> b"
+ by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_sym:
+ "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
+ by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_trans [trans]:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
+ by (auto simp: bequiv_up_to_def)
+
+
+lemma equiv_up_to_hoare:
+ "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+ unfolding hoare_valid_def equiv_up_to_def by blast
+
+lemma equiv_up_to_hoare_eq:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+ by (rule equiv_up_to_hoare)
+
+
+lemma equiv_up_to_semi:
+ "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
+ P \<Turnstile> (c; d) \<sim> (c'; d')"
+ by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
+
+lemma equiv_up_to_while_lemma:
+ shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
+ P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
+ (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+ \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
+ P s \<Longrightarrow>
+ d = WHILE b DO c \<Longrightarrow>
+ (WHILE b' DO c', s) \<Rightarrow> s'"
+proof (induct rule: big_step_induct)
+ case (WhileTrue b s1 c s2 s3)
+ note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
+
+ from WhileTrue.prems
+ have "P \<Turnstile> b <\<sim>> b'" by simp
+ with `bval b s1` `P s1`
+ have "bval b' s1" by (simp add: bequiv_up_to_def)
+ moreover
+ from WhileTrue.prems
+ have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
+ with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
+ have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
+ moreover
+ from WhileTrue.prems
+ have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
+ with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
+ have "P s2" by (simp add: hoare_valid_def)
+ hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
+ ultimately
+ show ?case by blast
+next
+ case WhileFalse
+ thus ?case by (auto simp: bequiv_up_to_def)
+qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
+
+lemma bequiv_context_subst:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
+ by (auto simp: bequiv_up_to_def)
+
+lemma equiv_up_to_while:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+ \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
+ P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+ apply (safe intro!: equiv_up_toI)
+ apply (auto intro: equiv_up_to_while_lemma)[1]
+ apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
+ apply (drule equiv_up_to_sym [THEN iffD1])
+ apply (drule bequiv_up_to_sym [THEN iffD1])
+ apply (auto intro: equiv_up_to_while_lemma)[1]
+ done
+
+lemma equiv_up_to_while_weak:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow>
+ P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+ by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken
+ simp: hoare_valid_def)
+
+lemma equiv_up_to_if:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+ P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+ by (auto simp: bequiv_up_to_def equiv_up_to_def)
+
+lemma equiv_up_to_if_weak:
+ "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
+ P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+ by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
+
+lemma equiv_up_to_if_True [intro!]:
+ "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_if_False [intro!]:
+ "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
+ by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_while_False [intro!]:
+ "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
+ by (auto simp: equiv_up_to_def)
+
+lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
+ by (induct rule: big_step_induct) auto
+
+lemma equiv_up_to_while_True [intro!,simp]:
+ "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
+ unfolding equiv_up_to_def
+ by (blast dest: while_never)
+
+
+end
\ No newline at end of file
--- a/src/HOL/Library/positivstellensatz.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Library/positivstellensatz.ML Mon Aug 08 16:19:57 2011 -0700
@@ -170,8 +170,8 @@
Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha)
(Thm.implies_intr (cprop_of tha) thb);
-fun prove_hyp tha thb =
- if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb))
+fun prove_hyp tha thb =
+ if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *)
then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
--- a/src/HOL/Orderings.thy Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Orderings.thy Mon Aug 08 16:19:57 2011 -0700
@@ -531,7 +531,7 @@
setup {*
let
-fun prp t thm = (#prop (rep_thm thm) = t);
+fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *)
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = Simplifier.prems_of ss;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 08 16:19:57 2011 -0700
@@ -46,7 +46,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- val {maxidx, ...} = rep_thm induct;
+ val maxidx = Thm.maxidx_of induct;
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
fun prove_casedist_thm (i, (T, t)) =
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Aug 08 16:19:57 2011 -0700
@@ -20,9 +20,6 @@
in map (fn ks => i::ks) is @ is end
else [[]];
-fun prf_of thm =
- Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
@@ -141,7 +138,8 @@
end
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -201,9 +199,10 @@
Proofterm.forall_intr_proof' (Logic.varify_global r)
(AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val prf' = Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
+ (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Aug 08 16:19:57 2011 -0700
@@ -270,7 +270,7 @@
fun lemma thm ct =
let
val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
- val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+ val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
in Thm (Z3_Proof_Tools.compose ccontr th) end
end
--- a/src/HOL/Tools/TFL/rules.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/TFL/rules.ML Mon Aug 08 16:19:57 2011 -0700
@@ -245,9 +245,7 @@
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
- fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
- aconv term_of atm)
- (#hyps(rep_thm th))
+ fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
--- a/src/HOL/Tools/inductive_codegen.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Aug 08 16:19:57 2011 -0700
@@ -581,7 +581,7 @@
(ks @ [SOME k]))) arities));
fun prep_intrs intrs =
- map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
+ map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs;
fun constrain cs [] = []
| constrain cs ((s, xs) :: ys) =
--- a/src/HOL/Tools/inductive_realizer.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Aug 08 16:19:57 2011 -0700
@@ -22,10 +22,8 @@
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
fun prf_of thm =
- let
- val thy = Thm.theory_of_thm thm;
- val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
- in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
+ Reconstruct.proof_of thm
+ |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *)
fun subsets [] = [[]]
| subsets (x::xs) =
--- a/src/HOL/Tools/sat_funcs.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/HOL/Tools/sat_funcs.ML Mon Aug 08 16:19:57 2011 -0700
@@ -153,11 +153,13 @@
fun resolution (c1, hyps1) (c2, hyps2) =
let
val _ =
- if ! trace_sat then
+ if ! trace_sat then (* FIXME !? *)
tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -189,7 +191,7 @@
if !trace_sat then
tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
" (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
else ()
val _ = Unsynchronized.inc counter
in
--- a/src/Provers/hypsubst.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Provers/hypsubst.ML Mon Aug 08 16:19:57 2011 -0700
@@ -116,8 +116,7 @@
(*For the simpset. Adds ALL suitable equalities, even if not first!
No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs bnd th =
- [ if inspect_pair bnd false (Data.dest_eq
- (Data.dest_Trueprop (#prop (rep_thm th))))
+ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
then th RS Data.eq_reflection
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];
--- a/src/Pure/IsaMakefile Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/IsaMakefile Mon Aug 08 16:19:57 2011 -0700
@@ -158,9 +158,9 @@
PIDE/document.ML \
PIDE/isar_document.ML \
Proof/extraction.ML \
+ Proof/proof_checker.ML \
Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML \
- Proof/proofchecker.ML \
Proof/reconstruct.ML \
ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/attrib.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Isar/attrib.ML Mon Aug 08 16:19:57 2011 -0700
@@ -444,6 +444,7 @@
register_config Printer.show_structs_raw #>
register_config Printer.show_question_marks_raw #>
register_config Syntax.ambiguity_level_raw #>
+ register_config Syntax.ambiguity_warnings_raw #>
register_config Syntax_Trans.eta_contract_raw #>
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
--- a/src/Pure/Isar/element.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Isar/element.ML Mon Aug 08 16:19:57 2011 -0700
@@ -266,7 +266,7 @@
val mark_witness = Logic.protect;
fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
+fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
fun map_witness f (Witness witn) = Witness (f witn);
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
--- a/src/Pure/Isar/rule_insts.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Isar/rule_insts.ML Mon Aug 08 16:19:57 2011 -0700
@@ -312,7 +312,7 @@
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
(* Lift and instantiate rule *)
- val {maxidx, ...} = rep_thm st;
+ val maxidx = Thm.maxidx_of st;
val paramTs = map #2 params
and inc = maxidx+1
fun liftvar (Var ((a,j), T)) =
--- a/src/Pure/Proof/extraction.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Proof/extraction.ML Mon Aug 08 16:19:57 2011 -0700
@@ -795,7 +795,7 @@
|> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
- (ProofChecker.thm_of_proof thy'
+ (Proof_Checker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
|> snd
|> fold Code.add_default_eqn def_thms
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Proof/proof_checker.ML Mon Aug 08 16:19:57 2011 -0700
@@ -0,0 +1,145 @@
+(* Title: Pure/Proof/proofchecker.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Simple proof checker based only on the core inference rules
+of Isabelle/Pure.
+*)
+
+signature PROOF_CHECKER =
+sig
+ val thm_of_proof : theory -> Proofterm.proof -> thm
+end;
+
+structure Proof_Checker : PROOF_CHECKER =
+struct
+
+(***** construct a theorem out of a proof term *****)
+
+fun lookup_thm thy =
+ let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+ fn s =>
+ (case Symtab.lookup tab s of
+ NONE => error ("Unknown theorem " ^ quote s)
+ | SOME thm => thm)
+ end;
+
+val beta_eta_convert =
+ Conv.fconv_rule Drule.beta_eta_conversion;
+
+(* equality modulo renaming of type variables *)
+fun is_equal t t' =
+ let
+ val atoms = fold_types (fold_atyps (insert (op =))) t [];
+ val atoms' = fold_types (fold_atyps (insert (op =))) t' []
+ in
+ length atoms = length atoms' andalso
+ map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
+ end;
+
+fun pretty_prf thy vs Hs prf =
+ let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
+ Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
+ in
+ (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
+ Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
+ end;
+
+fun pretty_term thy vs _ t =
+ let val t' = subst_bounds (map Free vs, t)
+ in
+ (Syntax.pretty_term_global thy t',
+ Syntax.pretty_typ_global thy (fastype_of t'))
+ end;
+
+fun appl_error thy prt vs Hs s f a =
+ let
+ val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
+ val (pp_a, pp_aT) = prt thy vs Hs a
+ in
+ error (cat_lines
+ [s,
+ "",
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operator:", Pretty.brk 2, pp_f,
+ Pretty.str " ::", Pretty.brk 1, pp_fT]),
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operand:", Pretty.brk 3, pp_a,
+ Pretty.str " ::", Pretty.brk 1, pp_aT]),
+ ""])
+ end;
+
+fun thm_of_proof thy =
+ let val lookup = lookup_thm thy in
+ fn prf =>
+ let
+ val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
+
+ fun thm_of_atom thm Ts =
+ let
+ val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+ val (fmap, thm') = Thm.varifyT_global' [] thm;
+ val ctye = map (pairself (Thm.ctyp_of thy))
+ (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
+ in
+ Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+ end;
+
+ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+ let
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+ val prop = Thm.prop_of thm;
+ val _ =
+ if is_equal prop prop' then ()
+ else
+ error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+ Syntax.string_of_term_global thy prop ^ "\n\n" ^
+ Syntax.string_of_term_global thy prop');
+ in thm_of_atom thm Ts end
+
+ | thm_of _ _ (PAxm (name, _, SOME Ts)) =
+ thm_of_atom (Thm.axiom thy name) Ts
+
+ | thm_of _ Hs (PBound i) = nth Hs i
+
+ | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
+ let
+ val (x, names') = Name.variant s names;
+ val thm = thm_of ((x, T) :: vs, names') Hs prf
+ in
+ Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
+ end
+
+ | thm_of (vs, names) Hs (prf % SOME t) =
+ let
+ val thm = thm_of (vs, names) Hs prf;
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ in
+ Thm.forall_elim ct thm
+ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
+ end
+
+ | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
+ let
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
+ in
+ Thm.implies_intr ct thm
+ end
+
+ | thm_of vars Hs (prf %% prf') =
+ let
+ val thm = beta_eta_convert (thm_of vars Hs prf);
+ val thm' = beta_eta_convert (thm_of vars Hs prf');
+ in
+ Thm.implies_elim thm thm'
+ handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
+ end
+
+ | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
+
+ | thm_of _ _ _ = error "thm_of_proof: partial proof term";
+
+ in beta_eta_convert (thm_of ([], prf_names) [] prf) end
+ end;
+
+end;
--- a/src/Pure/Proof/proofchecker.ML Mon Aug 08 16:04:58 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: Pure/Proof/proofchecker.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Simple proof checker based only on the core inference rules
-of Isabelle/Pure.
-*)
-
-signature PROOF_CHECKER =
-sig
- val thm_of_proof : theory -> Proofterm.proof -> thm
-end;
-
-structure ProofChecker : PROOF_CHECKER =
-struct
-
-(***** construct a theorem out of a proof term *****)
-
-fun lookup_thm thy =
- let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
- in
- (fn s => case Symtab.lookup tab s of
- NONE => error ("Unknown theorem " ^ quote s)
- | SOME thm => thm)
- end;
-
-val beta_eta_convert =
- Conv.fconv_rule Drule.beta_eta_conversion;
-
-(* equality modulo renaming of type variables *)
-fun is_equal t t' =
- let
- val atoms = fold_types (fold_atyps (insert (op =))) t [];
- val atoms' = fold_types (fold_atyps (insert (op =))) t' []
- in
- length atoms = length atoms' andalso
- map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
- end;
-
-fun pretty_prf thy vs Hs prf =
- let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
- Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
- in
- (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
- Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
- end;
-
-fun pretty_term thy vs _ t =
- let val t' = subst_bounds (map Free vs, t)
- in
- (Syntax.pretty_term_global thy t',
- Syntax.pretty_typ_global thy (fastype_of t'))
- end;
-
-fun appl_error thy prt vs Hs s f a =
- let
- val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
- val (pp_a, pp_aT) = prt thy vs Hs a
- in
- error (cat_lines
- [s,
- "",
- Pretty.string_of (Pretty.block
- [Pretty.str "Operator:", Pretty.brk 2, pp_f,
- Pretty.str " ::", Pretty.brk 1, pp_fT]),
- Pretty.string_of (Pretty.block
- [Pretty.str "Operand:", Pretty.brk 3, pp_a,
- Pretty.str " ::", Pretty.brk 1, pp_aT]),
- ""])
- end;
-
-fun thm_of_proof thy prf =
- let
- val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
- val lookup = lookup_thm thy;
-
- fun thm_of_atom thm Ts =
- let
- val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
- val (fmap, thm') = Thm.varifyT_global' [] thm;
- val ctye = map (pairself (Thm.ctyp_of thy))
- (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
- in
- Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
- end;
-
- fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
- let
- val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
- val {prop, ...} = rep_thm thm;
- val _ = if is_equal prop prop' then () else
- error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
- Syntax.string_of_term_global thy prop ^ "\n\n" ^
- Syntax.string_of_term_global thy prop');
- in thm_of_atom thm Ts end
-
- | thm_of _ _ (PAxm (name, _, SOME Ts)) =
- thm_of_atom (Thm.axiom thy name) Ts
-
- | thm_of _ Hs (PBound i) = nth Hs i
-
- | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
- let
- val (x, names') = Name.variant s names;
- val thm = thm_of ((x, T) :: vs, names') Hs prf
- in
- Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
- end
-
- | thm_of (vs, names) Hs (prf % SOME t) =
- let
- val thm = thm_of (vs, names) Hs prf;
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- in
- Thm.forall_elim ct thm
- handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
- end
-
- | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
- let
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
- in
- Thm.implies_intr ct thm
- end
-
- | thm_of vars Hs (prf %% prf') =
- let
- val thm = beta_eta_convert (thm_of vars Hs prf);
- val thm' = beta_eta_convert (thm_of vars Hs prf');
- in
- Thm.implies_elim thm thm'
- handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
- end
-
- | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
-
- | thm_of _ _ _ = error "thm_of_proof: partial proof term";
-
- in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
-
-end;
--- a/src/Pure/Proof/reconstruct.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Proof/reconstruct.ML Mon Aug 08 16:19:57 2011 -0700
@@ -10,6 +10,7 @@
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
+ val proof_of : thm -> Proofterm.proof
val expand_proof : theory -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
end;
@@ -323,6 +324,10 @@
val prop_of' = Envir.beta_eta_contract oo prop_of0;
val prop_of = prop_of' [];
+fun proof_of thm =
+ reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+
+
(**** expand and reconstruct subproofs ****)
@@ -352,8 +357,9 @@
(case AList.lookup (op =) prfs (a, prop) of
NONE =>
let
- val _ = message ("Reconstructing proof of " ^ a);
- val _ = message (Syntax.string_of_term_global thy prop);
+ val _ =
+ message ("Reconstructing proof of " ^ a ^ "\n" ^
+ Syntax.string_of_term_global thy prop);
val prf' = forall_intr_vfs_prf prop
(reconstruct_proof thy prop (Proofterm.join_proof body));
val (maxidx', prfs', prf) = expand
--- a/src/Pure/ROOT.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/ROOT.ML Mon Aug 08 16:19:57 2011 -0700
@@ -175,7 +175,7 @@
use "Proof/reconstruct.ML";
use "Proof/proof_syntax.ML";
use "Proof/proof_rewrite_rules.ML";
-use "Proof/proofchecker.ML";
+use "Proof/proof_checker.ML";
(*outer syntax*)
use "Isar/token.ML";
--- a/src/Pure/Syntax/syntax.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Syntax/syntax.ML Mon Aug 08 16:19:57 2011 -0700
@@ -16,6 +16,8 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
+ val ambiguity_warnings_raw: Config.raw
+ val ambiguity_warnings: bool Config.T
val read_token: string -> Symbol_Pos.T list * Position.T
val parse_token: Proof.context -> (XML.tree list -> 'a) ->
Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
@@ -193,6 +195,11 @@
val ambiguity_limit =
Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
+val ambiguity_warnings_raw =
+ Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
+val ambiguity_warnings =
+ Config.bool ambiguity_warnings_raw;
+
(* outer syntax token -- with optional YXML content *)
--- a/src/Pure/Syntax/syntax_phases.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Aug 08 16:19:57 2011 -0700
@@ -288,15 +288,17 @@
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val warnings = Config.get ctxt Syntax.ambiguity_warnings;
val _ =
if len <= Config.get ctxt Syntax.ambiguity_level then ()
else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
- else
+ else if warnings then
(Context_Position.if_visible ctxt warning (cat_lines
(("Ambiguous input" ^ Position.str_of pos ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
+ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
+ else ();
val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
@@ -353,6 +355,7 @@
val level = Config.get ctxt Syntax.ambiguity_level;
val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val warnings = Config.get ctxt Syntax.ambiguity_warnings;
val ambig_msg =
if ambiguity > 1 andalso ambiguity <= level then
@@ -381,7 +384,7 @@
report_result ctxt pos
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
else if len = 1 then
- (if ambiguity > level then
+ (if ambiguity > level andalso warnings then
Context_Position.if_visible ctxt warning
"Fortunately, only one parse tree is type correct.\n\
\You may still want to disambiguate your grammar or your input."
--- a/src/Pure/raw_simplifier.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/raw_simplifier.ML Mon Aug 08 16:19:57 2011 -0700
@@ -1197,7 +1197,7 @@
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
val i = 1 + fold Integer.max (map (fn p =>
- find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
+ find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
--- a/src/Pure/simplifier.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Pure/simplifier.ML Mon Aug 08 16:19:57 2011 -0700
@@ -410,7 +410,7 @@
if can Logic.dest_equals (Thm.concl_of thm) then [thm]
else [thm RS reflect] handle THM _ => [];
- fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+ fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
in
empty_ss setsubgoaler asm_simp_tac
setSSolver safe_solver
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Aug 08 16:04:58 2011 -0700
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Aug 08 16:19:57 2011 -0700
@@ -204,6 +204,10 @@
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
+ def string_width(s: String): Float =
+ if (s.isEmpty) 0.0f
+ else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+
val caret_range =
if (text_area.hasFocus) doc_view.caret_range()
else Text.Range(-1)
@@ -230,17 +234,27 @@
range.try_restrict(caret_range) match {
case Some(r) if !r.is_singularity =>
- val astr = new AttributedString(str)
val i = r.start - range.start
val j = r.stop - range.start
+ val s1 = str.substring(0, i)
+ val s2 = str.substring(i, j)
+ val s3 = str.substring(j)
+
+ if (!s1.isEmpty) gfx.drawString(s1, x1, y)
+
+ val astr = new AttributedString(s2)
astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
- gfx.drawString(astr.getIterator, x1, y)
+ astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+ gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+
+ if (!s3.isEmpty)
+ gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+
case _ =>
gfx.drawString(str, x1, y)
}
- x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ x1 += string_width(str)
}
}
w += chunk.width
--- a/src/ZF/Tools/datatype_package.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/ZF/Tools/datatype_package.ML Mon Aug 08 16:19:57 2011 -0700
@@ -339,7 +339,7 @@
end
val constructors =
- map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
+ map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
--- a/src/ZF/Tools/induct_tacs.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/ZF/Tools/induct_tacs.ML Mon Aug 08 16:19:57 2011 -0700
@@ -123,8 +123,7 @@
Syntax.string_of_term_global thy eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o
- #prop o rep_thm) case_eqns;
+ map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
val Const (@{const_name mem}, _) $ _ $ data =
FOLogic.dest_Trueprop (hd (prems_of elim));
--- a/src/ZF/arith_data.ML Mon Aug 08 16:04:58 2011 -0700
+++ b/src/ZF/arith_data.ML Mon Aug 08 16:19:57 2011 -0700
@@ -61,7 +61,7 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
fun is_eq_thm th =
- can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
+ can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
@@ -69,7 +69,7 @@
if t aconv u then NONE
else
let val prems' = filter_out is_eq_thm prems
- val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
+ val goal = Logic.list_implies (map Thm.prop_of prems',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
handle ERROR msg =>