--- a/src/HOL/Decision_Procs/Reflective_Field.thy Sun Dec 03 19:09:42 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Sun Dec 03 22:28:19 2017 +0100
@@ -5,7 +5,7 @@
*)
theory Reflective_Field
-imports "~~/src/HOL/Decision_Procs/Commutative_Ring"
+ imports Commutative_Ring
begin
datatype fexpr =
@@ -18,29 +18,28 @@
| FDiv fexpr fexpr
| FPow fexpr nat
-fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
- "nth_el [] n = \<zero>"
-| "nth_el (x # xs) 0 = x"
-| "nth_el (x # xs) (Suc n) = nth_el xs n"
+fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a"
+ where
+ "nth_el [] n = \<zero>"
+ | "nth_el (x # xs) 0 = x"
+ | "nth_el (x # xs) (Suc n) = nth_el xs n"
-lemma (in field) nth_el_Cons:
- "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))"
+lemma (in field) nth_el_Cons: "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))"
by (cases n) simp_all
-lemma (in field) nth_el_closed [simp]:
- "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R"
+lemma (in field) nth_el_closed [simp]: "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R"
by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def)
primrec (in field) feval :: "'a list \<Rightarrow> fexpr \<Rightarrow> 'a"
-where
- "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>"
-| "feval xs (FVar n) = nth_el xs n"
-| "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b"
-| "feval xs (FSub a b) = feval xs a \<ominus> feval xs b"
-| "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
-| "feval xs (FNeg a) = \<ominus> feval xs a"
-| "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
-| "feval xs (FPow a n) = feval xs a (^) n"
+ where
+ "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>"
+ | "feval xs (FVar n) = nth_el xs n"
+ | "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b"
+ | "feval xs (FSub a b) = feval xs a \<ominus> feval xs b"
+ | "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
+ | "feval xs (FNeg a) = \<ominus> feval xs a"
+ | "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
+ | "feval xs (FPow a n) = feval xs a (^) n"
lemma (in field) feval_Cnst:
"feval xs (FCnst 0) = \<zero>"
@@ -75,29 +74,29 @@
case (PExpr1 e')
then show ?thesis
apply (cases e')
- apply simp_all
- apply (erule assms)+
+ apply simp_all
+ apply (erule assms)+
done
next
case (PExpr2 e')
then show ?thesis
apply (cases e')
- apply simp_all
- apply (erule assms)+
+ apply simp_all
+ apply (erule assms)+
done
qed
lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases]
fun (in field) peval :: "'a list \<Rightarrow> pexpr \<Rightarrow> 'a"
-where
- "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>"
-| "peval xs (PExpr1 (PVar n)) = nth_el xs n"
-| "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b"
-| "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
-| "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
-| "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
-| "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n"
+ where
+ "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>"
+ | "peval xs (PExpr1 (PVar n)) = nth_el xs n"
+ | "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b"
+ | "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
+ | "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
+ | "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
+ | "peval xs (PExpr2 (PPow a n)) = peval xs a (^) n"
lemma (in field) peval_Cnst:
"peval xs (PExpr1 (PCnst 0)) = \<zero>"
@@ -113,44 +112,44 @@
by (induct e and e1 and e2) simp_all
definition npepow :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr"
-where
- "npepow e n =
- (if n = 0 then PExpr1 (PCnst 1)
- else if n = 1 then e
- else (case e of
- PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n))
- | _ \<Rightarrow> PExpr2 (PPow e n)))"
+ where "npepow e n =
+ (if n = 0 then PExpr1 (PCnst 1)
+ else if n = 1 then e
+ else
+ (case e of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n))
+ | _ \<Rightarrow> PExpr2 (PPow e n)))"
lemma (in field) npepow_correct:
"in_carrier xs \<Longrightarrow> peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))"
- by (cases e rule: pexpr_cases)
- (simp_all add: npepow_def)
+ by (cases e rule: pexpr_cases) (simp_all add: npepow_def)
fun npemul :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
-where
- "npemul x y = (case x of
- PExpr1 (PCnst c) \<Rightarrow>
- if c = 0 then x
- else if c = 1 then y else
- (case y of
- PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d))
- | _ \<Rightarrow> PExpr2 (PMul x y))
- | PExpr2 (PPow e1 n) \<Rightarrow>
- (case y of
- PExpr2 (PPow e2 m) \<Rightarrow>
- if n = m then npepow (npemul e1 e2) n
- else PExpr2 (PMul x y)
- | PExpr1 (PCnst d) \<Rightarrow>
- if d = 0 then y
- else if d = 1 then x
- else PExpr2 (PMul x y)
+ where "npemul x y =
+ (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then x
+ else if c = 1 then y else
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d))
| _ \<Rightarrow> PExpr2 (PMul x y))
- | _ \<Rightarrow> (case y of
- PExpr1 (PCnst d) \<Rightarrow>
- if d = 0 then y
- else if d = 1 then x
- else PExpr2 (PMul x y)
- | _ \<Rightarrow> PExpr2 (PMul x y)))"
+ | PExpr2 (PPow e1 n) \<Rightarrow>
+ (case y of
+ PExpr2 (PPow e2 m) \<Rightarrow>
+ if n = m then npepow (npemul e1 e2) n
+ else PExpr2 (PMul x y)
+ | PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then y
+ else if d = 1 then x
+ else PExpr2 (PMul x y)
+ | _ \<Rightarrow> PExpr2 (PMul x y))
+ | _ \<Rightarrow>
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then y
+ else if d = 1 then x
+ else PExpr2 (PMul x y)
+ | _ \<Rightarrow> PExpr2 (PMul x y)))"
lemma (in field) npemul_correct:
"in_carrier xs \<Longrightarrow> peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))"
@@ -160,104 +159,101 @@
proof (cases x y rule: pexpr_cases2)
case (PPow_PPow e n e' m)
then show ?thesis
- by (simp add: 1 npepow_correct nat_pow_distr
- npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"]
- del: npemul.simps)
+ by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distr
+ npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"])
qed simp_all
qed
declare npemul.simps [simp del]
definition npeadd :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
-where
- "npeadd x y = (case x of
- PExpr1 (PCnst c) \<Rightarrow>
- if c = 0 then y else
- (case y of
- PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d))
- | _ \<Rightarrow> PExpr1 (PAdd x y))
- | _ \<Rightarrow> (case y of
- PExpr1 (PCnst d) \<Rightarrow>
- if d = 0 then x
- else PExpr1 (PAdd x y)
- | _ \<Rightarrow> PExpr1 (PAdd x y)))"
+ where "npeadd x y =
+ (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then y
+ else
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d))
+ | _ \<Rightarrow> PExpr1 (PAdd x y))
+ | _ \<Rightarrow>
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then x
+ else PExpr1 (PAdd x y)
+ | _ \<Rightarrow> PExpr1 (PAdd x y)))"
lemma (in field) npeadd_correct:
"in_carrier xs \<Longrightarrow> peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))"
by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def)
definition npesub :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
-where
- "npesub x y = (case y of
- PExpr1 (PCnst d) \<Rightarrow>
- if d = 0 then x else
- (case x of
- PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d))
- | _ \<Rightarrow> PExpr1 (PSub x y))
- | _ \<Rightarrow> (case x of
- PExpr1 (PCnst c) \<Rightarrow>
- if c = 0 then PExpr1 (PNeg y)
- else PExpr1 (PSub x y)
- | _ \<Rightarrow> PExpr1 (PSub x y)))"
+ where "npesub x y =
+ (case y of
+ PExpr1 (PCnst d) \<Rightarrow>
+ if d = 0 then x
+ else
+ (case x of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d))
+ | _ \<Rightarrow> PExpr1 (PSub x y))
+ | _ \<Rightarrow>
+ (case x of
+ PExpr1 (PCnst c) \<Rightarrow>
+ if c = 0 then PExpr1 (PNeg y)
+ else PExpr1 (PSub x y)
+ | _ \<Rightarrow> PExpr1 (PSub x y)))"
lemma (in field) npesub_correct:
"in_carrier xs \<Longrightarrow> peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))"
by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def)
definition npeneg :: "pexpr \<Rightarrow> pexpr"
-where
- "npeneg e = (case e of
- PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c))
- | _ \<Rightarrow> PExpr1 (PNeg e))"
+ where "npeneg e =
+ (case e of
+ PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c))
+ | _ \<Rightarrow> PExpr1 (PNeg e))"
-lemma (in field) npeneg_correct:
- "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))"
+lemma (in field) npeneg_correct: "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))"
by (cases e rule: pexpr_cases) (simp_all add: npeneg_def)
lemma option_pair_cases [case_names None Some]:
- assumes
- "x = None \<Longrightarrow> P"
- "\<And>p q. x = Some (p, q) \<Longrightarrow> P"
- shows P
+ obtains (None) "x = None" | (Some) p q where "x = Some (p, q)"
proof (cases x)
case None
- then show ?thesis by (rule assms)
+ then show ?thesis by (rule that)
next
case (Some r)
then show ?thesis
- apply (cases r)
- apply simp
- by (rule assms)
+ by (cases r, simp) (rule that)
qed
-fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat * pexpr) option"
-where
- "isin e n (PExpr2 (PMul e1 e2)) m =
- (case isin e n e1 m of
+fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat \<times> pexpr) option"
+ where
+ "isin e n (PExpr2 (PMul e1 e2)) m =
+ (case isin e n e1 m of
Some (k, e3) \<Rightarrow>
if k = 0 then Some (0, npemul e3 (npepow e2 m))
- else (case isin e k e2 m of
+ else
+ (case isin e k e2 m of
Some (l, e4) \<Rightarrow> Some (l, npemul e3 e4)
| None \<Rightarrow> Some (k, npemul e3 (npepow e2 m)))
- | None \<Rightarrow> (case isin e n e2 m of
- Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3)
- | None \<Rightarrow> None))"
-| "isin e n (PExpr2 (PPow e' k)) m =
- (if k = 0 then None else isin e n e' (k * m))"
-| "isin (PExpr1 e) n (PExpr1 e') m =
- (if e = e' then
- if n >= m then Some (n - m, PExpr1 (PCnst 1))
+ | None \<Rightarrow>
+ (case isin e n e2 m of
+ Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3)
+ | None \<Rightarrow> None))"
+ | "isin e n (PExpr2 (PPow e' k)) m =
+ (if k = 0 then None else isin e n e' (k * m))"
+ | "isin (PExpr1 e) n (PExpr1 e') m =
+ (if e = e' then
+ if n \<ge> m then Some (n - m, PExpr1 (PCnst 1))
else Some (0, npepow (PExpr1 e) (m - n))
- else None)"
-| "isin (PExpr2 e) n (PExpr1 e') m = None"
+ else None)"
+ | "isin (PExpr2 e) n (PExpr1 e') m = None"
lemma (in field) isin_correct:
assumes "in_carrier xs"
- and "isin e n e' m = Some (p, e'')"
- shows
- "peval xs (PExpr2 (PPow e' m)) =
- peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))"
- "p \<le> n"
+ and "isin e n e' m = Some (p, e'')"
+ shows "peval xs (PExpr2 (PPow e' m)) = peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))"
+ and "p \<le> n"
using assms
by (induct e n e' m arbitrary: p e'' rule: isin.induct)
(force
@@ -268,38 +264,37 @@
lemma (in field) isin_correct':
"in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow>
- peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''"
+ peval xs e' = peval xs e (^) (n - p) \<otimes> peval xs e''"
"in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n"
- using isin_correct [where m=1]
- by simp_all
+ using isin_correct [where m = 1] by simp_all
fun split_aux :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr"
-where
- "split_aux (PExpr2 (PMul e1 e2)) n e =
- (let
- (left1, common1, right1) = split_aux e1 n e;
- (left2, common2, right2) = split_aux e2 n right1
- in (npemul left1 left2, npemul common1 common2, right2))"
-| "split_aux (PExpr2 (PPow e' m)) n e =
- (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e)
- else split_aux e' (m * n) e)"
-| "split_aux (PExpr1 e') n e =
- (case isin (PExpr1 e') n e 1 of
- Some (m, e'') \<Rightarrow>
- (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'')
- else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e''))
- | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))"
+ where
+ "split_aux (PExpr2 (PMul e1 e2)) n e =
+ (let
+ (left1, common1, right1) = split_aux e1 n e;
+ (left2, common2, right2) = split_aux e2 n right1
+ in (npemul left1 left2, npemul common1 common2, right2))"
+ | "split_aux (PExpr2 (PPow e' m)) n e =
+ (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e)
+ else split_aux e' (m * n) e)"
+ | "split_aux (PExpr1 e') n e =
+ (case isin (PExpr1 e') n e 1 of
+ Some (m, e'') \<Rightarrow>
+ (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'')
+ else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e''))
+ | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))"
-hide_const Left Right
+hide_const Left Right (* FIXME !? *)
-abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
- "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)"
+abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+ where "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)"
-abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
- "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))"
+abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+ where "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))"
-abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr" where
- "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))"
+abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
+ where "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))"
lemma split_aux_induct [case_names 1 2 3]:
assumes I1: "\<And>e1 e2 n e. P e1 n e \<Longrightarrow> P e2 n (snd (snd (split_aux e1 n e))) \<Longrightarrow>
@@ -321,11 +316,11 @@
lemma (in field) split_aux_correct:
"in_carrier xs \<Longrightarrow>
- peval xs (PExpr2 (PPow e\<^sub>1 n)) =
- peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
+ peval xs (PExpr2 (PPow e\<^sub>1 n)) =
+ peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
"in_carrier xs \<Longrightarrow>
- peval xs e\<^sub>2 =
- peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
+ peval xs e\<^sub>2 =
+ peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
(auto simp add: split_beta
nat_pow_distr nat_pow_pow nat_pow_mult m_ac
@@ -334,81 +329,78 @@
lemma (in field) split_aux_correct':
"in_carrier xs \<Longrightarrow>
- peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
+ peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
"in_carrier xs \<Longrightarrow>
- peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
- using split_aux_correct [where n=1]
- by simp_all
+ peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
+ using split_aux_correct [where n = 1] by simp_all
fun fnorm :: "fexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list"
-where
- "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])"
-| "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])"
-| "fnorm (FAdd e1 e2) =
- (let
- (xn, xd, xc) = fnorm e1;
- (yn, yd, yc) = fnorm e2;
- (left, common, right) = split_aux xd 1 yd
- in
- (npeadd (npemul xn right) (npemul yn left),
- npemul left (npemul right common),
- List.union xc yc))"
-| "fnorm (FSub e1 e2) =
- (let
- (xn, xd, xc) = fnorm e1;
- (yn, yd, yc) = fnorm e2;
- (left, common, right) = split_aux xd 1 yd
- in
- (npesub (npemul xn right) (npemul yn left),
- npemul left (npemul right common),
- List.union xc yc))"
-| "fnorm (FMul e1 e2) =
- (let
- (xn, xd, xc) = fnorm e1;
- (yn, yd, yc) = fnorm e2;
- (left1, common1, right1) = split_aux xn 1 yd;
- (left2, common2, right2) = split_aux yn 1 xd
- in
- (npemul left1 left2,
- npemul right2 right1,
- List.union xc yc))"
-| "fnorm (FNeg e) =
- (let (n, d, c) = fnorm e
- in (npeneg n, d, c))"
-| "fnorm (FDiv e1 e2) =
- (let
- (xn, xd, xc) = fnorm e1;
- (yn, yd, yc) = fnorm e2;
- (left1, common1, right1) = split_aux xn 1 yn;
- (left2, common2, right2) = split_aux xd 1 yd
- in
- (npemul left1 right2,
- npemul left2 right1,
- List.insert yn (List.union xc yc)))"
-| "fnorm (FPow e m) =
- (let (n, d, c) = fnorm e
- in (npepow n m, npepow d m, c))"
+ where
+ "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])"
+ | "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])"
+ | "fnorm (FAdd e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left, common, right) = split_aux xd 1 yd
+ in
+ (npeadd (npemul xn right) (npemul yn left),
+ npemul left (npemul right common),
+ List.union xc yc))"
+ | "fnorm (FSub e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left, common, right) = split_aux xd 1 yd
+ in
+ (npesub (npemul xn right) (npemul yn left),
+ npemul left (npemul right common),
+ List.union xc yc))"
+ | "fnorm (FMul e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left1, common1, right1) = split_aux xn 1 yd;
+ (left2, common2, right2) = split_aux yn 1 xd
+ in
+ (npemul left1 left2,
+ npemul right2 right1,
+ List.union xc yc))"
+ | "fnorm (FNeg e) =
+ (let (n, d, c) = fnorm e
+ in (npeneg n, d, c))"
+ | "fnorm (FDiv e1 e2) =
+ (let
+ (xn, xd, xc) = fnorm e1;
+ (yn, yd, yc) = fnorm e2;
+ (left1, common1, right1) = split_aux xn 1 yn;
+ (left2, common2, right2) = split_aux xd 1 yd
+ in
+ (npemul left1 right2,
+ npemul left2 right1,
+ List.insert yn (List.union xc yc)))"
+ | "fnorm (FPow e m) =
+ (let (n, d, c) = fnorm e
+ in (npepow n m, npepow d m, c))"
-abbreviation Num :: "fexpr \<Rightarrow> pexpr" where
- "Num e \<equiv> fst (fnorm e)"
+abbreviation Num :: "fexpr \<Rightarrow> pexpr"
+ where "Num e \<equiv> fst (fnorm e)"
-abbreviation Denom :: "fexpr \<Rightarrow> pexpr" where
- "Denom e \<equiv> fst (snd (fnorm e))"
+abbreviation Denom :: "fexpr \<Rightarrow> pexpr"
+ where "Denom e \<equiv> fst (snd (fnorm e))"
-abbreviation Cond :: "fexpr \<Rightarrow> pexpr list" where
- "Cond e \<equiv> snd (snd (fnorm e))"
+abbreviation Cond :: "fexpr \<Rightarrow> pexpr list"
+ where "Cond e \<equiv> snd (snd (fnorm e))"
primrec (in field) nonzero :: "'a list \<Rightarrow> pexpr list \<Rightarrow> bool"
-where
- "nonzero xs [] = True"
-| "nonzero xs (p # ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
+ where
+ "nonzero xs [] \<longleftrightarrow> True"
+ | "nonzero xs (p # ps) \<longleftrightarrow> peval xs p \<noteq> \<zero> \<and> nonzero xs ps"
-lemma (in field) nonzero_singleton:
- "nonzero xs [p] = (peval xs p \<noteq> \<zero>)"
+lemma (in field) nonzero_singleton: "nonzero xs [p] = (peval xs p \<noteq> \<zero>)"
by simp
-lemma (in field) nonzero_append:
- "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)"
+lemma (in field) nonzero_append: "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)"
by (induct ps) simp_all
lemma (in field) nonzero_idempotent:
@@ -426,12 +418,13 @@
lemma (in field) fnorm_correct:
assumes "in_carrier xs"
- and "nonzero xs (Cond e)"
+ and "nonzero xs (Cond e)"
shows "feval xs e = peval xs (Num e) \<oslash> peval xs (Denom e)"
- and "peval xs (Denom e) \<noteq> \<zero>"
+ and "peval xs (Denom e) \<noteq> \<zero>"
using assms
proof (induct e)
- case (FCnst c) {
+ case (FCnst c)
+ {
case 1
show ?case by simp
next
@@ -439,7 +432,8 @@
show ?case by simp
}
next
- case (FVar n) {
+ case (FVar n)
+ {
case 1
then show ?case by simp
next
@@ -448,21 +442,17 @@
}
next
case (FAdd e1 e2)
- note split = split_aux_correct' [where xs=xs and
- e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
{
case 1
let ?left = "peval xs (Left (Denom e1) (Denom e2))"
let ?common = "peval xs (Common (Denom e1) (Denom e2))"
let ?right = "peval xs (Right (Denom e1) (Denom e2))"
- from 1 FAdd
- have "feval xs (FAdd e1 e2) =
+ from 1 FAdd have "feval xs (FAdd e1 e2) =
(?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<oplus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
(?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
- by (simp add: split_beta split nonzero_union
- add_frac_eq r_distr m_ac)
- also from 1 FAdd have "\<dots> =
- peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))"
+ by (simp add: split_beta split nonzero_union add_frac_eq r_distr m_ac)
+ also from 1 FAdd have "\<dots> = peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))"
by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff)
finally show ?case .
next
@@ -472,8 +462,7 @@
}
next
case (FSub e1 e2)
- note split = split_aux_correct' [where xs=xs and
- e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
{
case 1
let ?left = "peval xs (Left (Denom e1) (Denom e2))"
@@ -483,10 +472,8 @@
have "feval xs (FSub e1 e2) =
(?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<ominus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
(?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
- by (simp add: split_beta split nonzero_union
- diff_frac_eq r_diff_distr m_ac)
- also from 1 FSub have "\<dots> =
- peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))"
+ by (simp add: split_beta split nonzero_union diff_frac_eq r_diff_distr m_ac)
+ also from 1 FSub have "\<dots> = peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))"
by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff)
finally show ?case .
next
@@ -497,10 +484,8 @@
next
case (FMul e1 e2)
note split =
- split_aux_correct' [where xs=xs and
- e\<^sub>1="Num e1" and e\<^sub>2="Denom e2"]
- split_aux_correct' [where xs=xs and
- e\<^sub>1="Num e2" and e\<^sub>2="Denom e1"]
+ split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Denom e2"]
+ split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e2" and e\<^sub>2 = "Denom e1"]
{
case 1
let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))"
@@ -509,14 +494,12 @@
let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))"
let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))"
let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))"
- from 1 FMul
- have "feval xs (FMul e1 e2) =
+ from 1 FMul have "feval xs (FMul e1 e2) =
((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?left\<^sub>2)) \<oslash>
((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?right\<^sub>2 \<otimes> ?right\<^sub>1))"
by (simp add: split_beta split nonzero_union
nonzero_divide_divide_eq_left m_ac)
- also from 1 FMul have "\<dots> =
- peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))"
+ also from 1 FMul have "\<dots> = peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))"
by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
finally show ?case .
next
@@ -538,10 +521,8 @@
next
case (FDiv e1 e2)
note split =
- split_aux_correct' [where xs=xs and
- e\<^sub>1="Num e1" and e\<^sub>2="Num e2"]
- split_aux_correct' [where xs=xs and
- e\<^sub>1="Denom e1" and e\<^sub>2="Denom e2"]
+ split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Num e2"]
+ split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
{
case 1
let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))"
@@ -556,8 +537,7 @@
((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>2 \<otimes> ?right\<^sub>1))"
by (simp add: split_beta split nonzero_union nonzero_insert
nonzero_divide_divide_eq m_ac)
- also from 1 FDiv have "\<dots> =
- peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))"
+ also from 1 FDiv have "\<dots> = peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))"
by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
finally show ?case .
next
@@ -580,16 +560,15 @@
lemma (in field) feval_eq0:
assumes "in_carrier xs"
- and "fnorm e = (n, d, c)"
- and "nonzero xs c"
- and "peval xs n = \<zero>"
+ and "fnorm e = (n, d, c)"
+ and "nonzero xs c"
+ and "peval xs n = \<zero>"
shows "feval xs e = \<zero>"
- using assms fnorm_correct [of xs e]
- by simp
+ using assms fnorm_correct [of xs e] by simp
lemma (in field) fexpr_in_carrier:
assumes "in_carrier xs"
- and "nonzero xs (Cond e)"
+ and "nonzero xs (Cond e)"
shows "feval xs e \<in> carrier R"
using assms
proof (induct e)
@@ -610,8 +589,8 @@
lemma (in field) feval_eq:
assumes "in_carrier xs"
- and "fnorm (FSub e e') = (n, d, c)"
- and "nonzero xs c"
+ and "fnorm (FSub e e') = (n, d, c)"
+ and "nonzero xs c"
shows "(feval xs e = feval xs e') = (peval xs n = \<zero>)"
proof -
from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')"
@@ -940,7 +919,8 @@
end
\<close>
-context field begin
+context field
+begin
local_setup \<open>
Local_Theory.declaration {syntax = false, pervasive = false}