equal
deleted
inserted
replaced
58 |
58 |
59 (********) |
59 (********) |
60 val _ = writeln " Proving monotonicity..."; |
60 val _ = writeln " Proving monotonicity..."; |
61 |
61 |
62 val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) = |
62 val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) = |
63 big_rec_def |> rep_thm |> #prop |> unvarify; |
63 big_rec_def |> rep_thm |> #prop |> Logic.unvarify; |
64 |
64 |
65 val bnd_mono = |
65 val bnd_mono = |
66 prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs), |
66 prove_goalw_cterm [] |
67 fn _ => |
67 (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs))) |
|
68 (fn _ => |
68 [rtac (Collect_subset RS bnd_monoI) 1, |
69 [rtac (Collect_subset RS bnd_monoI) 1, |
69 REPEAT (ares_tac (basic_monos @ monos) 1)]); |
70 REPEAT (ares_tac (basic_monos @ monos) 1)]); |
70 |
71 |
71 val dom_subset = standard (big_rec_def RS Fp.subs); |
72 val dom_subset = standard (big_rec_def RS Fp.subs); |
72 |
73 |
100 val mk_disj_rls = |
101 val mk_disj_rls = |
101 let fun f rl = rl RS disjI1 |
102 let fun f rl = rl RS disjI1 |
102 and g rl = rl RS disjI2 |
103 and g rl = rl RS disjI2 |
103 in accesses_bal(f, g, asm_rl) end; |
104 in accesses_bal(f, g, asm_rl) end; |
104 |
105 |
105 val intrs = map (prove_term sign part_rec_defs) |
106 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) |
106 (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms))); |
107 (map (cterm_of sign) intr_tms ~~ |
|
108 map intro_tacsf (mk_disj_rls(length intr_tms))); |
107 |
109 |
108 (********) |
110 (********) |
109 val _ = writeln " Proving the elimination rule..."; |
111 val _ = writeln " Proving the elimination rule..."; |
110 |
112 |
111 (*Includes rules for succ and Pair since they are common constructions*) |
113 (*Includes rules for succ and Pair since they are common constructions*) |