1894 Tactic.rewrite_goals_tac [pred_def] THEN |
1894 Tactic.rewrite_goals_tac [pred_def] THEN |
1895 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
1895 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
1896 Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1)); |
1896 Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1)); |
1897 |
1897 |
1898 val conjuncts = |
1898 val conjuncts = |
1899 Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, |
1899 (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, |
1900 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] |
1900 Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
1901 |> Drule.conj_elim_precise (length ts); |
1901 |> Drule.conj_elim_precise (length ts); |
1902 val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) => |
1902 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
1903 Tactic.prove_plain defs_thy [] [] t (fn _ => |
1903 Tactic.prove_plain defs_thy [] [] t (fn _ => |
1904 Tactic.rewrite_goals_tac defs THEN |
1904 Tactic.rewrite_goals_tac defs THEN |
1905 Tactic.compose_tac (false, ax, 0) 1)); |
1905 Tactic.compose_tac (false, ax, 0) 1)); |
1906 in (defs_thy, (statement, intro, axioms)) end; |
1906 in (defs_thy, (statement, intro, axioms)) end; |
1907 |
1907 |