# HG changeset patch # User huffman # Date 1312845597 25200 # Node ID 8eac3858229c671112f4d3becf02774b2ed262ba # Parent 427db4ab3c99b31b51a662b09ba6198c2eaa97d2# Parent 9ee98b584494d08438084571ca5f166d65c2e3ba merged diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/IMP/Big_Step.thy --- 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) \ s' \ (s' = s(x := aval a s))" + by auto subsection "Command Equivalence" diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/IMP/Comp_Rev.thy --- 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 = [] \ (c,s) \ s" by (induct c) auto -lemma assign [simp]: - "(x ::= a,s) \ s' \ (s' = s(x := aval a s))" - by auto +declare assign_simp [simp] lemma ccomp_exec_n: "ccomp c \ (0,s,stk) \^n (isize(ccomp c),t,stk') diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/IMP/Fold.thy --- /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 \ val option" + +(* maybe better as the composition of substitution and the existing simp_const(0) *) +fun simp_const :: "aexp \ tab \ aexp" where +"simp_const (N n) _ = N n" | +"simp_const (V x) t = (case t x of None \ V x | Some k \ N k)" | +"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of + (N n1, N n2) \ N(n1+n2) | (e1',e2') \ Plus e1' e2')" + +definition "approx t s \ (ALL x k. t x = Some k \ 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 \ aval a s = n" + using assms + by (induct a arbitrary: n) + (auto simp: approx_def split: aexp.splits option.splits) + +definition + "merge t1 t2 = (\m. if t1 m = t2 m then t1 m else None)" + +primrec lnames :: "com \ name set" where +"lnames SKIP = {}" | +"lnames (x ::= a) = {x}" | +"lnames (c1; c2) = lnames c1 \ lnames c2" | +"lnames (IF b THEN c1 ELSE c2) = lnames c1 \ lnames c2" | +"lnames (WHILE b DO c) = lnames c" + +primrec "defs" :: "com \ tab \ tab" where +"defs SKIP t = t" | +"defs (x ::= a) t = + (case simp_const a t of N k \ t(x \ k) | _ \ 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 \ approx t2 s \ approx (merge t1 t2) s" + by (fastsimp simp: merge_def approx_def) + +lemma approx_map_le: + "approx t2 s \ t1 \\<^sub>m t2 \ approx t1 s" + by (clarsimp simp: approx_def map_le_def dom_def) + +lemma restrict_map_le [intro!, simp]: "t |` S \\<^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 "\x. (t1 |` S) x = (t |` S) x" + and "\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) \ s' \ approx t s \ 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]: + "\ {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) \ s' \ approx (t |` (-lnames c)) s \ 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: + "\ {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 \ c \ 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)) \ + WHILE b DO c \ 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 = (\_. True)" + by (auto intro!: ext simp: approx_def) + +lemma equiv_sym: + "c \ c' \ c' \ c" + by (auto simp add: equiv_def) + +theorem constant_folding_equiv: + "fold c empty \ 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 \ tab \ 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 (\v)" + by (cases v) auto + +lemma not_B_eq [simp]: "(not b = B v) = (b = B (\v))" + by (cases b) auto + +lemma and_B_eq: + "(and a b = B v) = (a = B False \ \v \ + b = B False \ \v \ + (\v1 v2. a = B v1 \ b = B v2 \ v = v1 \ v2))" + by (rule and.induct) auto + +lemma less_B_eq [simp]: + "(less a b = B v) = (\n1 n2. a = N n1 \ b = N n2 \ v = (n1 < n2))" + by (rule less.induct) auto + +theorem bvalsimp_const_B: +assumes "approx t s" +shows "bsimp_const b t = B v \ 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 \ tab \ tab" where +"bdefs SKIP t = t" | +"bdefs (x ::= a) t = + (case simp_const a t of N k \ t(x \ k) | _ \ 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 \ bdefs c1 t + | B False \ bdefs c2 t + | _ \ 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 \ bfold c1 t + | B False \ bfold c2 t + | _ \ 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 \ SKIP + | _ \ 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) \ s' \ approx t s \ 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 `\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]: + "\ {approx t} c {approx (bdefs c t)}" + by (simp add: hoare_valid_def big_step_pres_approx_b) + +lemma bfold_equiv: + "approx t \ c \ 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 \ IF b THEN c1 ELSE c2 \ + 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)) \ + WHILE b DO c \ + WHILE bsimp_const b (t |` (- lnames c)) + DO bfold c (t |` (- lnames c))" (is "_ \ ?W \ ?W'") + by (auto intro: equiv_up_to_while_weak approx_restrict_inv + simp: bequiv_up_to_def) + hence "approx t \ ?W \ ?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 \ c" + using bfold_equiv [of empty c] + by (simp add: equiv_up_to_True equiv_sym) + + +end diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/IMP/ROOT.ML --- 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" ]; diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/IMP/Sem_Equiv.thy --- /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 \ com \ com \ bool" ("_ \ _ \ _" [60,0,10] 60) +where + "P \ c \ c' \ \s s'. P s \ (c,s) \ s' \ (c',s) \ s'" + +definition + bequiv_up_to :: "assn \ bexp \ bexp \ bool" ("_ \ _ <\> _" [60,0,10] 60) +where + "P \ b <\> b' \ \s. P s \ bval b s = bval b' s" + +lemma equiv_up_to_True: + "((\_. True) \ c \ c') = (c \ c')" + by (simp add: equiv_def equiv_up_to_def) + +lemma equiv_up_to_weaken: + "P \ c \ c' \ (\s. P' s \ P s) \ P' \ c \ c'" + by (simp add: equiv_up_to_def) + +lemma equiv_up_toI: + "(\s s'. P s \ (c, s) \ s' = (c', s) \ s') \ P \ c \ c'" + by (unfold equiv_up_to_def) blast + +lemma equiv_up_toD1: + "P \ c \ c' \ P s \ (c, s) \ s' \ (c', s) \ s'" + by (unfold equiv_up_to_def) blast + +lemma equiv_up_toD2: + "P \ c \ c' \ P s \ (c', s) \ s' \ (c, s) \ s'" + by (unfold equiv_up_to_def) blast + + +lemma equiv_up_to_refl [simp, intro!]: + "P \ c \ c" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_sym: + "(P \ c \ c') = (P \ c' \ c)" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_trans [trans]: + "P \ c \ c' \ P \ c' \ c'' \ P \ c \ c''" + by (auto simp: equiv_up_to_def) + + +lemma bequiv_up_to_refl [simp, intro!]: + "P \ b <\> b" + by (auto simp: bequiv_up_to_def) + +lemma bequiv_up_to_sym: + "(P \ b <\> b') = (P \ b' <\> b)" + by (auto simp: bequiv_up_to_def) + +lemma bequiv_up_to_trans [trans]: + "P \ b <\> b' \ P \ b' <\> b'' \ P \ b <\> b''" + by (auto simp: bequiv_up_to_def) + + +lemma equiv_up_to_hoare: + "P' \ c \ c' \ (\s. P s \ P' s) \ (\ {P} c {Q}) = (\ {P} c' {Q})" + unfolding hoare_valid_def equiv_up_to_def by blast + +lemma equiv_up_to_hoare_eq: + "P \ c \ c' \ (\ {P} c {Q}) = (\ {P} c' {Q})" + by (rule equiv_up_to_hoare) + + +lemma equiv_up_to_semi: + "P \ c \ c' \ Q \ d \ d' \ \ {P} c {Q} \ + P \ (c; d) \ (c'; d')" + by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast + +lemma equiv_up_to_while_lemma: + shows "(d,s) \ s' \ + P \ b <\> b' \ + (\s. P s \ bval b s) \ c \ c' \ + \ {\s. P s \ bval b s} c {P} \ + P s \ + d = WHILE b DO c \ + (WHILE b' DO c', s) \ 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 \ b <\> 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 "(\s. P s \ bval b s) \ c \ c'" by simp + with `bval b s1` `P s1` `(c, s1) \ s2` + have "(c', s1) \ s2" by (simp add: equiv_up_to_def) + moreover + from WhileTrue.prems + have "\ {\s. P s \ bval b s} c {P}" by simp + with `P s1` `bval b s1` `(c, s1) \ s2` + have "P s2" by (simp add: hoare_valid_def) + hence "(WHILE b' DO c', s2) \ 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 \ b <\> b' \ (P s \ bval b s) = (P s \ bval b' s)" + by (auto simp: bequiv_up_to_def) + +lemma equiv_up_to_while: + "P \ b <\> b' \ (\s. P s \ bval b s) \ c \ c' \ + \ {\s. P s \ bval b s} c {P} \ + P \ WHILE b DO c \ 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 \ b <\> b' \ P \ c \ c' \ \ {P} c {P} \ + P \ WHILE b DO c \ 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 \ b <\> b' \ P \ bval b \ c \ c' \ (\s. P s \ \bval b s) \ d \ d' \ + P \ IF b THEN c ELSE d \ IF b' THEN c' ELSE d'" + by (auto simp: bequiv_up_to_def equiv_up_to_def) + +lemma equiv_up_to_if_weak: + "P \ b <\> b' \ P \ c \ c' \ P \ d \ d' \ + P \ IF b THEN c ELSE d \ IF b' THEN c' ELSE d'" + by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken) + +lemma equiv_up_to_if_True [intro!]: + "(\s. P s \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c1" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_if_False [intro!]: + "(\s. P s \ \ bval b s) \ P \ IF b THEN c1 ELSE c2 \ c2" + by (auto simp: equiv_up_to_def) + +lemma equiv_up_to_while_False [intro!]: + "(\s. P s \ \ bval b s) \ P \ WHILE b DO c \ SKIP" + by (auto simp: equiv_up_to_def) + +lemma while_never: "(c, s) \ u \ c \ WHILE (B True) DO c'" + by (induct rule: big_step_induct) auto + +lemma equiv_up_to_while_True [intro!,simp]: + "P \ WHILE B True DO c \ WHILE B True DO SKIP" + unfolding equiv_up_to_def + by (blast dest: while_never) + + +end \ No newline at end of file diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Library/positivstellensatz.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Orderings.thy --- 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; diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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)) = diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/Datatype/datatype_realizer.ML --- 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]))))); diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/TFL/rules.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/inductive_codegen.ML --- 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) = diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/inductive_realizer.ML --- 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) = diff -r 427db4ab3c99 -r 8eac3858229c src/HOL/Tools/sat_funcs.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/Provers/hypsubst.ML --- 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 => []; diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/IsaMakefile --- 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 \ diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Isar/attrib.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 #> diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Isar/element.ML --- 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)); diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Isar/rule_insts.ML --- 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)) = diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Proof/extraction.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Proof/proof_checker.ML --- /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; diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Proof/proofchecker.ML --- 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; diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Proof/reconstruct.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/ROOT.ML --- 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"; diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Syntax/syntax.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 *) diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/Syntax/syntax_phases.ML --- 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." diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/raw_simplifier.ML --- 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) diff -r 427db4ab3c99 -r 8eac3858229c src/Pure/simplifier.ML --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/Tools/jEdit/src/text_area_painter.scala --- 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 diff -r 427db4ab3c99 -r 8eac3858229c src/ZF/Tools/datatype_package.ML --- 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); diff -r 427db4ab3c99 -r 8eac3858229c src/ZF/Tools/induct_tacs.ML --- 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)); diff -r 427db4ab3c99 -r 8eac3858229c src/ZF/arith_data.ML --- 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 =>