equal
deleted
inserted
replaced
|
1 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
|
2 notation ( output) "Trueprop" ("#_" [1000] 1000) |
1 |
3 |
2 ML {* |
4 ML {* |
3 fun dest_cbinop t = |
5 fun dest_cbinop t = |
4 let |
6 let |
5 val (t2, rhs) = Thm.dest_comb t; |
7 val (t2, rhs) = Thm.dest_comb t; |
70 |
72 |
71 |
73 |
72 lemma trueprop_cong: |
74 lemma trueprop_cong: |
73 shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)" |
75 shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)" |
74 by auto |
76 by auto |
|
77 |
|
78 lemma list_induct_hol4: |
|
79 fixes P :: "'a list ⇒ bool" |
|
80 assumes a: "((P []) ∧ (∀t. (P t) ⟶ (∀h. (P (h # t)))))" |
|
81 shows "∀l. (P l)" |
|
82 using a |
|
83 apply (rule_tac allI) |
|
84 apply (induct_tac "l") |
|
85 apply (simp) |
|
86 apply (metis) |
|
87 done |
|
88 |