src/FOLP/ex/If.thy
author wenzelm
Thu, 23 Jul 2015 14:25:05 +0200
changeset 60770 240563fbf41d
parent 58957 c9e744ea8a38
child 61337 4645502c3c64
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     1
theory If
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     2
imports FOLP
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     3
begin
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     4
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 25991
diff changeset
     5
definition "if" :: "[o,o,o]=>o" where
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     6
  "if(P,Q,R) == P&Q | ~P&R"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
     7
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
     8
schematic_lemma ifI:
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
     9
  assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    10
  shows "?p : if(P,Q,R)"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    11
apply (unfold if_def)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58957
diff changeset
    12
apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    13
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    14
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    15
schematic_lemma ifE:
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    16
  assumes 1: "p : if(P,Q,R)" and
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    17
    2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    18
    3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    19
  shows "?p : S"
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    20
apply (insert 1)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    21
apply (unfold if_def)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58957
diff changeset
    22
apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    23
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    24
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    25
schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    26
apply (rule iffI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    27
apply (erule ifE)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    28
apply (erule ifE)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    29
apply (rule ifI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    30
apply (rule ifI)
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    31
oops
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    32
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58957
diff changeset
    33
ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    34
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    35
schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58957
diff changeset
    36
apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    37
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    38
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    39
schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58957
diff changeset
    40
apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents: 19796
diff changeset
    41
done
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 0
diff changeset
    42
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
end