1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Wed Mar 06 09:43:41 2013 +0100
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Mon Mar 18 10:46:37 2013 +0100
1.3 @@ -11,7 +11,7 @@
1.4 the style of GCD_Poly.thy has been adapted to the function package.
1.5 *}
1.6
1.7 -(* WN130304 see Algebra/poly/LongDiv.thy: lcoeff_def*)
1.8 +(* WN130304.TODO see Algebra/poly/LongDiv.thy: lcoeff_def*)
1.9 (*---------------------------------------------------------------------------------------------
1.10 declare [[simp_trace_depth_limit = 99]]
1.11 declare [[simp_trace = true]]
1.12 @@ -644,12 +644,12 @@
1.13 in
1.14 if rest = [] then True else
1.15 if quot \<noteq> 0 & List.length ds \<le> List.length rest then ds dvd_up rest else False)"
1.16 -(*using [[show_types = true]]*)
1.17 apply pat_completeness
1.18 apply simp
1.19 defer
1.20 apply simp
1.21 (*---------------------------------------------------------------------------------------------
1.22 + FINALLY WE HAVE TO SHOW THE COMPATIBILITY OF THE TWO EQUATIONS
1.23 1. \<And>(d\<Colon>int) (p\<Colon>int) (ds\<Colon>int list) ps\<Colon>int list.
1.24 ([d], [p]) = (ds, ps) \<Longrightarrow>
1.25 (if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) then True else False) =
1.26 @@ -660,66 +660,69 @@
1.27 in if rest = [] then True
1.28 else if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)
1.29 ---------------------------------------------------------------------------------------------*)
1.30 -(*apply simp*)
1.31 -(*apply (subst Product_Type.Pair_eq) ???*)
1.32 sorry
1.33
1.34 -find_theorems "_ \<and> _ = _ \<and> _"
1.35 -
1.36 -lemma d000: "ds = [d] \<and> ps = [p] \<longrightarrow> replicate (length ps - length ds) (0\<Colon>int) @ ds = [d]"
1.37 -by simp
1.38 -thm d000
1.39 -
1.40 -lemma quot: "([d] mult_ups ((lcoeff [p]) div2 (lcoeff [d]))) = [p]"
1.41 -(*by simp ..loops GOON*)
1.42 -sorry
1.43 -
1.44 -lemma lem\<^isub>_1: "\<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) \<and> d \<noteq> 0 \<and> p \<noteq> 0 \<longrightarrow>
1.45 - drop_lc0 ([p] minus_up (d000 mult_ups quot)) = []"
1.46 -sorry
1.47 -
1.48 -
1.49 -lemma pat_compatibility [case_names equ\<^isub>1_true equ\<^isub>1_false]:
1.50 - fixes d p :: int and ds ps :: "unipoly"
1.51 +(*FINALLY WE HAVE TO SHOW THE COMPATIBILITY OF THE TWO EQUATIONS*)
1.52 +lemma pat_compatibility:
1.53 + fixes d p :: int and ds ps rest :: "unipoly"
1.54 assumes args_equal: "([d], [p]) = (ds, ps)" and not_zero: "d \<noteq> 0 \<and> p \<noteq> 0"
1.55 - assumes equ\<^isub>1_true: " \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int)"
1.56 - assumes equ\<^isub>1_false: "\<not> (\<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int))"
1.57 - shows "(if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) then True else False) \<equiv>
1.58 + assumes DELETE: "foo_sumC = body1"
1.59 + shows
1.60 + "(if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = 0 then True else False) =
1.61 (let ds = drop_lc0 ds; ps = drop_lc0 ps;
1.62 d000 = replicate (length ps - length ds) (0\<Colon>int) @ ds;
1.63 quot = lcoeff ps div2 lcoeff d000;
1.64 rest = drop_lc0 (ps minus_up (d000 div_ups quot))
1.65 in if rest = [] then True else
1.66 - if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"
1.67 - (is "?equ\<^isub>1 \<equiv> ?equ\<^isub>2")
1.68 + if quot \<noteq> 0 \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"
1.69 + (* using the assumptions reachable is only ^^^^^^^^^^^^^^^^^^^^^^^ *)
1.70 + (is "?body\<^isub>1 = ?body\<^isub>2")
1.71 proof -
1.72 - have args_equal': "[d] = ds \<and> [p] = ps" using args_equal by auto (*(rule Pair_eq) ?!?*)
1.73 - assume equ\<^isub>2: "?equ\<^isub>2"
1.74 - have equ\<^isub>2':
1.75 - "let d000 = replicate (length [p] - length [d]) (0\<Colon>int) @ [d];
1.76 - quot = lcoeff [p] div2 lcoeff d000;
1.77 - rest = drop_lc0 ([p] minus_up (d000 div_ups quot))
1.78 - in if rest = [] then True else
1.79 - if quot \<noteq> (0\<Colon>int) \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False"
1.80 - using args_equal' equ\<^isub>2 (*by auto*)
1.81 - proof -
1.82 - from not_zero have 1: "[d] = drop_lc0 [d]" by auto
1.83 - from not_zero have 2: "[p] = drop_lc0 [p]" by auto
1.84 -(*
1.85 - from equ\<^isub>1_true have ?equ\<^isub>1 by auto
1.86 - from args_equal' equ\<^isub>1_false have "~ ?equ\<^isub>2"
1.87 - proof -
1.88 -*)
1.89 + have "ds = [d]" and "ps = [p]" using args_equal by auto
1.90 + -- "required by hypsubst: assume 'ds = [d] \<Longrightarrow> ps = [p]' creates ((ds = [d] \<Longrightarrow> ps = [p])) \<Longrightarrow>"
1.91 + have simp1_ds: "drop_lc0 [d] = [d]" using not_zero by auto
1.92 + have simp1_ps: "drop_lc0 [p] = [p]" using not_zero by auto
1.93 + have simp2_body2: "drop_lc0 ([p] minus_up ([d] div_ups quot)) \<noteq> []" sorry
1.94 + have simp_body2: "True" sorry
1.95 + from `ds = [d]` `ps = [p]` have simp_body2: "?body\<^isub>2 = dvd_up_sumC (ds, rest)"
1.96 + proof -
1.97 + have "?body\<^isub>2 =
1.98 + (let quot = lcoeff [p] div2 lcoeff [d];
1.99 + rest = drop_lc0 ([p] minus_up ([d] div_ups quot))
1.100 + in if rest = [] then True else
1.101 + if quot \<noteq> 0 \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False)"
1.102 + using `ds = [d]` `ps = [p]`
1.103 + by (hypsubst, subst simp1_ds, subst simp1_ps, simp add: Let_def)
1.104 + also have "\<dots> = dvd_up_sumC (ds, rest)"
1.105 + using simp2_body2
1.106 + sorry
1.107 + finally show ?thesis .
1.108 + qed
1.109 + from simp_body2 DELETE show ?thesis sorry
1.110 +qed
1.111 +
1.112 +ML {* 1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1 *}
1.113 +
1.114 +(*---------------------------------------------------------------------------------------------
1.115 +declare [[simp_trace_depth_limit = 99]]
1.116 +declare [[simp_trace = true]]
1.117 +lemma trial:
1.118 + assumes "[d] = ds \<Longrightarrow> [p] = ps"
1.119 + and "(let d000 = replicate (length ps - length ds) (0\<Colon>int) @ ds;
1.120 + quot = lcoeff ps div2 lcoeff d000;
1.121 + rest = drop_lc0 (ps minus_up (d000 div_ups quot))
1.122 + in if rest = [] then True else
1.123 + if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"
1.124 + shows "(let d000 = replicate (length [p] - length [d]) (0\<Colon>int) @ [d];
1.125 + quot = lcoeff [p] div2 lcoeff d000;
1.126 + rest = drop_lc0 ([p] minus_up (d000 div_ups quot))
1.127 + in if rest = [] then True else
1.128 + if quot \<noteq> (0\<Colon>int) \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False)"
1.129 +
1.130 oops
1.131 +---------------------------------------------------------------------------------------------*)
1.132
1.133 -ML {*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*}
1.134
1.135 -value "replicate 5 (0::int)"
1.136 -value "-7 div2 (0::int)"
1.137 -value "[0, 0, 0] div_ups (0::int)"
1.138 -value "[1, -2, 3] minus_up [0, 0, 0]"
1.139 -
1.140 -value "xxx"
1.141 (*---------------------------------------------------------------------------------------------
1.142 (*
1.143 value "[2, 3] dvd_up [8, 22, 15] = True"