45 "--------------------- NTH ---------------------------------------------------"; |
45 "--------------------- NTH ---------------------------------------------------"; |
46 "--------------------- NTH ---------------------------------------------------"; |
46 "--------------------- NTH ---------------------------------------------------"; |
47 val ctxt = Proof_Context.init_global @{theory} |
47 val ctxt = Proof_Context.init_global @{theory} |
48 val prog_expr = get_rls @{context} "prog_expr" |
48 val prog_expr = get_rls @{context} "prog_expr" |
49 |
49 |
50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]"; |
50 val t = TermC.parse_test @{context} "NTH 1 [a,b,c,d,e]"; |
51 TermC.atomty t; |
51 TermC.atomty t; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
52 val thm = Thm.prop_of @{thm NTH_NIL}; |
53 TermC.atomty thm; |
53 TermC.atomty thm; |
54 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t; |
54 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t; |
55 if UnparseC.term t' = "a" then () |
55 if UnparseC.term t' = "a" then () |
56 else error "NTH 1 [a,b,c,d,e] = a ..changed"; |
56 else error "NTH 1 [a,b,c,d,e] = a ..changed"; |
57 |
57 |
58 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |
58 val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]"; |
59 case TermC.str2term "NTH 3 [a,b,c,d,e]" of |
59 case TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]" of |
60 Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $ |
60 Const (\<^const_name>\<open>NTH\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $ |
61 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $ |
61 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("a", _) $ |
62 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ |
62 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ |
63 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $ |
63 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("c", _) $ |
64 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $ |
64 (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $ |
69 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t; |
69 val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t; |
70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () |
70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () |
71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed"; |
71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed"; |
72 |
72 |
73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *) |
73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *) |
74 val t = TermC.str2term "NTH 3 [a,b,c,d,e]"; |
74 val t = TermC.parse_test @{context} "NTH 3 [a,b,c,d,e]"; |
75 TermC.atomty t; |
75 TermC.atomty t; |
76 |
76 |
77 val SOME (t', _) = rewrite_set_ ctxt false prog_expr t; |
77 val SOME (t', _) = rewrite_set_ ctxt false prog_expr t; |
78 if UnparseC.term t' = "c" then () |
78 if UnparseC.term t' = "c" then () |
79 else error "NTH 3 [a,b,c,d,e] = c ..changed"; |
79 else error "NTH 3 [a,b,c,d,e] = c ..changed"; |
82 "--------------------- Length ------------------------------------------------"; |
82 "--------------------- Length ------------------------------------------------"; |
83 "--------------------- Length ------------------------------------------------"; |
83 "--------------------- Length ------------------------------------------------"; |
84 val prog_expr = get_rls @{context} "prog_expr" |
84 val prog_expr = get_rls @{context} "prog_expr" |
85 |
85 |
86 val thy = @{theory ListC}; |
86 val thy = @{theory ListC}; |
87 val t = TermC.str2term "Length [1, 1, 1]"; |
87 val t = TermC.parse_test @{context} "Length [1, 1, 1]"; |
88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
89 UnparseC.term t = "1 + Length [1, 1]"; |
89 UnparseC.term t = "1 + Length [1, 1]"; |
90 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
90 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
91 UnparseC.term t = "1 + (1 + Length [1])"; |
91 UnparseC.term t = "1 + (1 + Length [1])"; |
92 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
92 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t; |
95 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t; |
95 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t; |
96 val NONE = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t; |
96 val NONE = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t; |
97 if UnparseC.term t = "1 + (1 + (1 + 0))" then () |
97 if UnparseC.term t = "1 + (1 + (1 + 0))" then () |
98 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed"; |
98 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0)) ..changed"; |
99 |
99 |
100 val t = TermC.str2term "Length [1, 1, 1]"; |
100 val t = TermC.parse_test @{context} "Length [1, 1, 1]"; |
101 val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t; |
101 val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t; |
102 if UnparseC.term t = "3" then () |
102 if UnparseC.term t = "3" then () |
103 else error "Length [1, 1, 1] = 3 ..prog_expr changed"; |
103 else error "Length [1, 1, 1] = 3 ..prog_expr changed"; |
104 |
104 |
105 val t = TermC.str2term "Length [1, 1, 1]"; |
105 val t = TermC.parse_test @{context} "Length [1, 1, 1]"; |
106 val t = eval_prog_expr ctxt prog_expr t; |
106 val t = eval_prog_expr ctxt prog_expr t; |
107 case t of |
107 case t of |
108 Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () |
108 Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () |
109 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed"; |
109 | _ => error "Length [1, 1, 1] = 3 ..eval_prog_expr changed"; |
110 |
110 |