92 (* second statement *) |
92 (* second statement *) |
93 val y = Free ("y",ak_type) |
93 val y = Free ("y",ak_type) |
94 val stmnt2 = HOLogic.mk_Trueprop |
94 val stmnt2 = HOLogic.mk_Trueprop |
95 (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0))) |
95 (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0))) |
96 |
96 |
97 val proof2 = fn _ => EVERY [DatatypePackage.case_tac "y" 1, |
97 val proof2 = fn {prems, context} => |
98 asm_simp_tac (HOL_basic_ss addsimps simp1) 1, |
98 InductTacs.case_tac (context |> Variable.declare_term y) ("y", NONE) 1 THEN |
99 rtac @{thm exI} 1, |
99 asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN |
100 rtac @{thm refl} 1] |
100 rtac @{thm exI} 1 THEN |
|
101 rtac @{thm refl} 1 |
101 |
102 |
102 (* third statement *) |
103 (* third statement *) |
103 val (inject_thm,thy3) = |
104 val (inject_thm,thy3) = |
104 PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 |
105 PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2 |
105 |
106 |